This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evlvarval

Description: Polynomial evaluation builder for a variable. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses evlvarval.1 
|- Q = ( I eval S )
evlvarval.2 
|- P = ( I mPoly S )
evlvarval.3 
|- K = ( Base ` S )
evlvarval.4 
|- B = ( Base ` P )
evlvarval.5 
|- .xb = ( .r ` P )
evlvarval.6 
|- .x. = ( .r ` S )
evlvarval.7 
|- ( ph -> I e. Z )
evlvarval.8 
|- ( ph -> S e. CRing )
evlvarval.9 
|- ( ph -> A e. ( K ^m I ) )
evlvarval.10 
|- V = ( I mVar S )
evlvarval.11 
|- ( ph -> X e. I )
Assertion evlvarval 
|- ( ph -> ( ( V ` X ) e. B /\ ( ( Q ` ( V ` X ) ) ` A ) = ( A ` X ) ) )

Proof

Step Hyp Ref Expression
1 evlvarval.1 
 |-  Q = ( I eval S )
2 evlvarval.2 
 |-  P = ( I mPoly S )
3 evlvarval.3 
 |-  K = ( Base ` S )
4 evlvarval.4 
 |-  B = ( Base ` P )
5 evlvarval.5 
 |-  .xb = ( .r ` P )
6 evlvarval.6 
 |-  .x. = ( .r ` S )
7 evlvarval.7 
 |-  ( ph -> I e. Z )
8 evlvarval.8 
 |-  ( ph -> S e. CRing )
9 evlvarval.9 
 |-  ( ph -> A e. ( K ^m I ) )
10 evlvarval.10 
 |-  V = ( I mVar S )
11 evlvarval.11 
 |-  ( ph -> X e. I )
12 8 crngringd 
 |-  ( ph -> S e. Ring )
13 2 10 4 7 12 11 mvrcl 
 |-  ( ph -> ( V ` X ) e. B )
14 fveq1 
 |-  ( a = A -> ( a ` X ) = ( A ` X ) )
15 1 10 3 7 8 11 evlvar 
 |-  ( ph -> ( Q ` ( V ` X ) ) = ( a e. ( K ^m I ) |-> ( a ` X ) ) )
16 3 fvexi 
 |-  K e. _V
17 16 a1i 
 |-  ( ph -> K e. _V )
18 7 17 9 elmaprd 
 |-  ( ph -> A : I --> K )
19 18 11 ffvelcdmd 
 |-  ( ph -> ( A ` X ) e. K )
20 14 15 9 19 fvmptd4 
 |-  ( ph -> ( ( Q ` ( V ` X ) ) ` A ) = ( A ` X ) )
21 13 20 jca 
 |-  ( ph -> ( ( V ` X ) e. B /\ ( ( Q ` ( V ` X ) ) ` A ) = ( A ` X ) ) )