---

Step * 1 1 of Lemma sg-inv-unique


1. sg : s-Group
2. x : Point
3. y : Point
4. (x y) ≡ 1
5. ((x^-1 x) y) ≡ (x^-1 1)
⊢ x^-1 ≡ y
BY
{ (RWW "sg-inv-op sg-op-id sg-id-op" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  x  :  Point
3.  y  :  Point
4.  (x  y)  \mequiv{}  1
5.  ((x\^{}-1  x)  y)  \mequiv{}  (x\^{}-1  1)
\mvdash{}  x\^{}-1  \mequiv{}  y


By

---

Latex:
(RWW  "sg-inv-op  sg-op-id  sg-id-op"  (-1)  THEN  Auto)

---

Home Index