---

Step * 6 of Lemma mk-s-subgroup_wf


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)
BY
{ (Reduce 0
   THEN (Assert sg ∈ s-Group BY
               Auto)
   THEN (D 1 THENA Auto)
   THEN DoSubsume
   THEN Try (Trivial)
   THEN Folds ``sg-op sg-inv`` 0
   THEN Unfold `all` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  P  :  Point  {}\mrightarrow{}  \mBbbP{}
3.  P[1]
4.  \mforall{}x:Point.  (P[x]  {}\mRightarrow{}  P[x\^{}-1])
5.  \mforall{}x,y:Point.    (P[x]  {}\mRightarrow{}  P[y]  {}\mRightarrow{}  P[(x  y)])
\mvdash{}  sg."invsep"  \mmember{}  \mforall{}x,y:\{x:Point|  P[x]\}  .    ((\mlambda{}x.x\^{}-1)  x  \#  (\mlambda{}x.x\^{}-1)  y  {}\mRightarrow{}  x  \#  y)


By

---

Latex:
(Reduce  0
  THEN  (Assert  sg  \mmember{}  s-Group  BY
                          Auto)
  THEN  (D  1  THENA  Auto)
  THEN  DoSubsume
  THEN  Try  (Trivial)
  THEN  Folds  ``sg-op  sg-inv``  0
  THEN  Unfold  `all`  0
  THEN  Auto)

---

Home Index