Metamath Proof Explorer

Theorem mplvrpmfgalem

Description: Permuting variables in a multivariate polynomial conserves finite support. (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses mplvrpmga.1 
|- S = ( SymGrp ` I )
mplvrpmga.2 
|- P = ( Base ` S )
mplvrpmga.3 
|- M = ( Base ` ( I mPoly R ) )
mplvrpmga.4 
|- A = ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) )
mplvrpmga.5 
|- ( ph -> I e. V )
mplvrpmfgalem.z 
|- .0. = ( 0g ` R )
mplvrpmfgalem.f 
|- ( ph -> F e. M )
mplvrpmfgalem.q 
|- ( ph -> Q e. P )
Assertion mplvrpmfgalem 
|- ( ph -> ( Q A F ) finSupp .0. )

Proof

Step Hyp Ref Expression
1 mplvrpmga.1 
 |-  S = ( SymGrp ` I )
2 mplvrpmga.2 
 |-  P = ( Base ` S )
3 mplvrpmga.3 
 |-  M = ( Base ` ( I mPoly R ) )
4 mplvrpmga.4 
 |-  A = ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) )
5 mplvrpmga.5 
 |-  ( ph -> I e. V )
6 mplvrpmfgalem.z 
 |-  .0. = ( 0g ` R )
7 mplvrpmfgalem.f 
 |-  ( ph -> F e. M )
8 mplvrpmfgalem.q 
 |-  ( ph -> Q e. P )
9 4 a1i 
 |-  ( ph -> A = ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) )
10 simpr 
 |-  ( ( d = Q /\ f = F ) -> f = F )
11 coeq2 
 |-  ( d = Q -> ( x o. d ) = ( x o. Q ) )
12 11 adantr 
 |-  ( ( d = Q /\ f = F ) -> ( x o. d ) = ( x o. Q ) )
13 10 12 fveq12d 
 |-  ( ( d = Q /\ f = F ) -> ( f ` ( x o. d ) ) = ( F ` ( x o. Q ) ) )
14 13 mpteq2dv 
 |-  ( ( d = Q /\ f = F ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` ( x o. Q ) ) ) )
15 14 adantl 
 |-  ( ( ph /\ ( d = Q /\ f = F ) ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` ( x o. Q ) ) ) )
16 ovex 
 |-  ( NN0 ^m I ) e. _V
17 16 rabex 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V
18 17 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V )
19 18 mptexd 
 |-  ( ph -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` ( x o. Q ) ) ) e. _V )
20 9 15 8 7 19 ovmpod 
 |-  ( ph -> ( Q A F ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` ( x o. Q ) ) ) )
21 breq1 
 |-  ( h = ( x o. Q ) -> ( h finSupp 0 <-> ( x o. Q ) finSupp 0 ) )
22 nn0ex 
 |-  NN0 e. _V
23 22 a1i 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> NN0 e. _V )
24 5 adantr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> I e. V )
25 eqid 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | h finSupp 0 }
26 25 psrbasfsupp 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
27 26 psrbagf 
 |-  ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } -> x : I --> NN0 )
28 27 adantl 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x : I --> NN0 )
29 1 2 symgbasf1o 
 |-  ( Q e. P -> Q : I -1-1-onto-> I )
30 8 29 syl 
 |-  ( ph -> Q : I -1-1-onto-> I )
31 f1of 
 |-  ( Q : I -1-1-onto-> I -> Q : I --> I )
32 30 31 syl 
 |-  ( ph -> Q : I --> I )
33 32 adantr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> Q : I --> I )
34 28 33 fcod 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. Q ) : I --> NN0 )
35 23 24 34 elmapdd 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. Q ) e. ( NN0 ^m I ) )
36 26 psrbagfsupp 
 |-  ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } -> x finSupp 0 )
37 36 adantl 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x finSupp 0 )
38 f1of1 
 |-  ( Q : I -1-1-onto-> I -> Q : I -1-1-> I )
39 30 38 syl 
 |-  ( ph -> Q : I -1-1-> I )
40 39 adantr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> Q : I -1-1-> I )
41 0nn0 
 |-  0 e. NN0
42 41 a1i 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> 0 e. NN0 )
43 simpr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
44 37 40 42 43 fsuppco 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. Q ) finSupp 0 )
45 21 35 44 elrabd 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. Q ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
46 eqidd 
 |-  ( ph -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( x o. Q ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( x o. Q ) ) )
47 eqidd 
 |-  ( ph -> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` y ) ) = ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` y ) ) )
48 fveq2 
 |-  ( y = ( x o. Q ) -> ( F ` y ) = ( F ` ( x o. Q ) ) )
49 45 46 47 48 fmptco 
 |-  ( ph -> ( ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` y ) ) o. ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( x o. Q ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` ( x o. Q ) ) ) )
50 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
51 eqid 
 |-  ( Base ` R ) = ( Base ` R )
52 50 51 3 26 7 mplelf 
 |-  ( ph -> F : { h e. ( NN0 ^m I ) | h finSupp 0 } --> ( Base ` R ) )
53 52 feqmptd 
 |-  ( ph -> F = ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` y ) ) )
54 50 3 6 7 mplelsfi 
 |-  ( ph -> F finSupp .0. )
55 53 54 breq1dd 
 |-  ( ph -> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` y ) ) finSupp .0. )
56 22 a1i 
 |-  ( ph -> NN0 e. _V )
57 41 a1i 
 |-  ( ph -> 0 e. NN0 )
58 breq1 
 |-  ( h = g -> ( h finSupp 0 <-> g finSupp 0 ) )
59 58 cbvrabv 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { g e. ( NN0 ^m I ) | g finSupp 0 }
60 30 5 5 56 57 25 59 fcobijfs2 
 |-  ( ph -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( x o. Q ) ) : { h e. ( NN0 ^m I ) | h finSupp 0 } -1-1-onto-> { h e. ( NN0 ^m I ) | h finSupp 0 } )
61 f1of1 
 |-  ( ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( x o. Q ) ) : { h e. ( NN0 ^m I ) | h finSupp 0 } -1-1-onto-> { h e. ( NN0 ^m I ) | h finSupp 0 } -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( x o. Q ) ) : { h e. ( NN0 ^m I ) | h finSupp 0 } -1-1-> { h e. ( NN0 ^m I ) | h finSupp 0 } )
62 60 61 syl 
 |-  ( ph -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( x o. Q ) ) : { h e. ( NN0 ^m I ) | h finSupp 0 } -1-1-> { h e. ( NN0 ^m I ) | h finSupp 0 } )
63 6 fvexi 
 |-  .0. e. _V
64 63 a1i 
 |-  ( ph -> .0. e. _V )
65 18 mptexd 
 |-  ( ph -> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` y ) ) e. _V )
66 55 62 64 65 fsuppco 
 |-  ( ph -> ( ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` y ) ) o. ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( x o. Q ) ) ) finSupp .0. )
67 49 66 breq1dd 
 |-  ( ph -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( F ` ( x o. Q ) ) ) finSupp .0. )
68 20 67 eqbrtrd 
 |-  ( ph -> ( Q A F ) finSupp .0. )