Metamath Proof Explorer

Theorem cnsrplycl

Description: Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014)

Ref Expression
Hypotheses cnsrplycl.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ ℂfld ) )
cnsrplycl.p ⊢ ( 𝜑 → 𝑃 ∈ ( Poly ‘ 𝐶 ) )
cnsrplycl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
cnsrplycl.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝑆 )
Assertion cnsrplycl ( 𝜑 → ( 𝑃 ‘ 𝑋 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 cnsrplycl.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ ℂfld ) )
2 cnsrplycl.p ⊢ ( 𝜑 → 𝑃 ∈ ( Poly ‘ 𝐶 ) )
3 cnsrplycl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
4 cnsrplycl.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝑆 )
5 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
6 5 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 ⊆ ℂ )
7 1 6 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
8 plyss ⊢ ( ( 𝐶 ⊆ 𝑆 ∧ 𝑆 ⊆ ℂ ) → ( Poly ‘ 𝐶 ) ⊆ ( Poly ‘ 𝑆 ) )
9 4 7 8 syl2anc ⊢ ( 𝜑 → ( Poly ‘ 𝐶 ) ⊆ ( Poly ‘ 𝑆 ) )
10 9 2 sseldd ⊢ ( 𝜑 → 𝑃 ∈ ( Poly ‘ 𝑆 ) )
11 7 3 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
12 eqid ⊢ ( coeff ‘ 𝑃 ) = ( coeff ‘ 𝑃 )
13 eqid ⊢ ( deg ‘ 𝑃 ) = ( deg ‘ 𝑃 )
14 12 13 coeid2 ⊢ ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → ( 𝑃 ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑃 ) ) ( ( ( coeff ‘ 𝑃 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
15 10 11 14 syl2anc ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑃 ) ) ( ( ( coeff ‘ 𝑃 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
16 fzfid ⊢ ( 𝜑 → ( 0 ... ( deg ‘ 𝑃 ) ) ∈ Fin )
17 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑃 ) ) ) → 𝑆 ∈ ( SubRing ‘ ℂfld ) )
18 subrgsubg ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 ∈ ( SubGrp ‘ ℂfld ) )
19 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
20 19 subg0cl ⊢ ( 𝑆 ∈ ( SubGrp ‘ ℂfld ) → 0 ∈ 𝑆 )
21 1 18 20 3syl ⊢ ( 𝜑 → 0 ∈ 𝑆 )
22 12 coef2 ⊢ ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ 𝑆 ) → ( coeff ‘ 𝑃 ) : ℕ0 ⟶ 𝑆 )
23 10 21 22 syl2anc ⊢ ( 𝜑 → ( coeff ‘ 𝑃 ) : ℕ0 ⟶ 𝑆 )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑃 ) ) ) → ( coeff ‘ 𝑃 ) : ℕ0 ⟶ 𝑆 )
25 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( deg ‘ 𝑃 ) ) → 𝑘 ∈ ℕ0 )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑃 ) ) ) → 𝑘 ∈ ℕ0 )
27 24 26 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑃 ) ) ) → ( ( coeff ‘ 𝑃 ) ‘ 𝑘 ) ∈ 𝑆 )
28 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑃 ) ) ) → 𝑋 ∈ 𝑆 )
29 17 28 26 cnsrexpcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑃 ) ) ) → ( 𝑋 ↑ 𝑘 ) ∈ 𝑆 )
30 cnfldmul ⊢ · = ( .r ‘ ℂfld )
31 30 subrgmcl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( ( coeff ‘ 𝑃 ) ‘ 𝑘 ) ∈ 𝑆 ∧ ( 𝑋 ↑ 𝑘 ) ∈ 𝑆 ) → ( ( ( coeff ‘ 𝑃 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ∈ 𝑆 )
32 17 27 29 31 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑃 ) ) ) → ( ( ( coeff ‘ 𝑃 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ∈ 𝑆 )
33 1 16 32 fsumcnsrcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑃 ) ) ( ( ( coeff ‘ 𝑃 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ∈ 𝑆 )
34 15 33 eqeltrd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) ∈ 𝑆 )