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

Metamath Proof Explorer

Theorem evlsvarval

Description: Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024)

Ref Expression
Hypotheses evlsvarval.q 
|- Q = ( ( I evalSub S ) ` R )
evlsvarval.p 
|- P = ( I mPoly U )
evlsvarval.v 
|- V = ( I mVar U )
evlsvarval.u 
|- U = ( S |`s R )
evlsvarval.k 
|- K = ( Base ` S )
evlsvarval.b 
|- B = ( Base ` P )
evlsvarval.i 
|- ( ph -> I e. W )
evlsvarval.s 
|- ( ph -> S e. CRing )
evlsvarval.r 
|- ( ph -> R e. ( SubRing ` S ) )
evlsvarval.x 
|- ( ph -> X e. I )
evlsvarval.a 
|- ( ph -> A e. ( K ^m I ) )
Assertion evlsvarval 
|- ( ph -> ( ( V ` X ) e. B /\ ( ( Q ` ( V ` X ) ) ` A ) = ( A ` X ) ) )

Proof

Step Hyp Ref Expression
1 evlsvarval.q 
 |-  Q = ( ( I evalSub S ) ` R )
2 evlsvarval.p 
 |-  P = ( I mPoly U )
3 evlsvarval.v 
 |-  V = ( I mVar U )
4 evlsvarval.u 
 |-  U = ( S |`s R )
5 evlsvarval.k 
 |-  K = ( Base ` S )
6 evlsvarval.b 
 |-  B = ( Base ` P )
7 evlsvarval.i 
 |-  ( ph -> I e. W )
8 evlsvarval.s 
 |-  ( ph -> S e. CRing )
9 evlsvarval.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
10 evlsvarval.x 
 |-  ( ph -> X e. I )
11 evlsvarval.a 
 |-  ( ph -> A e. ( K ^m I ) )
12 4 subrgring 
 |-  ( R e. ( SubRing ` S ) -> U e. Ring )
13 9 12 syl 
 |-  ( ph -> U e. Ring )
14 2 3 6 7 13 10 mvrcl 
 |-  ( ph -> ( V ` X ) e. B )
15 fveq1 
 |-  ( g = A -> ( g ` X ) = ( A ` X ) )
16 1 3 4 5 7 8 9 10 evlsvar 
 |-  ( ph -> ( Q ` ( V ` X ) ) = ( g e. ( K ^m I ) |-> ( g ` X ) ) )
17 fvexd 
 |-  ( ph -> ( A ` X ) e. _V )
18 15 16 11 17 fvmptd4 
 |-  ( ph -> ( ( Q ` ( V ` X ) ) ` A ) = ( A ` X ) )
19 14 18 jca 
 |-  ( ph -> ( ( V ` X ) e. B /\ ( ( Q ` ( V ` X ) ) ` A ) = ( A ` X ) ) )