Metamath Proof Explorer

Theorem extvfvvcl

Description: Closure for 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 extvfvvcl.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
extvfvvcl.3 
|- .0. = ( 0g ` R )
extvfvvcl.i 
|- ( ph -> I e. V )
extvfvvcl.r 
|- ( ph -> R e. Ring )
extvfvvcl.b 
|- B = ( Base ` R )
extvfvvcl.j 
|- J = ( I \ { A } )
extvfvvcl.m 
|- M = ( Base ` ( J mPoly R ) )
extvfvvcl.1 
|- ( ph -> A e. I )
extvfvvcl.f 
|- ( ph -> F e. M )
extvfvvcl.x 
|- ( ph -> X e. D )
Assertion extvfvvcl 
|- ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) e. B )

Proof

Step Hyp Ref Expression
1 extvfvvcl.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
2 extvfvvcl.3 
 |-  .0. = ( 0g ` R )
3 extvfvvcl.i 
 |-  ( ph -> I e. V )
4 extvfvvcl.r 
 |-  ( ph -> R e. Ring )
5 extvfvvcl.b 
 |-  B = ( Base ` R )
6 extvfvvcl.j 
 |-  J = ( I \ { A } )
7 extvfvvcl.m 
 |-  M = ( Base ` ( J mPoly R ) )
8 extvfvvcl.1 
 |-  ( ph -> A e. I )
9 extvfvvcl.f 
 |-  ( ph -> F e. M )
10 extvfvvcl.x 
 |-  ( ph -> X e. D )
11 1 2 3 4 8 6 7 9 10 extvfvv 
 |-  ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) = if ( ( X ` A ) = 0 , ( F ` ( X |` J ) ) , .0. ) )
12 eqid 
 |-  ( J mPoly R ) = ( J mPoly R )
13 eqid 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } = { h e. ( NN0 ^m J ) | h finSupp 0 }
14 13 psrbasfsupp 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } = { h e. ( NN0 ^m J ) | ( `' h " NN ) e. Fin }
15 12 5 7 14 9 mplelf 
 |-  ( ph -> F : { h e. ( NN0 ^m J ) | h finSupp 0 } --> B )
16 breq1 
 |-  ( h = ( X |` J ) -> ( h finSupp 0 <-> ( X |` J ) finSupp 0 ) )
17 nn0ex 
 |-  NN0 e. _V
18 17 a1i 
 |-  ( ph -> NN0 e. _V )
19 3 difexd 
 |-  ( ph -> ( I \ { A } ) e. _V )
20 6 19 eqeltrid 
 |-  ( ph -> J e. _V )
21 1 ssrab3 
 |-  D C_ ( NN0 ^m I )
22 21 10 sselid 
 |-  ( ph -> X e. ( NN0 ^m I ) )
23 3 18 22 elmaprd 
 |-  ( ph -> X : I --> NN0 )
24 difssd 
 |-  ( ph -> ( I \ { A } ) C_ I )
25 6 24 eqsstrid 
 |-  ( ph -> J C_ I )
26 23 25 fssresd 
 |-  ( ph -> ( X |` J ) : J --> NN0 )
27 18 20 26 elmapdd 
 |-  ( ph -> ( X |` J ) e. ( NN0 ^m J ) )
28 breq1 
 |-  ( h = X -> ( h finSupp 0 <-> X finSupp 0 ) )
29 10 1 eleqtrdi 
 |-  ( ph -> X e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
30 28 29 elrabrd 
 |-  ( ph -> X finSupp 0 )
31 c0ex 
 |-  0 e. _V
32 31 a1i 
 |-  ( ph -> 0 e. _V )
33 30 32 fsuppres 
 |-  ( ph -> ( X |` J ) finSupp 0 )
34 16 27 33 elrabd 
 |-  ( ph -> ( X |` J ) e. { h e. ( NN0 ^m J ) | h finSupp 0 } )
35 15 34 ffvelcdmd 
 |-  ( ph -> ( F ` ( X |` J ) ) e. B )
36 5 2 ring0cl 
 |-  ( R e. Ring -> .0. e. B )
37 4 36 syl 
 |-  ( ph -> .0. e. B )
38 35 37 ifcld 
 |-  ( ph -> if ( ( X ` A ) = 0 , ( F ` ( X |` J ) ) , .0. ) e. B )
39 11 38 eqeltrd 
 |-  ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) e. B )