---

Step * of Lemma generated-s-subgroup_wf

∀[sg:s-Group]. ∀[P:Point ⟶ ℙ].  generated-s-subgroup(sg;f.P[f]) ∈ s-Group supposing ∀f:Point. (P[f] ⇒ P[f^-1])
BY
{ (ProveWfLemma THEN D 0 THEN Auto THEN ExRepD) }

1
1. sg : s-Group
2. P : Point ⟶ ℙ
3. ∀f:Point. (P[f] ⇒ P[f^-1])
⊢ ∃L:Point List. ((∀f∈L.P[f]) ∧ 1 ≡ reduce(λx,y. (x y);1;L))

2
1. sg : s-Group
2. P : Point ⟶ ℙ
3. ∀f:Point. (P[f] ⇒ P[f^-1])
4. g : Point
5. L : Point List
6. (∀f∈L.P[f])
7. g ≡ reduce(λx,y. (x y);1;L)
⊢ ∃L:Point List. ((∀f∈L.P[f]) ∧ g^-1 ≡ reduce(λx,y. (x y);1;L))

3
1. sg : s-Group
2. P : Point ⟶ ℙ
3. ∀f:Point. (P[f] ⇒ P[f^-1])
4. ∀g:Point
     ((∃L:Point List. ((∀f∈L.P[f]) ∧ g ≡ reduce(λx,y. (x y);1;L)))
     ⇒ (∃L:Point List. ((∀f∈L.P[f]) ∧ g^-1 ≡ reduce(λx,y. (x y);1;L))))
5. g : Point
6. y : Point
7. L1 : Point List
8. (∀f∈L1.P[f])
9. g ≡ reduce(λx,y. (x y);1;L1)
10. L : Point List
11. (∀f∈L.P[f])
12. y ≡ reduce(λx,y. (x y);1;L)
⊢ ∃L:Point List. ((∀f∈L.P[f]) ∧ (g y) ≡ reduce(λx,y. (x y);1;L))

---

Latex:

---

Latex:
\mforall{}[sg:s-Group].  \mforall{}[P:Point  {}\mrightarrow{}  \mBbbP{}].
    generated-s-subgroup(sg;f.P[f])  \mmember{}  s-Group  supposing  \mforall{}f:Point.  (P[f]  {}\mRightarrow{}  P[f\^{}-1])


By

---

Latex:
(ProveWfLemma  THEN  D  0  THEN  Auto  THEN  ExRepD)

---

Home Index