---

Step * 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) ∧ ((f 1) = 1 ∈ |s|)
6. f[0] = 0 ∈ |s|
7. x : |r|
8. (f (x +r (-r x))) = ((f x) +s (f (-r x))) ∈ |s|
⊢ f[-r x] = (-s f[x]) ∈ |s|
BY
{ (RW RngNormC (-1) THEN 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. (f 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)  \mwedge{}  ((f  1)  =  1)
6.  f[0]  =  0
7.  x  :  |r|
8.  (f  (x  +r  (-r  x)))  =  ((f  x)  +s  (f  (-r  x)))
\mvdash{}  f[-r  x]  =  (-s  f[x])


By

---

Latex:
(RW  RngNormC  (-1)  THEN  Auto)

---

Home Index