---

Step * 1 of Lemma rng_hom_zero


1. r : Rng
2. s : Rng
3. f : |r| ⟶ |s|
4. FunThru2op(|r|;|s|;+r;+s;f)
5. FunThru2op(|r|;|s|;*;*;f)
6. (f 1) = 1 ∈ |s|
7. (f 0) = ((f 0) +s (f 0)) ∈ |s|
⊢ (f 0) = 0 ∈ |s|
BY
{ ((Assert ((-s (f 0)) +s (f 0)) = ((-s (f 0)) +s ((f 0) +s (f 0))) ∈ |s| BY Auto) THEN RW RngNormC (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  s  :  Rng
3.  f  :  |r|  {}\mrightarrow{}  |s|
4.  FunThru2op(|r|;|s|;+r;+s;f)
5.  FunThru2op(|r|;|s|;*;*;f)
6.  (f  1)  =  1
7.  (f  0)  =  ((f  0)  +s  (f  0))
\mvdash{}  (f  0)  =  0


By

---

Latex:
((Assert  ((-s  (f  0))  +s  (f  0))  =  ((-s  (f  0))  +s  ((f  0)  +s  (f  0)))  BY
                Auto)
  THEN  RW  RngNormC  (-1)
  THEN  Auto)

---

Home Index