---

Step * 2 2 1 2 1 of Lemma generated-s-subgroup_wf


1. sg : s-Group
2. u : Point
3. v : Point List
4. ∀a:Point. (a^-1 reduce(λx,y. (x y);1;v))^-1 ≡ reduce(λx,y. (x y);a;rev(map(λf.f^-1;v)))
5. a : Point
6. v1 : Point
7. reduce(λx,y. (x y);1;v) = v1 ∈ Point
⊢ (a^-1 (u v1))^-1 ≡ ((u^-1 a)^-1 v1)^-1
BY
{ (RWW "sg-inv-of-op sg-inv-inv" 0 THENA Auto) }

1
1. sg : s-Group
2. u : Point
3. v : Point List
4. ∀a:Point. (a^-1 reduce(λx,y. (x y);1;v))^-1 ≡ reduce(λx,y. (x y);a;rev(map(λf.f^-1;v)))
5. a : Point
6. v1 : Point
7. reduce(λx,y. (x y);1;v) = v1 ∈ Point
⊢ ((v1^-1 u^-1) a) ≡ (v1^-1 (u^-1 a))

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  u  :  Point
3.  v  :  Point  List
4.  \mforall{}a:Point.  (a\^{}-1  reduce(\mlambda{}x,y.  (x  y);1;v))\^{}-1  \mequiv{}  reduce(\mlambda{}x,y.  (x  y);a;rev(map(\mlambda{}f.f\^{}-1;v)))
5.  a  :  Point
6.  v1  :  Point
7.  reduce(\mlambda{}x,y.  (x  y);1;v)  =  v1
\mvdash{}  (a\^{}-1  (u  v1))\^{}-1  \mequiv{}  ((u\^{}-1  a)\^{}-1  v1)\^{}-1


By

---

Latex:
(RWW  "sg-inv-of-op  sg-inv-inv"  0  THENA  Auto)

---

Home Index