git @ Cat's Eye Technologies Eqthy / 6e3a6d3
Checkpoint this proof in progress. Chris Pressey 2 years ago
1 changed file(s) with 42 addition(s) and 0 deletion(s). Raw diff Collapse all Expand all
+42
-0
eg/semigroup-right-inverse-is-left.eqthy.md less more
0 Right Inverse for All is Left Inverse
1 =====================================
2
3 See [Right Inverse for All is Left Inverse](https://proofwiki.org/wiki/Right_Inverse_for_All_is_Left_Inverse)
4 on proofwiki.org.
5
6 TODO DRAFT
7
8 First we need the semigroup axioms.
9
10 axiom (#id-right) mul(A, e) = A
11 axiom (#assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
12 axiom (#inv-right) mul(A, inv(A)) = e
13
14 Next we need "Product of Semigroup Element with Right Inverse is Idempotent"
15 as a lemma.
16
17 theorem (#product-of-semigroup-element-with-right-inverse-is-idempotent)
18 mul(mul(inv(A), A), mul(inv(A), A)) = mul(inv(A), A)
19 proof
20 mul(inv(A), A) = mul(inv(A), A)
21 mul(mul(inv(A), e), A) = mul(inv(A), A)
22 mul(mul(inv(A), mul(A, inv(A))), A) = mul(inv(A), A)
23 mul(mul(mul(inv(A), A), inv(A)), A) = mul(inv(A), A)
24 mul(mul(inv(A), A), mul(inv(A), A)) = mul(inv(A), A)
25 qed
26
27 Finally we need this proof.
28
29 theorem (#right-inverse-for-semigroup-is-left-inverse)
30 // TODO FIXME DRAFT IN PROGRESS
31 // mul(A, inv(A)) = mul(inv(A), A)
32 mul(mul(mul(inv(A), A), inv(mul(inv(A), A))), inv(mul(inv(A), A))) = e
33 proof
34 e = e
35 mul(A, inv(A)) = e
36 mul(mul(A, e), inv(A)) = e
37 mul(mul(A, mul(A, inv(A))), inv(A)) = e
38 mul(mul(mul(A, A), inv(A)), inv(A)) = e
39 mul(mul(mul(mul(inv(A), A), mul(inv(A), A)), inv(mul(inv(A), A))), inv(mul(inv(A), A))) = e [by substitution of mul(inv(A), A) into A]
40 mul(mul(mul(inv(A), A), inv(mul(inv(A), A))), inv(mul(inv(A), A))) = e [by #product-of-semigroup-element-with-right-inverse-is-idempotent]
41 qed