---

Step * of Lemma imonomial-term-add-ringeq

∀r:Rng. ∀vs:ℤ List. ∀a,b:ℤ-o. ∀f:ℤ ⟶ |r|.  ((ring_term_value(f;imonomial-term(<a, vs>)) +r ring_term_value(f;imonomial-\000Cterm(<b, vs>))) = ring_term_value(f;imonomial-term(<a + b, vs>)) ∈ |r|)
BY
{ xxx(Auto THEN RWO "imonomial-term-linear-ringeq" 0 THEN Auto THEN RWO "int-to-ring-add" 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}r:Rng.  \mforall{}vs:\mBbbZ{}  List.  \mforall{}a,b:\mBbbZ{}\msupminus{}\msupzero{}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  |r|.
    ((ring\_term\_value(f;imonomial-term(<a,  vs>))  +r  ring\_term\_value(f;imonomial-term(<b,  vs>)))  =  ring\000C\_term\_value(f;imonomial-term(<a  +  b,  vs>)))


By

---

Latex:
xxx(Auto
        THEN  RWO  "imonomial-term-linear-ringeq"  0
        THEN  Auto
        THEN  RWO  "int-to-ring-add"  0
        THEN  Auto)xxx

---

Home Index