---

Step * 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. (f 0) = ((f (-r x)) +s (f x)) ∈ |s|
⊢ f[-r x] = (-s f[x]) ∈ |s|
BY
{ (RWO "-3" (-1) THENA Auto) }

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

---

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.  (f  0)  =  ((f  (-r  x))  +s  (f  x))
\mvdash{}  f[-r  x]  =  (-s  f[x])


By

---

Latex:
(RWO  "-3"  (-1)  THENA  Auto)

---

Home Index