---

Step * of Lemma ideal_defines_eqv

∀r:CRng. ∀[a:|r| ⟶ ℙ]. (a Ideal of r ⇒ EquivRel(|r|;u,v.a (u +r (-r v))))
BY
{ (Auto THEN D -1 THEN RepeatFor 2 (D 0) THEN Auto) }

1
1. r : CRng@i'
2. [a] : |r| ⟶ ℙ
3. a SubGrp of r↓+gp@i
4. ∀a@0,b:|r|.  ((a a@0) ⇒ (a (a@0 * b)))@i
5. a@0 : |r|@i
⊢ a (a@0 +r (-r a@0))

2
1. r : CRng@i'
2. [a] : |r| ⟶ ℙ
3. a SubGrp of r↓+gp@i
4. ∀a@0,b:|r|.  ((a a@0) ⇒ (a (a@0 * b)))@i
⊢ Sym(|r|;u,v.a (u +r (-r v)))

3
1. r : CRng@i'
2. [a] : |r| ⟶ ℙ
3. a SubGrp of r↓+gp@i
4. ∀a@0,b:|r|.  ((a a@0) ⇒ (a (a@0 * b)))@i
⊢ Trans(|r|;u,v.a (u +r (-r v)))

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}[a:|r|  {}\mrightarrow{}  \mBbbP{}].  (a  Ideal  of  r  {}\mRightarrow{}  EquivRel(|r|;u,v.a  (u  +r  (-r  v))))


By

---

Latex:
(Auto  THEN  D  -1  THEN  RepeatFor  2  (D  0)  THEN  Auto)

---

Home Index