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

Metamath Proof Explorer

Theorem extvfval

Description: The "variable extension" function evaluated for 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 ) )
Assertion extvfval 
|- ( ph -> ( ( I extendVars R ) ` A ) = ( f e. M |-> ( 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 sneq 
 |-  ( a = A -> { a } = { A } )
9 8 difeq2d 
 |-  ( a = A -> ( I \ { a } ) = ( I \ { A } ) )
10 9 6 eqtr4di 
 |-  ( a = A -> ( I \ { a } ) = J )
11 10 fvoveq1d 
 |-  ( a = A -> ( Base ` ( ( I \ { a } ) mPoly R ) ) = ( Base ` ( J mPoly R ) ) )
12 11 7 eqtr4di 
 |-  ( a = A -> ( Base ` ( ( I \ { a } ) mPoly R ) ) = M )
13 fveqeq2 
 |-  ( a = A -> ( ( x ` a ) = 0 <-> ( x ` A ) = 0 ) )
14 10 reseq2d 
 |-  ( a = A -> ( x |` ( I \ { a } ) ) = ( x |` J ) )
15 14 fveq2d 
 |-  ( a = A -> ( f ` ( x |` ( I \ { a } ) ) ) = ( f ` ( x |` J ) ) )
16 13 15 ifbieq1d 
 |-  ( a = A -> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) = if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) )
17 16 mpteq2dv 
 |-  ( a = A -> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) )
18 12 17 mpteq12dv 
 |-  ( a = A -> ( f e. ( Base ` ( ( I \ { a } ) mPoly R ) ) |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) = ( f e. M |-> ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) ) )
19 eqid 
 |-  ( I \ { a } ) = ( I \ { a } )
20 eqid 
 |-  ( Base ` ( ( I \ { a } ) mPoly R ) ) = ( Base ` ( ( I \ { a } ) mPoly R ) )
21 1 2 3 4 19 20 extvval 
 |-  ( ph -> ( I extendVars R ) = ( a e. I |-> ( f e. ( Base ` ( ( I \ { a } ) mPoly R ) ) |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) ) )
22 7 fvexi 
 |-  M e. _V
23 22 mptex 
 |-  ( f e. M |-> ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) ) e. _V
24 23 a1i 
 |-  ( ph -> ( f e. M |-> ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) ) e. _V )
25 18 21 5 24 fvmptd4 
 |-  ( ph -> ( ( I extendVars R ) ` A ) = ( f e. M |-> ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) ) )