---

Step * 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
⊢ EquivRel(|g|;x,y.x ≡ y (mod s in g))
BY
{ AbEval ``equiv_rel refl sym trans eqv_mod_subset`` 0 
THEN Auto }

1
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))

2
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))

3
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
⊢ s (a * (~ c))

---

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
\mvdash{}  EquivRel(|g|;x,y.x  \mequiv{}  y  (mod  s  in  g))


By

---

Latex:
AbEval  ``equiv\_rel  refl  sym  trans  eqv\_mod\_subset``  0 
THEN  Auto

---

Home Index