---

Step * 2 2 2 1 1 1 2 1 of Lemma add-ipoly-ringeq


1. r : Rng
2. v2 : |r|
3. v3 : |r|
4. v4 : |r|
5. v5 : |r|
⊢ ((v2 +r v3) = 0 ∈ |r|) ⇒ ((v4 +r v5) = ((v2 +r v4) +r (v3 +r v5)) ∈ |r|)
BY
{ Auto }

1
1. r : Rng
2. v2 : |r|
3. v3 : |r|
4. v4 : |r|
5. v5 : |r|
6. (v2 +r v3) = 0 ∈ |r|
⊢ (v4 +r v5) = ((v2 +r v4) +r (v3 +r v5)) ∈ |r|

---

Latex:

---

Latex:

1.  r  :  Rng
2.  v2  :  |r|
3.  v3  :  |r|
4.  v4  :  |r|
5.  v5  :  |r|
\mvdash{}  ((v2  +r  v3)  =  0)  {}\mRightarrow{}  ((v4  +r  v5)  =  ((v2  +r  v4)  +r  (v3  +r  v5)))


By

---

Latex:
Auto

---

Home Index