---

Step * of Lemma rng_hom_minus

∀[r,s:Rng]. ∀[f:|r| ⟶ |s|].  ∀[x:|r|]. (f[-r x] = (-s f[x]) ∈ |s|) supposing rng_hom_p(r;s;f)
BY
{ (InstLemma `rng_hom_zero` [] THEN RepeatFor 4 (ParallelLast') THEN D -2) }

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

---

Latex:

---

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


By

---

Latex:
(InstLemma  `rng\_hom\_zero`  []  THEN  RepeatFor  4  (ParallelLast')  THEN  D  -2)

---

Home Index