---

Step * of Lemma mk-s-subgroup_wf

∀[sg:s-Group]. ∀[P:Point ⟶ ℙ].  mk-s-subgroup(sg;x.P[x]) ∈ s-Group supposing sg-subgroup(sg;x.P[x])
BY
{ ((Auto THEN D -1 THEN ExRepD)
   THEN Unfold `mk-s-subgroup` 0
   THEN MemCD
   THEN (All  (RWO "set-ss-point set-ss-eq set-ss-sep") THENA Auto)) }

1
1. sg : s-Group
2. P : Point ⟶ ℙ
3. P[1]
4. ∀x:Point. (P[x] ⇒ P[x^-1])
5. ∀x,y:Point.  (P[x] ⇒ P[y] ⇒ P[(x y)])
⊢ set-ss(sg;x.P[x]) ∈ SeparationSpace

2
1. sg : s-Group
2. P : Point ⟶ ℙ
3. P[1]
4. ∀x:Point. (P[x] ⇒ P[x^-1])
5. ∀x,y:Point.  (P[x] ⇒ P[y] ⇒ P[(x y)])
⊢ 1 ∈ {x:Point| P[x]} 

3
1. sg : s-Group
2. P : Point ⟶ ℙ
3. P[1]
4. ∀x:Point. (P[x] ⇒ P[x^-1])
5. ∀x,y:Point.  (P[x] ⇒ P[y] ⇒ P[(x y)])
⊢ λx.x^-1 ∈ {x:Point| P[x]}  ⟶ {x:Point| P[x]} 

4
1. sg : s-Group
2. P : Point ⟶ ℙ
3. P[1]
4. ∀x:Point. (P[x] ⇒ P[x^-1])
5. ∀x,y:Point.  (P[x] ⇒ P[y] ⇒ P[(x y)])
⊢ λx,y. (x y) ∈ {f:{x:Point| P[x]}  ⟶ {x:Point| P[x]}  ⟶ {x:Point| P[x]} | 
             (∀x,y,z:{x:Point| P[x]} .  f x (f y z) ≡ f (f x y) z)
             ∧ (∀x:{x:Point| P[x]} . f x 1 ≡ x)
             ∧ (∀x:{x:Point| P[x]} . f x ((λx.x^-1) x) ≡ 1)} 

5
1. sg : s-Group
2. P : Point ⟶ ℙ
3. P[1]
4. ∀x:Point. (P[x] ⇒ P[x^-1])
5. ∀x,y:Point.  (P[x] ⇒ P[y] ⇒ P[(x y)])
⊢ sg."opsep" ∈ ∀x,x',y,y':{x:Point| P[x]} .  ((λx,y. (x y)) x y # (λx,y. (x y)) x' y ⇒ (x # x' ∨ y # y'))

6
1. sg : s-Group
2. P : Point ⟶ ℙ
3. P[1]
4. ∀x:Point. (P[x] ⇒ P[x^-1])
5. ∀x,y:Point.  (P[x] ⇒ P[y] ⇒ P[(x y)])
⊢ sg."invsep" ∈ ∀x,y:{x:Point| P[x]} .  ((λx.x^-1) x # (λx.x^-1) y ⇒ x # y)

---

Latex:

---

Latex:
\mforall{}[sg:s-Group].  \mforall{}[P:Point  {}\mrightarrow{}  \mBbbP{}].    mk-s-subgroup(sg;x.P[x])  \mmember{}  s-Group  supposing  sg-subgroup(sg;x.P[x])


By

---

Latex:
((Auto  THEN  D  -1  THEN  ExRepD)
  THEN  Unfold  `mk-s-subgroup`  0
  THEN  MemCD
  THEN  (All    (RWO  "set-ss-point  set-ss-eq  set-ss-sep")  THENA  Auto))

---

Home Index