Theorem cnsrplycl

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

	Ref	Expression
Hypotheses	cnsrplycl.s	$$⊢\phi \to S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
	cnsrplycl.p	$$⊢\phi \to P\in \mathrm{Poly}\left(C\right)$$
	cnsrplycl.x	$$⊢\phi \to X\in S$$
	cnsrplycl.c	$$⊢\phi \to C\subseteq S$$
Assertion	cnsrplycl	$$⊢\phi \to P\left(X\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		cnsrplycl.s	$$⊢\phi \to S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
2		cnsrplycl.p	$$⊢\phi \to P\in \mathrm{Poly}\left(C\right)$$
3		cnsrplycl.x	$$⊢\phi \to X\in S$$
4		cnsrplycl.c	$$⊢\phi \to C\subseteq S$$
5		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
6	5	subrgss	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to S\subseteq ℂ$$
7	1 6	syl	$$⊢\phi \to S\subseteq ℂ$$
8		plyss	$$⊢\left(C\subseteq S\wedge S\subseteq ℂ\right)\to \mathrm{Poly}\left(C\right)\subseteq \mathrm{Poly}\left(S\right)$$
9	4 7 8	syl2anc	$$⊢\phi \to \mathrm{Poly}\left(C\right)\subseteq \mathrm{Poly}\left(S\right)$$
10	9 2	sseldd	$$⊢\phi \to P\in \mathrm{Poly}\left(S\right)$$
11	7 3	sseldd	$$⊢\phi \to X\in ℂ$$
12		eqid	$$⊢\mathrm{coeff}\left(P\right)=\mathrm{coeff}\left(P\right)$$
13		eqid	$$⊢\mathrm{deg}\left(P\right)=\mathrm{deg}\left(P\right)$$
14	12 13	coeid2	$$⊢\left(P\in \mathrm{Poly}\left(S\right)\wedge X\in ℂ\right)\to P\left(X\right)=\sum _{k=0}^{\mathrm{deg}\left(P\right)}\mathrm{coeff}\left(P\right)\left(k\right)X^k$$
15	10 11 14	syl2anc	$$⊢\phi \to P\left(X\right)=\sum _{k=0}^{\mathrm{deg}\left(P\right)}\mathrm{coeff}\left(P\right)\left(k\right)X^k$$
16		fzfid	$$⊢\phi \to \left(0\dots \mathrm{deg}\left(P\right)\right)\in \mathrm{Fin}$$
17	1	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots \mathrm{deg}\left(P\right)\right)\right)\to S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
18		subrgsubg	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to S\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
19		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
20	19	subg0cl	$$⊢S\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\to 0\in S$$
21	1 18 20	3syl	$$⊢\phi \to 0\in S$$
22	12	coef2	$$⊢\left(P\in \mathrm{Poly}\left(S\right)\wedge 0\in S\right)\to \mathrm{coeff}\left(P\right):{\mathbb{N}}_0⟶S$$
23	10 21 22	syl2anc	$$⊢\phi \to \mathrm{coeff}\left(P\right):{\mathbb{N}}_0⟶S$$
24	23	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots \mathrm{deg}\left(P\right)\right)\right)\to \mathrm{coeff}\left(P\right):{\mathbb{N}}_0⟶S$$
25		elfznn0	$$⊢k\in \left(0\dots \mathrm{deg}\left(P\right)\right)\to k\in {\mathbb{N}}_0$$
26	25	adantl	$$⊢\left(\phi \wedge k\in \left(0\dots \mathrm{deg}\left(P\right)\right)\right)\to k\in {\mathbb{N}}_0$$
27	24 26	ffvelcdmd	$$⊢\left(\phi \wedge k\in \left(0\dots \mathrm{deg}\left(P\right)\right)\right)\to \mathrm{coeff}\left(P\right)\left(k\right)\in S$$
28	3	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots \mathrm{deg}\left(P\right)\right)\right)\to X\in S$$
29	17 28 26	cnsrexpcl	$$⊢\left(\phi \wedge k\in \left(0\dots \mathrm{deg}\left(P\right)\right)\right)\to X^k\in S$$
30		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
31	30	subrgmcl	$$⊢\left(S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge \mathrm{coeff}\left(P\right)\left(k\right)\in S\wedge X^k\in S\right)\to \mathrm{coeff}\left(P\right)\left(k\right)X^k\in S$$
32	17 27 29 31	syl3anc	$$⊢\left(\phi \wedge k\in \left(0\dots \mathrm{deg}\left(P\right)\right)\right)\to \mathrm{coeff}\left(P\right)\left(k\right)X^k\in S$$
33	1 16 32	fsumcnsrcl	$$⊢\phi \to \sum _{k=0}^{\mathrm{deg}\left(P\right)}\mathrm{coeff}\left(P\right)\left(k\right)X^k\in S$$
34	15 33	eqeltrd	$$⊢\phi \to P\left(X\right)\in S$$