Metamath Proof Explorer

Definition df-extv

Description: Define the "variable extension" function. The function ( ( I extendVars R )A ) converts polynomials with variables indexed by ( I \ { A } ) into polynomials indexed by I , and therefore maps elements of ( ( I \ { A } ) mPoly R ) onto ( I mPoly R ) . (Contributed by Thierry Arnoux, 20-Jan-2026)

Ref Expression
Assertion 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 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cextv 
 |-  extendVars
1 vi 
 |-  i
2 cvv 
 |-  _V
3 vr 
 |-  r
4 va 
 |-  a
5 1 cv 
 |-  i
6 vf 
 |-  f
7 cbs 
 |-  Base
8 4 cv 
 |-  a
9 8 csn 
 |-  { a }
10 5 9 cdif 
 |-  ( i \ { a } )
11 cmpl 
 |-  mPoly
12 3 cv 
 |-  r
13 10 12 11 co 
 |-  ( ( i \ { a } ) mPoly r )
14 13 7 cfv 
 |-  ( Base ` ( ( i \ { a } ) mPoly r ) )
15 vx 
 |-  x
16 vh 
 |-  h
17 cn0 
 |-  NN0
18 cmap 
 |-  ^m
19 17 5 18 co 
 |-  ( NN0 ^m i )
20 16 cv 
 |-  h
21 cfsupp 
 |-  finSupp
22 cc0 
 |-  0
23 20 22 21 wbr 
 |-  h finSupp 0
24 23 16 19 crab 
 |-  { h e. ( NN0 ^m i ) | h finSupp 0 }
25 15 cv 
 |-  x
26 8 25 cfv 
 |-  ( x ` a )
27 26 22 wceq 
 |-  ( x ` a ) = 0
28 6 cv 
 |-  f
29 25 10 cres 
 |-  ( x |` ( i \ { a } ) )
30 29 28 cfv 
 |-  ( f ` ( x |` ( i \ { a } ) ) )
31 c0g 
 |-  0g
32 12 31 cfv 
 |-  ( 0g ` r )
33 27 30 32 cif 
 |-  if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) )
34 15 24 33 cmpt 
 |-  ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) )
35 6 14 34 cmpt 
 |-  ( 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 ) ) ) )
36 4 5 35 cmpt 
 |-  ( 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 ) ) ) ) )
37 1 3 2 2 36 cmpo 
 |-  ( 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 ) ) ) ) ) )
38 0 37 wceq 
 |-  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 ) ) ) ) ) )