---

Step * 1 1 1 1 of Lemma rng_hom_minus


1. r : Rng
2. s : Rng
3. f : |r| ⟶ |s|
4. ∀[a1,a2:|r|].  ((f (a1 +r a2)) = ((f a1) +s (f a2)) ∈ |s|)
5. FunThru2op(|r|;|s|;*;*;f)
6. (f 1) = 1 ∈ |s|
7. f[0] = 0 ∈ |s|
8. x : |r|
9. 0 = ((f (-r x)) +s (f x)) ∈ |s|
⊢ f[-r x] = (-s f[x]) ∈ |s|
BY
{ ((Assert ((-s f[x]) +s 0) = ((-s f[x]) +s ((f (-r x)) +s (f x))) ∈ |s| BY
          Auto)
   THEN Unfold `so_apply` -1
   THEN (RW RngNormC (-1) THENA Auto)
   THEN Unfold `so_apply` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  s  :  Rng
3.  f  :  |r|  {}\mrightarrow{}  |s|
4.  \mforall{}[a1,a2:|r|].    ((f  (a1  +r  a2))  =  ((f  a1)  +s  (f  a2)))
5.  FunThru2op(|r|;|s|;*;*;f)
6.  (f  1)  =  1
7.  f[0]  =  0
8.  x  :  |r|
9.  0  =  ((f  (-r  x))  +s  (f  x))
\mvdash{}  f[-r  x]  =  (-s  f[x])


By

---

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

---

Home Index