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

Metamath Proof Explorer

Theorem issply

Description: Conditions for being a symmetric polynomial. (Contributed by Thierry Arnoux, 18-Jan-2026)

Ref Expression
Hypotheses issply.s ⊢ 𝑆 = ( SymGrp ‘ 𝐼 )
issply.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
issply.m ⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
issply.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
issply.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
issply.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
issply.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
issply.1 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ ( 𝑥 ∘ 𝑝 ) ) = ( 𝐹 ‘ 𝑥 ) )
Assertion issply ( 𝜑 → 𝐹 ∈ ( 𝐼 SymPoly 𝑅 ) )

Proof

Step Hyp Ref Expression
1 issply.s ⊢ 𝑆 = ( SymGrp ‘ 𝐼 )
2 issply.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
3 issply.m ⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
4 issply.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
5 issply.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 issply.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
7 issply.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
8 issply.1 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ ( 𝑥 ∘ 𝑝 ) ) = ( 𝐹 ‘ 𝑥 ) )
9 8 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑝 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) )
10 coeq2 ⊢ ( 𝑐 = 𝑑 → ( 𝑦 ∘ 𝑐 ) = ( 𝑦 ∘ 𝑑 ) )
11 10 fveq2d ⊢ ( 𝑐 = 𝑑 → ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) = ( 𝑒 ‘ ( 𝑦 ∘ 𝑑 ) ) )
12 11 mpteq2dv ⊢ ( 𝑐 = 𝑑 → ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) ) = ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑑 ) ) ) )
13 fveq1 ⊢ ( 𝑒 = 𝑓 → ( 𝑒 ‘ ( 𝑦 ∘ 𝑑 ) ) = ( 𝑓 ‘ ( 𝑦 ∘ 𝑑 ) ) )
14 13 mpteq2dv ⊢ ( 𝑒 = 𝑓 → ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑑 ) ) ) = ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑦 ∘ 𝑑 ) ) ) )
15 12 14 cbvmpov ⊢ ( 𝑐 ∈ 𝑃 , 𝑒 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) ) ) = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑦 ∘ 𝑑 ) ) ) )
16 coeq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∘ 𝑑 ) = ( 𝑥 ∘ 𝑑 ) )
17 16 fveq2d ⊢ ( 𝑦 = 𝑥 → ( 𝑓 ‘ ( 𝑦 ∘ 𝑑 ) ) = ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) )
18 17 cbvmptv ⊢ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑦 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) )
19 18 a1i ⊢ ( ( 𝑑 ∈ 𝑃 ∧ 𝑓 ∈ 𝑀 ) → ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑦 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
20 19 mpoeq3ia ⊢ ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑦 ∘ 𝑑 ) ) ) ) = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
21 15 20 eqtri ⊢ ( 𝑐 ∈ 𝑃 , 𝑒 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) ) ) = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
22 21 a1i ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑐 ∈ 𝑃 , 𝑒 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) ) ) = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) )
23 4 eqcomi ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = 𝐷
24 23 a1i ⊢ ( ( 𝑑 = 𝑝 ∧ 𝑓 = 𝐹 ) → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = 𝐷 )
25 simpr ⊢ ( ( 𝑑 = 𝑝 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
26 coeq2 ⊢ ( 𝑑 = 𝑝 → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝑝 ) )
27 26 adantr ⊢ ( ( 𝑑 = 𝑝 ∧ 𝑓 = 𝐹 ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝑝 ) )
28 25 27 fveq12d ⊢ ( ( 𝑑 = 𝑝 ∧ 𝑓 = 𝐹 ) → ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) = ( 𝐹 ‘ ( 𝑥 ∘ 𝑝 ) ) )
29 24 28 mpteq12dv ⊢ ( ( 𝑑 = 𝑝 ∧ 𝑓 = 𝐹 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑝 ) ) ) )
30 29 adantl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑑 = 𝑝 ∧ 𝑓 = 𝐹 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑝 ) ) ) )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝑃 )
32 7 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝐹 ∈ 𝑀 )
33 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
34 4 33 rabex2 ⊢ 𝐷 ∈ V
35 34 a1i ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝐷 ∈ V )
36 35 mptexd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑝 ) ) ) ∈ V )
37 22 30 31 32 36 ovmpod ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ( 𝑐 ∈ 𝑃 , 𝑒 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) ) ) 𝐹 ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑝 ) ) ) )
38 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
39 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
40 4 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
41 38 39 3 40 32 mplelf ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
42 41 feqmptd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝐹 = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) )
43 9 37 42 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ( 𝑐 ∈ 𝑃 , 𝑒 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) ) ) 𝐹 ) = 𝐹 )
44 43 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝑃 ( 𝑝 ( 𝑐 ∈ 𝑃 , 𝑒 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) ) ) 𝐹 ) = 𝐹 )
45 1 2 3 21 5 mplvrpmga ⊢ ( 𝜑 → ( 𝑐 ∈ 𝑃 , 𝑒 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) ) ) ∈ ( 𝑆 GrpAct 𝑀 ) )
46 2 45 7 isfxp ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑀 FixPts ( 𝑐 ∈ 𝑃 , 𝑒 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) ) ) ) ↔ ∀ 𝑝 ∈ 𝑃 ( 𝑝 ( 𝑐 ∈ 𝑃 , 𝑒 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) ) ) 𝐹 ) = 𝐹 ) )
47 44 46 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 FixPts ( 𝑐 ∈ 𝑃 , 𝑒 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) ) ) ) )
48 1 2 3 21 5 6 splyval ⊢ ( 𝜑 → ( 𝐼 SymPoly 𝑅 ) = ( 𝑀 FixPts ( 𝑐 ∈ 𝑃 , 𝑒 ∈ 𝑀 ↦ ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑒 ‘ ( 𝑦 ∘ 𝑐 ) ) ) ) ) )
49 47 48 eleqtrrd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐼 SymPoly 𝑅 ) )