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