Step
*
1
1
1
of Lemma
sg-id-op
1. sg : s-Group
2. x : Point
3. (x x^-1) ≡ 1
4. (x^-1 x^-1^-1) ≡ 1
⊢ ((x x^-1) (x (x^-1 x^-1^-1))) ≡ x
BY
{ ((RW (AddrC [2;3] (LemmaC `sg-assoc`)) 0 THENA Auto) THEN (RW (AddrC [2;3;2] (HypC 3)) 0 THENA Auto)) }
1
1. sg : s-Group
2. x : Point
3. (x x^-1) ≡ 1
4. (x^-1 x^-1^-1) ≡ 1
⊢ ((x x^-1) (1 x^-1^-1)) ≡ x
Latex:
Latex:
1.  sg  :  s-Group
2.  x  :  Point
3.  (x  x\^{}-1)  \mequiv{}  1
4.  (x\^{}-1  x\^{}-1\^{}-1)  \mequiv{}  1
\mvdash{}  ((x  x\^{}-1)  (x  (x\^{}-1  x\^{}-1\^{}-1)))  \mequiv{}  x
By
Latex:
((RW  (AddrC  [2;3]  (LemmaC  `sg-assoc`))  0  THENA  Auto)
  THEN  (RW  (AddrC  [2;3;2]  (HypC  3))  0  THENA  Auto)
  )
Home
Index