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

Metamath Proof Explorer

Theorem extvfv

Description: The "variable extension" function evaluated for converting a given polynomial F by adding a variable with index A . (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses extvval.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
extvval.1 
|- .0. = ( 0g ` R )
extvval.i 
|- ( ph -> I e. V )
extvval.r 
|- ( ph -> R e. W )
extvfval.a 
|- ( ph -> A e. I )
extvfval.j 
|- J = ( I \ { A } )
extvfval.m 
|- M = ( Base ` ( J mPoly R ) )
extvfv.1 
|- ( ph -> F e. M )
Assertion extvfv 
|- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) )

Proof

Step Hyp Ref Expression
1 extvval.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
2 extvval.1 
 |-  .0. = ( 0g ` R )
3 extvval.i 
 |-  ( ph -> I e. V )
4 extvval.r 
 |-  ( ph -> R e. W )
5 extvfval.a 
 |-  ( ph -> A e. I )
6 extvfval.j 
 |-  J = ( I \ { A } )
7 extvfval.m 
 |-  M = ( Base ` ( J mPoly R ) )
8 extvfv.1 
 |-  ( ph -> F e. M )
9 fveq1 
 |-  ( f = F -> ( f ` ( x |` J ) ) = ( F ` ( x |` J ) ) )
10 9 ifeq1d 
 |-  ( f = F -> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) = if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) )
11 10 mpteq2dv 
 |-  ( f = F -> ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) )
12 1 2 3 4 5 6 7 extvfval 
 |-  ( ph -> ( ( I extendVars R ) ` A ) = ( f e. M |-> ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) ) )
13 ovex 
 |-  ( NN0 ^m I ) e. _V
14 1 13 rabex2 
 |-  D e. _V
15 14 a1i 
 |-  ( ph -> D e. _V )
16 15 mptexd 
 |-  ( ph -> ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) e. _V )
17 11 12 8 16 fvmptd4 
 |-  ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) )