---

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


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|
BY
{ (Subst' ((v2 +r v4) +r (v3 +r v5)) = ((v4 +r v5) +r (v2 +r v3)) ∈ |r| 0 THENA (Auto THEN RW RngNormC 0 THEN 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) = ((v4 +r v5) +r (v2 +r v3)) ∈ |r|

---

Latex:

---

Latex:

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


By

---

Latex:
(Subst'  ((v2  +r  v4)  +r  (v3  +r  v5))  =  ((v4  +r  v5)  +r  (v2  +r  v3))  0
  THENA  (Auto  THEN  RW  RngNormC  0  THEN  Auto)
  )

---

Home Index