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-idempotence.eqthy.md @master — view markup · raw · history · blame

Product of Semigroup Element with Right Inverse is Idempotent

See Product of Semigroup Element with Right Inverse is Idempotent on proofwiki.org.

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

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