---

Step * 1 1 of Lemma rng_plus_comm

.....assertion..... 
1. r : Rng
2. a : |r|
3. b : |r|
⊢ ((a +r b) +r (((-r 1) +r 1) * (b +r a))) = (b +r a) ∈ |r|
BY
{ RWH (GenLemmaC 2 `rng_times_over_plus`) 0 THENA Auto }

1
1. r : Rng
2. a : |r|
3. b : |r|
⊢ ((a +r b) +r (((-r 1) * (b +r a)) +r (1 * (b +r a)))) = (b +r a) ∈ |r|

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  Rng
2.  a  :  |r|
3.  b  :  |r|
\mvdash{}  ((a  +r  b)  +r  (((-r  1)  +r  1)  *  (b  +r  a)))  =  (b  +r  a)


By

---

Latex:
RWH  (GenLemmaC  2  `rng\_times\_over\_plus`)  0  THENA  Auto

---

Home Index