---

Step * 1 1 of Lemma eqv_mod_subset_is_eqv


1. g : IGroup@i'
2. [s] : |g| ⟶ ℙ
3. s e@i
4. ∀a:|g|. ((s a) ⇒ (s (~ a)))@i
5. ∀a,b:|g|.  ((s a) ⇒ (s b) ⇒ (s (a * b)))@i
6. a : |g|@i
⊢ s (a * (~ a))
BY
{ RW GrpNormC 0
THEN Auto }

---

Latex:

---

Latex:

1.  g  :  IGroup@i'
2.  [s]  :  |g|  {}\mrightarrow{}  \mBbbP{}
3.  s  e@i
4.  \mforall{}a:|g|.  ((s  a)  {}\mRightarrow{}  (s  (\msim{}  a)))@i
5.  \mforall{}a,b:|g|.    ((s  a)  {}\mRightarrow{}  (s  b)  {}\mRightarrow{}  (s  (a  *  b)))@i
6.  a  :  |g|@i
\mvdash{}  s  (a  *  (\msim{}  a))


By

---

Latex:
RW  GrpNormC  0
THEN  Auto

---

Home Index