---

Step * 1 2 3 of Lemma princ_ideal_wf


1. r : Rng
2. a : |r|
3. b2 : |r|
4. 0 = (a * b2) ∈ |r|
5. ∀a@0:|r|. ((∃b:|r|. (a@0 = (a * b) ∈ |r|)) ⇒ (∃b:|r|. ((-r a@0) = (a * b) ∈ |r|)))
6. a@0 : |r|@i
7. b : |r|@i
8. b1 : |r|@i
9. a@0 = (a * b1) ∈ |r|
10. b@0 : |r|@i
11. b = (a * b@0) ∈ |r|
⊢ ∃b@0:|r|. ((a@0 +r b) = (a * b@0) ∈ |r|)
BY
{ TACTIC:(With ⌜b1 +r b@0⌝ (D 0)⋅ THEN Auto THEN RWO "-1 -3" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  a  :  |r|
3.  b2  :  |r|
4.  0  =  (a  *  b2)
5.  \mforall{}a@0:|r|.  ((\mexists{}b:|r|.  (a@0  =  (a  *  b)))  {}\mRightarrow{}  (\mexists{}b:|r|.  ((-r  a@0)  =  (a  *  b))))
6.  a@0  :  |r|@i
7.  b  :  |r|@i
8.  b1  :  |r|@i
9.  a@0  =  (a  *  b1)
10.  b@0  :  |r|@i
11.  b  =  (a  *  b@0)
\mvdash{}  \mexists{}b@0:|r|.  ((a@0  +r  b)  =  (a  *  b@0))


By

---

Latex:
TACTIC:(With  \mkleeneopen{}b1  +r  b@0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  RWO  "-1  -3"  0  THEN  Auto)

---

Home Index