git @ Cat's Eye Technologies Eqthy / dc711ad
Add some lemmas regarding group inverses. Chris Pressey 2 years ago
2 changed file(s) with 45 addition(s) and 1 deletion(s). Raw diff Collapse all Expand all
+2
-1
eg/group-id-comm.eqthy.md less more
11 ===================================
22
33 See [Group Element Commutes with Inverse](https://proofwiki.org/wiki/Group_Element_Commutes_with_Inverse)
4 on proofwiki.org.
4 on proofwiki.org. (Although, this does not need even all the structure of a group; the axioms below
5 define a monoid.)
56
67 Note that this proof provides justifications on each step. For a proof as simple as this one,
78 this isn't actually necessary, and if they were omitted, the `eqthy` checker would still be
+43
-0
eg/group-inverse.eqthy.md less more
0 Group Inverse
1 =============
2
3 When working in abstract algebra, one sometimes proves that the identity
4 element is unique, or writes a proof leveraging that fact. However, such
5 proofs cannot be written in a purely equational setting, where the
6 identity element has been defined, not with an existence axiom, but as
7 a nullary operator.
8
9 So other techniques need to be used when working in
10 equational logic.
11
12 axiom (#id-right) mul(A, e) = A
13 axiom (#id-left) mul(e, A) = A
14 axiom (#assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
15 axiom (#inv-right) mul(A, inv(A)) = e
16 axiom (#inv-left) mul(inv(A), A) = e
17
18 ### Inverse of Identity is Identity
19
20 theorem
21 inv(e) = e
22 proof
23 e = e
24 mul(inv(e), e) = e [by #inv-left with A=e]
25 inv(e) = e
26 qed
27
28 ### Inverse of Group Inverse
29
30 Also see [Inverse of Group Inverse](https://proofwiki.org/wiki/Inverse_of_Group_Inverse) on ProofWiki.
31
32 theorem
33 inv(inv(A)) = A
34 proof
35 e = e
36 e = mul(inv(A), A)
37 mul(inv(inv(A)), e) = mul(inv(inv(A)), mul(inv(A), A)) [by congruence of X and mul(inv(inv(A)), X)]
38 inv(inv(A)) = mul(inv(inv(A)), mul(inv(A), A))
39 inv(inv(A)) = mul(mul(inv(inv(A)), inv(A)), A)
40 inv(inv(A)) = mul(e, A) [by #inv-left]
41 inv(inv(A)) = A
42 qed