Tree @master (Download .tar.gz)
- ..
- incorrect
- absorption-laws.eqthy.md
- boolean-algebra.eqthy.md
- combinatory-logic.eqthy.md
- group-inverse.eqthy.md
- group-theory.eqthy.md
- interior-algebra.eqthy.md
- monoid-id-comm.eqthy.md
- propositional-algebra.eqthy.md
- rule-congruence.eqthy.md
- rule-substitution.eqthy.md
- rule-variable-renaming.eqthy.md
- semigroup-idempotence.eqthy.md
- semigroup-right-inverse-is-left.eqthy.md
- set-difference.eqthy.md
- socks-and-shoes.eqthy.md
semigroup-right-inverse-is-left.eqthy.md @master — view markup · raw · history · blame
Right Inverse for All is Left Inverse
See Right Inverse for All is Left Inverse on proofwiki.org.
First we need the semigroup axioms (plus a right identity).
axiom (#id-right) mul(A, e) = A
axiom (#assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
axiom (#inv-right) mul(A, inv(A)) = e
Next we need Product of Semigroup Element with Right Inverse is Idempotent as a lemma.
theorem (#product-of-semigroup-element-with-right-inverse-is-idempotent)
mul(mul(inv(A), A), mul(inv(A), A)) = mul(inv(A), A)
proof
mul(inv(A), A) = mul(inv(A), A)
mul(mul(inv(A), e), A) = mul(inv(A), A)
mul(mul(inv(A), mul(A, inv(A))), A) = mul(inv(A), A)
mul(mul(mul(inv(A), A), inv(A)), A) = mul(inv(A), A)
mul(mul(inv(A), A), mul(inv(A), A)) = mul(inv(A), A)
qed
Finally we need this proof.
theorem (#right-inverse-for-semigroup-is-left-inverse)
mul(inv(A), A) = e
proof
e = e
mul(A, inv(A)) = e
mul(mul(inv(A), A), inv(mul(inv(A), A))) = e
[by substitution of mul(inv(A), A) into A]
mul(mul(mul(inv(A), A), mul(inv(A), A)), inv(mul(inv(A), A))) = e
[by #product-of-semigroup-element-with-right-inverse-is-idempotent]
mul(mul(inv(A), A), mul(mul(inv(A), A), inv(mul(inv(A), A)))) = e
mul(mul(inv(A), A), e) = e
mul(inv(A), A) = e
qed