Metamath Proof Explorer

Theorem extvval

Description: Value of the "variable extension" function. (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 )
extvval.j 
|- J = ( I \ { a } )
extvval.m 
|- M = ( Base ` ( J mPoly R ) )
Assertion extvval 
|- ( ph -> ( I extendVars R ) = ( a e. I |-> ( f e. M |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .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 extvval.j 
 |-  J = ( I \ { a } )
6 extvval.m 
 |-  M = ( Base ` ( J mPoly R ) )
7 df-extv 
 |-  extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) )
8 7 a1i 
 |-  ( ph -> extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) ) )
9 simpl 
 |-  ( ( i = I /\ r = R ) -> i = I )
10 difeq1 
 |-  ( i = I -> ( i \ { a } ) = ( I \ { a } ) )
11 10 5 eqtr4di 
 |-  ( i = I -> ( i \ { a } ) = J )
12 11 adantr 
 |-  ( ( i = I /\ r = R ) -> ( i \ { a } ) = J )
13 simpr 
 |-  ( ( i = I /\ r = R ) -> r = R )
14 12 13 oveq12d 
 |-  ( ( i = I /\ r = R ) -> ( ( i \ { a } ) mPoly r ) = ( J mPoly R ) )
15 14 fveq2d 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( ( i \ { a } ) mPoly r ) ) = ( Base ` ( J mPoly R ) ) )
16 15 6 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( ( i \ { a } ) mPoly r ) ) = M )
17 oveq2 
 |-  ( i = I -> ( NN0 ^m i ) = ( NN0 ^m I ) )
18 17 rabeqdv 
 |-  ( i = I -> { h e. ( NN0 ^m i ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | h finSupp 0 } )
19 18 1 eqtr4di 
 |-  ( i = I -> { h e. ( NN0 ^m i ) | h finSupp 0 } = D )
20 19 adantr 
 |-  ( ( i = I /\ r = R ) -> { h e. ( NN0 ^m i ) | h finSupp 0 } = D )
21 10 reseq2d 
 |-  ( i = I -> ( x |` ( i \ { a } ) ) = ( x |` ( I \ { a } ) ) )
22 21 fveq2d 
 |-  ( i = I -> ( f ` ( x |` ( i \ { a } ) ) ) = ( f ` ( x |` ( I \ { a } ) ) ) )
23 22 adantr 
 |-  ( ( i = I /\ r = R ) -> ( f ` ( x |` ( i \ { a } ) ) ) = ( f ` ( x |` ( I \ { a } ) ) ) )
24 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
25 24 adantl 
 |-  ( ( i = I /\ r = R ) -> ( 0g ` r ) = ( 0g ` R ) )
26 25 2 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( 0g ` r ) = .0. )
27 23 26 ifeq12d 
 |-  ( ( i = I /\ r = R ) -> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) = if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) )
28 20 27 mpteq12dv 
 |-  ( ( i = I /\ r = R ) -> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) = ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) )
29 16 28 mpteq12dv 
 |-  ( ( i = I /\ r = R ) -> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) = ( f e. M |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) )
30 9 29 mpteq12dv 
 |-  ( ( i = I /\ r = R ) -> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) = ( a e. I |-> ( f e. M |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) ) )
31 30 adantl 
 |-  ( ( ph /\ ( i = I /\ r = R ) ) -> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) = ( a e. I |-> ( f e. M |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) ) )
32 3 elexd 
 |-  ( ph -> I e. _V )
33 4 elexd 
 |-  ( ph -> R e. _V )
34 3 mptexd 
 |-  ( ph -> ( a e. I |-> ( f e. M |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) ) e. _V )
35 8 31 32 33 34 ovmpod 
 |-  ( ph -> ( I extendVars R ) = ( a e. I |-> ( f e. M |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) ) )