---

Step * 1 3 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|. (s (a * (~ a)))
7. ∀a,b:|g|.  ((s (a * (~ b))) ⇒ (s (b * (~ a))))
8. a : |g|@i
9. b : |g|@i
10. c : |g|@i
11. s (a * (~ b))@i
12. s (b * (~ c))@i
13. s ((a * (~ b)) * (b * (~ c)))
⊢ s (a * (~ c))
BY
{ RW GrpNormC (-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.  \mforall{}a,b:|g|.    ((s  (a  *  (\msim{}  b)))  {}\mRightarrow{}  (s  (b  *  (\msim{}  a))))
8.  a  :  |g|@i
9.  b  :  |g|@i
10.  c  :  |g|@i
11.  s  (a  *  (\msim{}  b))@i
12.  s  (b  *  (\msim{}  c))@i
13.  s  ((a  *  (\msim{}  b))  *  (b  *  (\msim{}  c)))
\mvdash{}  s  (a  *  (\msim{}  c))


By

---

Latex:
RW  GrpNormC  (-1)
THEN  Auto

---

Home Index