Metamath Proof Explorer

Theorem esplyfval0

Description: The 0 -th elementary symmetric polynomial is the constant 1 . (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses esplyfval0.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
esplyfval0.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
esplyfval0.0 ⊢ 𝑈 = ( 1r ‘ ( 𝐼 mPoly 𝑅 ) )
Assertion esplyfval0 ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 0 ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 esplyfval0.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
2 esplyfval0.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
3 esplyfval0.0 ⊢ 𝑈 = ( 1r ‘ ( 𝐼 mPoly 𝑅 ) )
4 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
5 4 1 2 esplyval ⊢ ( 𝜑 → ( 𝐼 eSymPoly 𝑅 ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )
6 eqeq2 ⊢ ( 𝑘 = 0 → ( ( ♯ ‘ 𝑐 ) = 𝑘 ↔ ( ♯ ‘ 𝑐 ) = 0 ) )
7 6 rabbidv ⊢ ( 𝑘 = 0 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } = { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 0 } )
8 7 imaeq2d ⊢ ( 𝑘 = 0 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) = ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 0 } ) )
9 8 fveq2d ⊢ ( 𝑘 = 0 → ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) = ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) )
10 9 coeq2d ⊢ ( 𝑘 = 0 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) ) )
11 fvif ⊢ ( ( ℤRHom ‘ 𝑅 ) ‘ if ( 𝑓 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) = if ( 𝑓 = ( 𝐼 × { 0 } ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) )
12 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
13 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
14 12 13 zrh1 ⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = ( 1r ‘ 𝑅 ) )
15 2 14 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = ( 1r ‘ 𝑅 ) )
16 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
17 12 16 zrh0 ⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
18 2 17 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
19 15 18 ifeq12d ⊢ ( 𝜑 → if ( 𝑓 = ( 𝐼 × { 0 } ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) ) = if ( 𝑓 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → if ( 𝑓 = ( 𝐼 × { 0 } ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) ) = if ( 𝑓 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
21 11 20 eqtrid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( ℤRHom ‘ 𝑅 ) ‘ if ( 𝑓 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) = if ( 𝑓 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
22 21 mpteq2dva ⊢ ( 𝜑 → ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ if ( 𝑓 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑓 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
23 1zzd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 1 ∈ ℤ )
24 0zd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 0 ∈ ℤ )
25 23 24 ifcld ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → if ( 𝑓 = ( 𝐼 × { 0 } ) , 1 , 0 ) ∈ ℤ )
26 fveqeq2 ⊢ ( 𝑐 = ∅ → ( ( ♯ ‘ 𝑐 ) = 0 ↔ ( ♯ ‘ ∅ ) = 0 ) )
27 0elpw ⊢ ∅ ∈ 𝒫 𝐼
28 27 a1i ⊢ ( 𝜑 → ∅ ∈ 𝒫 𝐼 )
29 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
30 29 a1i ⊢ ( 𝜑 → ( ♯ ‘ ∅ ) = 0 )
31 hasheq0 ⊢ ( 𝑐 ∈ 𝒫 𝐼 → ( ( ♯ ‘ 𝑐 ) = 0 ↔ 𝑐 = ∅ ) )
32 31 biimpa ⊢ ( ( 𝑐 ∈ 𝒫 𝐼 ∧ ( ♯ ‘ 𝑐 ) = 0 ) → 𝑐 = ∅ )
33 32 adantll ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) ∧ ( ♯ ‘ 𝑐 ) = 0 ) → 𝑐 = ∅ )
34 26 28 30 33 rabeqsnd ⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 0 } = { ∅ } )
35 34 imaeq2d ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 0 } ) = ( ( 𝟭 ‘ 𝐼 ) “ { ∅ } ) )
36 indf1o ⊢ ( 𝐼 ∈ 𝑉 → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) )
37 f1of ⊢ ( ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
38 1 36 37 3syl ⊢ ( 𝜑 → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
39 38 ffnd ⊢ ( 𝜑 → ( 𝟭 ‘ 𝐼 ) Fn 𝒫 𝐼 )
40 39 28 fnimasnd ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { ∅ } ) = { ( ( 𝟭 ‘ 𝐼 ) ‘ ∅ ) } )
41 indconst0 ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝟭 ‘ 𝐼 ) ‘ ∅ ) = ( 𝐼 × { 0 } ) )
42 1 41 syl ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) ‘ ∅ ) = ( 𝐼 × { 0 } ) )
43 42 sneqd ⊢ ( 𝜑 → { ( ( 𝟭 ‘ 𝐼 ) ‘ ∅ ) } = { ( 𝐼 × { 0 } ) } )
44 35 40 43 3eqtrd ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 0 } ) = { ( 𝐼 × { 0 } ) } )
45 44 fveq2d ⊢ ( 𝜑 → ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) = ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ { ( 𝐼 × { 0 } ) } ) )
46 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
47 46 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V
48 breq1 ⊢ ( ℎ = ( 𝐼 × { 0 } ) → ( ℎ finSupp 0 ↔ ( 𝐼 × { 0 } ) finSupp 0 ) )
49 nn0ex ⊢ ℕ0 ∈ V
50 49 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
51 c0ex ⊢ 0 ∈ V
52 51 fconst ⊢ ( 𝐼 × { 0 } ) : 𝐼 ⟶ { 0 }
53 52 a1i ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) : 𝐼 ⟶ { 0 } )
54 0nn0 ⊢ 0 ∈ ℕ0
55 54 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
56 55 snssd ⊢ ( 𝜑 → { 0 } ⊆ ℕ0 )
57 53 56 fssd ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) : 𝐼 ⟶ ℕ0 )
58 50 1 57 elmapdd ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ ( ℕ0 ↑m 𝐼 ) )
59 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
60 1 59 fczfsuppd ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) finSupp 0 )
61 48 58 60 elrabd ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
62 indsn ⊢ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V ∧ ( 𝐼 × { 0 } ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ { ( 𝐼 × { 0 } ) } ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑓 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
63 47 61 62 sylancr ⊢ ( 𝜑 → ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ { ( 𝐼 × { 0 } ) } ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑓 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
64 45 63 eqtrd ⊢ ( 𝜑 → ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑓 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
65 12 zrhrhm ⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
66 zringbas ⊢ ℤ = ( Base ‘ ℤring )
67 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
68 66 67 rhmf ⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
69 2 65 68 3syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
70 69 feqmptd ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) = ( 𝑧 ∈ ℤ ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑧 ) ) )
71 fveq2 ⊢ ( 𝑧 = if ( 𝑓 = ( 𝐼 × { 0 } ) , 1 , 0 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑅 ) ‘ if ( 𝑓 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
72 25 64 70 71 fmptco ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ if ( 𝑓 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ) )
73 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
74 4 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
75 73 74 16 13 3 1 2 mpl1 ⊢ ( 𝜑 → 𝑈 = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑓 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
76 22 72 75 3eqtr4d ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) ) = 𝑈 )
77 10 76 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) = 𝑈 )
78 3 fvexi ⊢ 𝑈 ∈ V
79 78 a1i ⊢ ( 𝜑 → 𝑈 ∈ V )
80 5 77 55 79 fvmptd ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 0 ) = 𝑈 )