---

Step * 3 1 1 of Lemma ideal_defines_eqv


1. r : CRng@i'
2. [a] : |r| ⟶ ℙ
3. a e@i
4. ∀a@0:|r↓+gp|. ((a a@0) ⇒ (a (~ a@0)))@i
5. ∀a@0,b:|r↓+gp|.  ((a a@0) ⇒ (a b) ⇒ (a (a@0 * b)))@i
6. ∀a@0,b:|r|.  ((a a@0) ⇒ (a (a@0 * b)))@i
7. a@0 : |r|@i
8. b : |r|@i
9. c : |r|@i
10. a (a@0 +r (-r b))@i
11. a (b +r (-r c))@i
12. a ((a@0 +r (-r b)) +r (b +r (-r c)))
⊢ a (a@0 +r (-r c))
BY
{ ((RW RngNormC (-1) THENA Auto) THEN RW RngNormC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng@i'
2.  [a]  :  |r|  {}\mrightarrow{}  \mBbbP{}
3.  a  e@i
4.  \mforall{}a@0:|r\mdownarrow{}+gp|.  ((a  a@0)  {}\mRightarrow{}  (a  (\msim{}  a@0)))@i
5.  \mforall{}a@0,b:|r\mdownarrow{}+gp|.    ((a  a@0)  {}\mRightarrow{}  (a  b)  {}\mRightarrow{}  (a  (a@0  *  b)))@i
6.  \mforall{}a@0,b:|r|.    ((a  a@0)  {}\mRightarrow{}  (a  (a@0  *  b)))@i
7.  a@0  :  |r|@i
8.  b  :  |r|@i
9.  c  :  |r|@i
10.  a  (a@0  +r  (-r  b))@i
11.  a  (b  +r  (-r  c))@i
12.  a  ((a@0  +r  (-r  b))  +r  (b  +r  (-r  c)))
\mvdash{}  a  (a@0  +r  (-r  c))


By

---

Latex:
((RW  RngNormC  (-1)  THENA  Auto)  THEN  RW  RngNormC  0  THEN  Auto)

---

Home Index