Metamath Proof Explorer

Theorem esplymhp

Description: The K -th elementary symmetric polynomial is homogeneous of degree K . (Contributed by Thierry Arnoux, 18-Jan-2026)

Ref Expression
Hypotheses esplympl.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
esplympl.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
esplympl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
esplympl.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
esplymhp.1 ⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
Assertion esplymhp ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( 𝐻 ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 esplympl.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 esplympl.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
3 esplympl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 esplympl.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
5 esplymhp.1 ⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
6 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝐼 ∈ Fin )
7 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 )
8 6 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 ) → 𝐼 ∈ Fin )
9 ssrab2 ⊢ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼
10 9 a1i ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼 )
11 10 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝑏 ∈ 𝒫 𝐼 )
12 11 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝑏 ⊆ 𝐼 )
13 12 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 ) → 𝑏 ⊆ 𝐼 )
14 indf ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑏 ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) : 𝐼 ⟶ { 0 , 1 } )
15 8 13 14 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) : 𝐼 ⟶ { 0 , 1 } )
16 7 15 feq1dd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 ) → 𝑑 : 𝐼 ⟶ { 0 , 1 } )
17 indf1o ⊢ ( 𝐼 ∈ Fin → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) )
18 f1of ⊢ ( ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
19 2 17 18 3syl ⊢ ( 𝜑 → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
20 19 ffund ⊢ ( 𝜑 → Fun ( 𝟭 ‘ 𝐼 ) )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → Fun ( 𝟭 ‘ 𝐼 ) )
22 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
23 1 ssrab3 ⊢ 𝐷 ⊆ ( ℕ0 ↑m 𝐼 )
24 22 23 ssexi ⊢ 𝐷 ∈ V
25 24 a1i ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝐷 ∈ V )
26 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
27 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝐾 ∈ ℕ0 )
28 1 6 26 27 esplylem ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 )
29 simplr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑑 ∈ 𝐷 )
30 simpr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) )
31 30 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ¬ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) = ( 0g ‘ 𝑅 ) )
32 indf ⊢ ( ( 𝐷 ∈ V ∧ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 ) → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
33 25 28 32 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
34 33 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 ) → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
35 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 ) → 𝑑 ∈ 𝐷 )
36 34 35 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 ) → ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ∈ { 0 , 1 } )
37 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 ) → ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 )
38 elprn2 ⊢ ( ( ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ∈ { 0 , 1 } ∧ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 ) → ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) = 0 )
39 36 37 38 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 ) → ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) = 0 )
40 39 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ) = ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) )
41 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
42 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
43 41 42 zrh0 ⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
44 3 43 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
45 44 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
46 40 45 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ) = ( 0g ‘ 𝑅 ) )
47 1 2 3 4 esplyfval ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) )
48 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) )
49 48 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) ‘ 𝑑 ) )
50 33 29 fvco3d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) ‘ 𝑑 ) = ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ) )
51 49 50 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) = ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ) )
52 51 30 eqnetrrd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ) ≠ ( 0g ‘ 𝑅 ) )
53 52 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ) ≠ ( 0g ‘ 𝑅 ) )
54 46 53 pm2.21ddne ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) = ( 0g ‘ 𝑅 ) )
55 31 54 mtand ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ¬ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 )
56 nne ⊢ ( ¬ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) ≠ 1 ↔ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) = 1 )
57 55 56 sylib ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) = 1 )
58 ind1a ⊢ ( ( 𝐷 ∈ V ∧ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 ∧ 𝑑 ∈ 𝐷 ) → ( ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) = 1 ↔ 𝑑 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) )
59 58 biimpa ⊢ ( ( ( 𝐷 ∈ V ∧ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑑 ) = 1 ) → 𝑑 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
60 25 28 29 57 59 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑑 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
61 fvelima ⊢ ( ( Fun ( 𝟭 ‘ 𝐼 ) ∧ 𝑑 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) → ∃ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 )
62 21 60 61 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ∃ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 )
63 16 62 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑑 : 𝐼 ⟶ { 0 , 1 } )
64 6 63 indfsid ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑑 = ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝑑 supp 0 ) ) )
65 64 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ℂfld Σg 𝑑 ) = ( ℂfld Σg ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝑑 supp 0 ) ) ) )
66 nn0subm ⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
67 66 a1i ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ℕ0 ∈ ( SubMnd ‘ ℂfld ) )
68 23 a1i ⊢ ( 𝜑 → 𝐷 ⊆ ( ℕ0 ↑m 𝐼 ) )
69 68 sselda ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑑 ∈ ( ℕ0 ↑m 𝐼 ) )
70 69 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑑 ∈ ( ℕ0 ↑m 𝐼 ) )
71 6 67 70 elmaprd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑑 : 𝐼 ⟶ ℕ0 )
72 eqid ⊢ ( ℂfld ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
73 6 67 71 72 gsumsubm ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ℂfld Σg 𝑑 ) = ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) )
74 suppssdm ⊢ ( 𝑑 supp 0 ) ⊆ dom 𝑑
75 2 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝐼 ∈ Fin )
76 nn0ex ⊢ ℕ0 ∈ V
77 76 a1i ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ℕ0 ∈ V )
78 75 77 69 elmaprd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑑 : 𝐼 ⟶ ℕ0 )
79 78 fdmd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → dom 𝑑 = 𝐼 )
80 79 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → dom 𝑑 = 𝐼 )
81 74 80 sseqtrid ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑑 supp 0 ) ⊆ 𝐼 )
82 6 81 ssfid ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑑 supp 0 ) ∈ Fin )
83 6 81 82 gsumind ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ℂfld Σg ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝑑 supp 0 ) ) ) = ( ♯ ‘ ( 𝑑 supp 0 ) ) )
84 7 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) supp 0 ) = ( 𝑑 supp 0 ) )
85 indsupp ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑏 ⊆ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) supp 0 ) = 𝑏 )
86 8 13 85 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) supp 0 ) = 𝑏 )
87 84 86 eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 ) → ( 𝑑 supp 0 ) = 𝑏 )
88 87 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 ) → ( ♯ ‘ ( 𝑑 supp 0 ) ) = ( ♯ ‘ 𝑏 ) )
89 fveqeq2 ⊢ ( 𝑐 = 𝑏 → ( ( ♯ ‘ 𝑐 ) = 𝐾 ↔ ( ♯ ‘ 𝑏 ) = 𝐾 ) )
90 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 ) → 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } )
91 89 90 elrabrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 ) → ( ♯ ‘ 𝑏 ) = 𝐾 )
92 88 91 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑏 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑏 ) = 𝑑 ) → ( ♯ ‘ ( 𝑑 supp 0 ) ) = 𝐾 )
93 92 62 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ♯ ‘ ( 𝑑 supp 0 ) ) = 𝐾 )
94 83 93 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ℂfld Σg ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝑑 supp 0 ) ) ) = 𝐾 )
95 65 73 94 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝐾 )
96 95 ex ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝐾 ) )
97 96 ralrimiva ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐷 ( ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝐾 ) )
98 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
99 eqid ⊢ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
100 1 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
101 1 2 3 4 99 esplympl ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
102 5 98 99 42 100 4 101 ismhp3 ⊢ ( 𝜑 → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( 𝐻 ‘ 𝐾 ) ↔ ∀ 𝑑 ∈ 𝐷 ( ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝐾 ) ) )
103 97 102 mpbird ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( 𝐻 ‘ 𝐾 ) )