---

Step * of Lemma imonomial-cons-ringeq

∀r:CRng. ∀v:ℤ List. ∀u,a:ℤ. ∀f:ℤ ⟶ |r|.  (ring_term_value(f;imonomial-term(<a, [u / v]>)) = ((f u) * ring_term_value(f;\000Cimonomial-term(<a, v>))) ∈ |r|)
BY
{ xxx((Auto THEN (RWO "imonomial-term-linear-ringeq" 0 THENA Auto))
      THEN (Assert  ⌜ring_term_value(f;imonomial-term(<1, [u / v]>)) = ((f u) * ring_term_value(f;imonomial-term(<1, v>)\000C)) ∈ |r|⌝⋅ THENM (RWO "-1" 0 THEN Auto))
      )xxx }

1
.....assertion..... 
1. r : CRng
2. v : ℤ List
3. u : ℤ
4. a : ℤ
5. f : ℤ ⟶ |r|
⊢ ring_term_value(f;imonomial-term(<1, [u / v]>)) = ((f u) * ring_term_value(f;imonomial-term(<1, v>))) ∈ |r|

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}v:\mBbbZ{}  List.  \mforall{}u,a:\mBbbZ{}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  |r|.
    (ring\_term\_value(f;imonomial-term(<a,  [u  /  v]>))  =  ((f  u)  *  ring\_term\_value(f;imonomial-term(<a,  v\000C>))))


By

---

Latex:
xxx((Auto  THEN  (RWO  "imonomial-term-linear-ringeq"  0  THENA  Auto))
        THEN  (Assert    \mkleeneopen{}ring\_term\_value(f;imonomial-term(ə,  [u  /  v]>))  =  ((f  u)  *  ring\_term\_value(f;imon\000Comial-term(ə,  v>)))\mkleeneclose{}\mcdot{}  THENM  (RWO  "-1"  0  THEN  Auto))
        )xxx

---

Home Index