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 
|- ( ph -> S e. ( SubRing ` CCfld ) )
cnsrplycl.p 
|- ( ph -> P e. ( Poly ` C ) )
cnsrplycl.x 
|- ( ph -> X e. S )
cnsrplycl.c 
|- ( ph -> C C_ S )
Assertion cnsrplycl 
|- ( ph -> ( P ` X ) e. S )

Proof

Step Hyp Ref Expression
1 cnsrplycl.s 
 |-  ( ph -> S e. ( SubRing ` CCfld ) )
2 cnsrplycl.p 
 |-  ( ph -> P e. ( Poly ` C ) )
3 cnsrplycl.x 
 |-  ( ph -> X e. S )
4 cnsrplycl.c 
 |-  ( ph -> C C_ S )
5 cnfldbas 
 |-  CC = ( Base ` CCfld )
6 5 subrgss 
 |-  ( S e. ( SubRing ` CCfld ) -> S C_ CC )
7 1 6 syl 
 |-  ( ph -> S C_ CC )
8 plyss 
 |-  ( ( C C_ S /\ S C_ CC ) -> ( Poly ` C ) C_ ( Poly ` S ) )
9 4 7 8 syl2anc 
 |-  ( ph -> ( Poly ` C ) C_ ( Poly ` S ) )
10 9 2 sseldd 
 |-  ( ph -> P e. ( Poly ` S ) )
11 7 3 sseldd 
 |-  ( ph -> X e. CC )
12 eqid 
 |-  ( coeff ` P ) = ( coeff ` P )
13 eqid 
 |-  ( deg ` P ) = ( deg ` P )
14 12 13 coeid2 
 |-  ( ( P e. ( Poly ` S ) /\ X e. CC ) -> ( P ` X ) = sum_ k e. ( 0 ... ( deg ` P ) ) ( ( ( coeff ` P ) ` k ) x. ( X ^ k ) ) )
15 10 11 14 syl2anc 
 |-  ( ph -> ( P ` X ) = sum_ k e. ( 0 ... ( deg ` P ) ) ( ( ( coeff ` P ) ` k ) x. ( X ^ k ) ) )
16 fzfid 
 |-  ( ph -> ( 0 ... ( deg ` P ) ) e. Fin )
17 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( deg ` P ) ) ) -> S e. ( SubRing ` CCfld ) )
18 subrgsubg 
 |-  ( S e. ( SubRing ` CCfld ) -> S e. ( SubGrp ` CCfld ) )
19 cnfld0 
 |-  0 = ( 0g ` CCfld )
20 19 subg0cl 
 |-  ( S e. ( SubGrp ` CCfld ) -> 0 e. S )
21 1 18 20 3syl 
 |-  ( ph -> 0 e. S )
22 12 coef2 
 |-  ( ( P e. ( Poly ` S ) /\ 0 e. S ) -> ( coeff ` P ) : NN0 --> S )
23 10 21 22 syl2anc 
 |-  ( ph -> ( coeff ` P ) : NN0 --> S )
24 23 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( deg ` P ) ) ) -> ( coeff ` P ) : NN0 --> S )
25 elfznn0 
 |-  ( k e. ( 0 ... ( deg ` P ) ) -> k e. NN0 )
26 25 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( deg ` P ) ) ) -> k e. NN0 )
27 24 26 ffvelrnd 
 |-  ( ( ph /\ k e. ( 0 ... ( deg ` P ) ) ) -> ( ( coeff ` P ) ` k ) e. S )
28 3 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( deg ` P ) ) ) -> X e. S )
29 17 28 26 cnsrexpcl 
 |-  ( ( ph /\ k e. ( 0 ... ( deg ` P ) ) ) -> ( X ^ k ) e. S )
30 cnfldmul 
 |-  x. = ( .r ` CCfld )
31 30 subrgmcl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( ( coeff ` P ) ` k ) e. S /\ ( X ^ k ) e. S ) -> ( ( ( coeff ` P ) ` k ) x. ( X ^ k ) ) e. S )
32 17 27 29 31 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... ( deg ` P ) ) ) -> ( ( ( coeff ` P ) ` k ) x. ( X ^ k ) ) e. S )
33 1 16 32 fsumcnsrcl 
 |-  ( ph -> sum_ k e. ( 0 ... ( deg ` P ) ) ( ( ( coeff ` P ) ` k ) x. ( X ^ k ) ) e. S )
34 15 33 eqeltrd 
 |-  ( ph -> ( P ` X ) e. S )