---

Step * of Lemma rng_hom_zero

∀[r,s:Rng]. ∀[f:|r| ⟶ |s|].  f[0] = 0 ∈ |s| supposing rng_hom_p(r;s;f)
BY
{ (Unfold `so_apply` 0
   THEN (((Unfold `rng_hom_p` 0) THEN Auto)
         THEN (Assert (f (0 +r 0)) = ((f 0) +s (f 0)) ∈ |s| BY
                     Auto)
         THEN (RW RngNormC (-1) THENA Auto))
   ) }

1
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|

---

Latex:

---

Latex:
\mforall{}[r,s:Rng].  \mforall{}[f:|r|  {}\mrightarrow{}  |s|].    f[0]  =  0  supposing  rng\_hom\_p(r;s;f)


By

---

Latex:
(Unfold  `so\_apply`  0
  THEN  (((Unfold  `rng\_hom\_p`  0)  THEN  Auto)
              THEN  (Assert  (f  (0  +r  0))  =  ((f  0)  +s  (f  0))  BY
                                      Auto)
              THEN  (RW  RngNormC  (-1)  THENA  Auto))
  )

---

Home Index