---

Step * 2 1 of Lemma ideal_defines_eqv


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
6. b : |r|@i
7. a (a@0 +r (-r b))@i
⊢ a (b +r (-r a@0))
BY
{ (InstHyp [⌜a@0 +r (-r b)⌝;⌜-r 1⌝] 4⋅ THENA 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
6. b : |r|@i
7. a (a@0 +r (-r b))@i
8. a ((a@0 +r (-r b)) * (-r 1))
⊢ a (b +r (-r a@0))

---

Latex:

---

Latex:

1.  r  :  CRng@i'
2.  [a]  :  |r|  {}\mrightarrow{}  \mBbbP{}
3.  a  SubGrp  of  r\mdownarrow{}+gp@i
4.  \mforall{}a@0,b:|r|.    ((a  a@0)  {}\mRightarrow{}  (a  (a@0  *  b)))@i
5.  a@0  :  |r|@i
6.  b  :  |r|@i
7.  a  (a@0  +r  (-r  b))@i
\mvdash{}  a  (b  +r  (-r  a@0))


By

---

Latex:
(InstHyp  [\mkleeneopen{}a@0  +r  (-r  b)\mkleeneclose{};\mkleeneopen{}-r  1\mkleeneclose{}]  4\mcdot{}  THENA  Auto)

---

Home Index