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

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 ⊢ 𝑆 = ( SymGrp ‘ 𝐼 )
mplvrpmga.2 ⊢ 𝑃 = ( Base ‘ 𝑆 )
mplvrpmga.3 ⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
mplvrpmga.4 ⊢ 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
mplvrpmga.5 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mplvrpmfgalem.z ⊢ 0 = ( 0g ‘ 𝑅 )
mplvrpmfgalem.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
mplvrpmfgalem.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
Assertion mplvrpmfgalem ( 𝜑 → ( 𝑄 𝐴 𝐹 ) finSupp 0 )

Proof

Step Hyp Ref Expression
1 mplvrpmga.1 ⊢ 𝑆 = ( SymGrp ‘ 𝐼 )
2 mplvrpmga.2 ⊢ 𝑃 = ( Base ‘ 𝑆 )
3 mplvrpmga.3 ⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
4 mplvrpmga.4 ⊢ 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
5 mplvrpmga.5 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 mplvrpmfgalem.z ⊢ 0 = ( 0g ‘ 𝑅 )
7 mplvrpmfgalem.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
8 mplvrpmfgalem.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
9 4 a1i ⊢ ( 𝜑 → 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) )
10 simpr ⊢ ( ( 𝑑 = 𝑄 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
11 coeq2 ⊢ ( 𝑑 = 𝑄 → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝑄 ) )
12 11 adantr ⊢ ( ( 𝑑 = 𝑄 ∧ 𝑓 = 𝐹 ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝑄 ) )
13 10 12 fveq12d ⊢ ( ( 𝑑 = 𝑄 ∧ 𝑓 = 𝐹 ) → ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) = ( 𝐹 ‘ ( 𝑥 ∘ 𝑄 ) ) )
14 13 mpteq2dv ⊢ ( ( 𝑑 = 𝑄 ∧ 𝑓 = 𝐹 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑄 ) ) ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝑄 ∧ 𝑓 = 𝐹 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑄 ) ) ) )
16 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
17 16 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V
18 17 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V )
19 18 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑄 ) ) ) ∈ V )
20 9 15 8 7 19 ovmpod ⊢ ( 𝜑 → ( 𝑄 𝐴 𝐹 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑄 ) ) ) )
21 breq1 ⊢ ( ℎ = ( 𝑥 ∘ 𝑄 ) → ( ℎ finSupp 0 ↔ ( 𝑥 ∘ 𝑄 ) finSupp 0 ) )
22 nn0ex ⊢ ℕ0 ∈ V
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ℕ0 ∈ V )
24 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐼 ∈ 𝑉 )
25 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
26 25 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
27 26 psrbagf ⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } → 𝑥 : 𝐼 ⟶ ℕ0 )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
29 1 2 symgbasf1o ⊢ ( 𝑄 ∈ 𝑃 → 𝑄 : 𝐼 –1-1-onto→ 𝐼 )
30 8 29 syl ⊢ ( 𝜑 → 𝑄 : 𝐼 –1-1-onto→ 𝐼 )
31 f1of ⊢ ( 𝑄 : 𝐼 –1-1-onto→ 𝐼 → 𝑄 : 𝐼 ⟶ 𝐼 )
32 30 31 syl ⊢ ( 𝜑 → 𝑄 : 𝐼 ⟶ 𝐼 )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑄 : 𝐼 ⟶ 𝐼 )
34 28 33 fcod ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝑄 ) : 𝐼 ⟶ ℕ0 )
35 23 24 34 elmapdd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝑄 ) ∈ ( ℕ0 ↑m 𝐼 ) )
36 26 psrbagfsupp ⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } → 𝑥 finSupp 0 )
37 36 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 finSupp 0 )
38 f1of1 ⊢ ( 𝑄 : 𝐼 –1-1-onto→ 𝐼 → 𝑄 : 𝐼 –1-1→ 𝐼 )
39 30 38 syl ⊢ ( 𝜑 → 𝑄 : 𝐼 –1-1→ 𝐼 )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑄 : 𝐼 –1-1→ 𝐼 )
41 0nn0 ⊢ 0 ∈ ℕ0
42 41 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 0 ∈ ℕ0 )
43 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
44 37 40 42 43 fsuppco ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝑄 ) finSupp 0 )
45 21 35 44 elrabd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝑄 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
46 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑥 ∘ 𝑄 ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑥 ∘ 𝑄 ) ) )
47 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ 𝑦 ) ) = ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ 𝑦 ) ) )
48 fveq2 ⊢ ( 𝑦 = ( 𝑥 ∘ 𝑄 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑥 ∘ 𝑄 ) ) )
49 45 46 47 48 fmptco ⊢ ( 𝜑 → ( ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑥 ∘ 𝑄 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑄 ) ) ) )
50 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
51 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
52 50 51 3 26 7 mplelf ⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
53 52 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ 𝑦 ) ) )
54 50 3 6 7 mplelsfi ⊢ ( 𝜑 → 𝐹 finSupp 0 )
55 53 54 breq1dd ⊢ ( 𝜑 → ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ 𝑦 ) ) finSupp 0 )
56 22 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
57 41 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
58 breq1 ⊢ ( ℎ = 𝑔 → ( ℎ finSupp 0 ↔ 𝑔 finSupp 0 ) )
59 58 cbvrabv ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { 𝑔 ∈ ( ℕ0 ↑m 𝐼 ) ∣ 𝑔 finSupp 0 }
60 30 5 5 56 57 25 59 fcobijfs2 ⊢ ( 𝜑 → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑥 ∘ 𝑄 ) ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } –1-1-onto→ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
61 f1of1 ⊢ ( ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑥 ∘ 𝑄 ) ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } –1-1-onto→ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑥 ∘ 𝑄 ) ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } –1-1→ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
62 60 61 syl ⊢ ( 𝜑 → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑥 ∘ 𝑄 ) ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } –1-1→ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
63 6 fvexi ⊢ 0 ∈ V
64 63 a1i ⊢ ( 𝜑 → 0 ∈ V )
65 18 mptexd ⊢ ( 𝜑 → ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ V )
66 55 62 64 65 fsuppco ⊢ ( 𝜑 → ( ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑥 ∘ 𝑄 ) ) ) finSupp 0 )
67 49 66 breq1dd ⊢ ( 𝜑 → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑄 ) ) ) finSupp 0 )
68 20 67 eqbrtrd ⊢ ( 𝜑 → ( 𝑄 𝐴 𝐹 ) finSupp 0 )