---

Step * 1 2 4 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,b:|r|.
     ((∃b:|r|. (a@0 = (a * b) ∈ |r|))
     ⇒ (∃b@0:|r|. (b = (a * b@0) ∈ |r|))
     ⇒ (∃b@0:|r|. ((a@0 +r b) = (a * b@0) ∈ |r|)))
7. a@0 : |r|@i
8. b : |r|@i
9. b1 : |r|@i
10. a@0 = (a * b1) ∈ |r|
⊢ ∃b@0:|r|. ((a@0 * b) = (a * b@0) ∈ |r|)
BY
{ TACTIC:(RWO "-1" 0 THEN Auto) }

1
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,b:|r|.
     ((∃b:|r|. (a@0 = (a * b) ∈ |r|))
     ⇒ (∃b@0:|r|. (b = (a * b@0) ∈ |r|))
     ⇒ (∃b@0:|r|. ((a@0 +r b) = (a * b@0) ∈ |r|)))
7. a@0 : |r|@i
8. b : |r|@i
9. b1 : |r|@i
10. a@0 = (a * b1) ∈ |r|
⊢ ∃b@0:|r|. (((a * b1) * b) = (a * b@0) ∈ |r|)

---

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.  \mforall{}a@0,b:|r|.
          ((\mexists{}b:|r|.  (a@0  =  (a  *  b)))
          {}\mRightarrow{}  (\mexists{}b@0:|r|.  (b  =  (a  *  b@0)))
          {}\mRightarrow{}  (\mexists{}b@0:|r|.  ((a@0  +r  b)  =  (a  *  b@0))))
7.  a@0  :  |r|@i
8.  b  :  |r|@i
9.  b1  :  |r|@i
10.  a@0  =  (a  *  b1)
\mvdash{}  \mexists{}b@0:|r|.  ((a@0  *  b)  =  (a  *  b@0))


By

---

Latex:
TACTIC:(RWO  "-1"  0  THEN  Auto)

---

Home Index