---

Step * 1 2 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|. (s (a * (~ a)))
7. a : |g|@i
8. b : |g|@i
9. s (a * (~ b))@i
⊢ s (b * (~ a))
BY
{ FHyp 4 [-1]
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.  \mforall{}a:|g|.  (s  (a  *  (\msim{}  a)))
7.  a  :  |g|@i
8.  b  :  |g|@i
9.  s  (a  *  (\msim{}  b))@i
\mvdash{}  s  (b  *  (\msim{}  a))


By

---

Latex:
FHyp  4  [-1]
THEN  Auto

---

Home Index