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

Metamath Proof Explorer

Theorem splyval

Description: The symmetric polynomials for a given index I of variables and base ring R . These are the fixed points of the action A which permutes variables. (Contributed by Thierry Arnoux, 11-Jan-2026)

Ref Expression
Hypotheses splyval.s ⊢ 𝑆 = ( SymGrp ‘ 𝐼 )
splyval.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
splyval.m ⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
splyval.a ⊢ 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
splyval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
splyval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
Assertion splyval ( 𝜑 → ( 𝐼 SymPoly 𝑅 ) = ( 𝑀 FixPts 𝐴 ) )

Proof

Step Hyp Ref Expression
1 splyval.s ⊢ 𝑆 = ( SymGrp ‘ 𝐼 )
2 splyval.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
3 splyval.m ⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
4 splyval.a ⊢ 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
5 splyval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 splyval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
7 df-sply ⊢ SymPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) FixPts ( 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑖 ) ) , 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) ) )
8 7 a1i ⊢ ( 𝜑 → SymPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) FixPts ( 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑖 ) ) , 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) ) ) )
9 oveq12 ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 mPoly 𝑟 ) = ( 𝐼 mPoly 𝑅 ) )
10 9 fveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
11 10 3 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) = 𝑀 )
12 fveq2 ⊢ ( 𝑖 = 𝐼 → ( SymGrp ‘ 𝑖 ) = ( SymGrp ‘ 𝐼 ) )
13 12 adantr ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( SymGrp ‘ 𝑖 ) = ( SymGrp ‘ 𝐼 ) )
14 13 1 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( SymGrp ‘ 𝑖 ) = 𝑆 )
15 14 fveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( SymGrp ‘ 𝑖 ) ) = ( Base ‘ 𝑆 ) )
16 15 2 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( SymGrp ‘ 𝑖 ) ) = 𝑃 )
17 oveq2 ⊢ ( 𝑖 = 𝐼 → ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) )
18 17 adantr ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) )
19 18 rabeqdv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
20 19 mpteq1d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
21 16 11 20 mpoeq123dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑖 ) ) , 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) )
22 21 4 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑖 ) ) , 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) = 𝐴 )
23 11 22 oveq12d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) FixPts ( 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑖 ) ) , 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) ) = ( 𝑀 FixPts 𝐴 ) )
24 23 adantl ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → ( ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) FixPts ( 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑖 ) ) , 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) ) = ( 𝑀 FixPts 𝐴 ) )
25 5 elexd ⊢ ( 𝜑 → 𝐼 ∈ V )
26 6 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
27 ovexd ⊢ ( 𝜑 → ( 𝑀 FixPts 𝐴 ) ∈ V )
28 8 24 25 26 27 ovmpod ⊢ ( 𝜑 → ( 𝐼 SymPoly 𝑅 ) = ( 𝑀 FixPts 𝐴 ) )