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" 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" THEN Auto))
      )xxx }

1
.....assertion..... 
1. CRng
2. : ℤ List
3. : ℤ
4. : ℤ
5. : ℤ ⟶ |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