---

Step * 1 of Lemma rng_hom_minus


1. r : Rng
2. s : Rng
3. f : |r| ⟶ |s|
4. FunThru2op(|r|;|s|;+r;+s;f)
5. FunThru2op(|r|;|s|;*;*;f) ∧ ((f 1) = 1 ∈ |s|)
6. f[0] = 0 ∈ |s|
⊢ ∀[x:|r|]. (f[-r x] = (-s f[x]) ∈ |s|)
BY
{ ((D 0 THENA Auto) THEN UnfoldTopAb 4 THEN (InstHyp [⌜x⌝;⌜-r x⌝] 4⋅ 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) ∧ ((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|

---

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)  \mwedge{}  ((f  1)  =  1)
6.  f[0]  =  0
\mvdash{}  \mforall{}[x:|r|].  (f[-r  x]  =  (-s  f[x]))


By

---

Latex:
((D  0  THENA  Auto)  THEN  UnfoldTopAb  4  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}-r  x\mkleeneclose{}]  4\mcdot{}  THENA  Auto))

---

Home Index