---

Step * of Lemma eqv_mod_subset_is_eqv

∀g:IGroup
  ∀[s:|g| ⟶ ℙ]
    ((s e)
    ⇒ (∀a:|g|. ((s a) ⇒ (s (~ a))))
    ⇒ (∀a,b:|g|.  ((s a) ⇒ (s b) ⇒ (s (a * b))))
    ⇒ EquivRel(|g|;x,y.x ≡ y (mod s in g)))
BY
{ 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
⊢ EquivRel(|g|;x,y.x ≡ y (mod s in g))

---

Latex:

---

Latex:
\mforall{}g:IGroup
    \mforall{}[s:|g|  {}\mrightarrow{}  \mBbbP{}]
        ((s  e)
        {}\mRightarrow{}  (\mforall{}a:|g|.  ((s  a)  {}\mRightarrow{}  (s  (\msim{}  a))))
        {}\mRightarrow{}  (\mforall{}a,b:|g|.    ((s  a)  {}\mRightarrow{}  (s  b)  {}\mRightarrow{}  (s  (a  *  b))))
        {}\mRightarrow{}  EquivRel(|g|;x,y.x  \mequiv{}  y  (mod  s  in  g)))


By

---

Latex:
Auto

---

Home Index