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 𝐴 ) )