Theorem plypf1 23968

Description: Write the set of complex polynomials in a subring in terms of the abstract polynomial construction. (Contributed by Mario Carneiro, 3-Jul-2015.) (Proof shortened by AV, 29-Sep-2019.)

Hypotheses

Ref	Expression
plypf1.r	|- R = (ℂfld ↾s S )
plypf1.p	|- P = (Poly1 ` R )
plypf1.a	|- A = ( Base ` P )
plypf1.e	|- E = (eval1 ` ℂfld )

Assertion

Ref	Expression
plypf1	|- ( S e. (SubRing ` ℂfld ) -> (Poly ` S ) = ( E " A ) )

Proof of Theorem plypf1

Dummy variables f a k n x z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elply 23951	. . . . 5 |- ( f e. (Poly ` S ) <-> ( S C_ CC /\ E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
2	1	simprbi 480	. . . 4 |- ( f e. (Poly ` S ) -> E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
3		eqid 2622	. . . . . . . . 9 |- (ℂfld ^s CC ) = (ℂfld ^s CC )
4		cnfldbas 19750	. . . . . . . . 9 |- CC = ( Base ` ℂfld )
5		eqid 2622	. . . . . . . . 9 |- ( 0g ` (ℂfld ^s CC ) ) = ( 0g ` (ℂfld ^s CC ) )
6		cnex 10017	. . . . . . . . . 10 |- CC e. _V
7	6	a1i 11	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> CC e. _V )
8		fzfid 12772	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( 0 ... n ) e. Fin )
9		cnring 19768	. . . . . . . . . 10 |- ℂfld e. Ring
10		ringcmn 18581	. . . . . . . . . 10 |- (ℂfld e. Ring -> ℂfld e. CMnd )
11	9, 10	mp1i 13	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ℂfld e. CMnd )
12	4	subrgss 18781	. . . . . . . . . . . . 13 |- ( S e. (SubRing ` ℂfld ) -> S C_ CC )
13	12	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> S C_ CC )
14		elmapi 7879	. . . . . . . . . . . . . . 15 |- ( a e. ( ( S u. { 0 } ) ^m NN0 ) -> a : NN0 --> ( S u. { 0 } ) )
15	14	ad2antll 765	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> a : NN0 --> ( S u. { 0 } ) )
16		subrgsubg 18786	. . . . . . . . . . . . . . . . . . 19 |- ( S e. (SubRing ` ℂfld ) -> S e. (SubGrp ` ℂfld ) )
17		cnfld0 19770	. . . . . . . . . . . . . . . . . . . 20 |- 0 = ( 0g ` ℂfld )
18	17	subg0cl 17602	. . . . . . . . . . . . . . . . . . 19 |- ( S e. (SubGrp ` ℂfld ) -> 0 e. S )
19	16, 18	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( S e. (SubRing ` ℂfld ) -> 0 e. S )
20	19	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> 0 e. S )
21	20	snssd 4340	. . . . . . . . . . . . . . . 16 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> { 0 } C_ S )
22		ssequn2 3786	. . . . . . . . . . . . . . . 16 |- ( { 0 } C_ S <-> ( S u. { 0 } ) = S )
23	21, 22	sylib 208	. . . . . . . . . . . . . . 15 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( S u. { 0 } ) = S )
24	23	feq3d 6032	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( a : NN0 --> ( S u. { 0 } ) <-> a : NN0 --> S ) )
25	15, 24	mpbid 222	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> a : NN0 --> S )
26		elfznn0 12433	. . . . . . . . . . . . 13 |- ( k e. ( 0 ... n ) -> k e. NN0 )
27		ffvelrn 6357	. . . . . . . . . . . . 13 |- ( ( a : NN0 --> S /\ k e. NN0 ) -> ( a ` k ) e. S )
28	25, 26, 27	syl2an 494	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( a ` k ) e. S )
29	13, 28	sseldd 3604	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( a ` k ) e. CC )
30	29	adantrl 752	. . . . . . . . . 10 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( z e. CC /\ k e. ( 0 ... n ) ) ) -> ( a ` k ) e. CC )
31		simprl 794	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( z e. CC /\ k e. ( 0 ... n ) ) ) -> z e. CC )
32	26	ad2antll 765	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( z e. CC /\ k e. ( 0 ... n ) ) ) -> k e. NN0 )
33		expcl 12878	. . . . . . . . . . 11 |- ( ( z e. CC /\ k e. NN0 ) -> ( z ^ k ) e. CC )
34	31, 32, 33	syl2anc 693	. . . . . . . . . 10 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( z e. CC /\ k e. ( 0 ... n ) ) ) -> ( z ^ k ) e. CC )
35	30, 34	mulcld 10060	. . . . . . . . 9 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( z e. CC /\ k e. ( 0 ... n ) ) ) -> ( ( a ` k ) x. ( z ^ k ) ) e. CC )
36		eqid 2622	. . . . . . . . . 10 |- ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) = ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) )
37	6	mptex 6486	. . . . . . . . . . 11 |- ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) e. _V
38	37	a1i 11	. . . . . . . . . 10 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) e. _V )
39		fvex 6201	. . . . . . . . . . 11 |- ( 0g ` (ℂfld ^s CC ) ) e. _V
40	39	a1i 11	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( 0g ` (ℂfld ^s CC ) ) e. _V )
41	36, 8, 38, 40	fsuppmptdm 8286	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) finSupp ( 0g ` (ℂfld ^s CC ) ) )
42	3, 4, 5, 7, 8, 11, 35, 41	pwsgsum 18378	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( (ℂfld ^s CC ) gsumg ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) ) = ( z e. CC |-> (ℂfld gsumg ( k e. ( 0 ... n ) |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )
43		fzfid 12772	. . . . . . . . . 10 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) -> ( 0 ... n ) e. Fin )
44	35	anassrs 680	. . . . . . . . . 10 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) /\ k e. ( 0 ... n ) ) -> ( ( a ` k ) x. ( z ^ k ) ) e. CC )
45	43, 44	gsumfsum 19813	. . . . . . . . 9 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) -> (ℂfld gsumg ( k e. ( 0 ... n ) |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) = sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
46	45	mpteq2dva 4744	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( z e. CC |-> (ℂfld gsumg ( k e. ( 0 ... n ) |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
47	42, 46	eqtrd 2656	. . . . . . 7 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( (ℂfld ^s CC ) gsumg ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
48	3	pwsring 18615	. . . . . . . . . 10 |- ( (ℂfld e. Ring /\ CC e. _V ) -> (ℂfld ^s CC ) e. Ring )
49	9, 6, 48	mp2an 708	. . . . . . . . 9 |- (ℂfld ^s CC ) e. Ring
50		ringcmn 18581	. . . . . . . . 9 |- ( (ℂfld ^s CC ) e. Ring -> (ℂfld ^s CC ) e. CMnd )
51	49, 50	mp1i 13	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> (ℂfld ^s CC ) e. CMnd )
52		cncrng 19767	. . . . . . . . . . 11 |- ℂfld e. CRing
53		plypf1.e	. . . . . . . . . . . 12 |- E = (eval1 ` ℂfld )
54		eqid 2622	. . . . . . . . . . . 12 |- (Poly1 ` ℂfld ) = (Poly1 ` ℂfld )
55	53, 54, 3, 4	evl1rhm 19696	. . . . . . . . . . 11 |- (ℂfld e. CRing -> E e. ( (Poly1 ` ℂfld ) RingHom (ℂfld ^s CC ) ) )
56	52, 55	ax-mp 5	. . . . . . . . . 10 |- E e. ( (Poly1 ` ℂfld ) RingHom (ℂfld ^s CC ) )
57		plypf1.r	. . . . . . . . . . . 12 |- R = (ℂfld ↾s S )
58		plypf1.p	. . . . . . . . . . . 12 |- P = (Poly1 ` R )
59		plypf1.a	. . . . . . . . . . . 12 |- A = ( Base ` P )
60	54, 57, 58, 59	subrgply1 19603	. . . . . . . . . . 11 |- ( S e. (SubRing ` ℂfld ) -> A e. (SubRing ` (Poly1 ` ℂfld ) ) )
61	60	adantr 481	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> A e. (SubRing ` (Poly1 ` ℂfld ) ) )
62		rhmima 18811	. . . . . . . . . 10 |- ( ( E e. ( (Poly1 ` ℂfld ) RingHom (ℂfld ^s CC ) ) /\ A e. (SubRing ` (Poly1 ` ℂfld ) ) ) -> ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) )
63	56, 61, 62	sylancr 695	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) )
64		subrgsubg 18786	. . . . . . . . 9 |- ( ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) -> ( E " A ) e. (SubGrp ` (ℂfld ^s CC ) ) )
65		subgsubm 17616	. . . . . . . . 9 |- ( ( E " A ) e. (SubGrp ` (ℂfld ^s CC ) ) -> ( E " A ) e. (SubMnd ` (ℂfld ^s CC ) ) )
66	63, 64, 65	3syl 18	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( E " A ) e. (SubMnd ` (ℂfld ^s CC ) ) )
67		eqid 2622	. . . . . . . . . . . 12 |- ( Base ` (ℂfld ^s CC ) ) = ( Base ` (ℂfld ^s CC ) )
68	9	a1i 11	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ℂfld e. Ring )
69	6	a1i 11	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> CC e. _V )
70		fconst6g 6094	. . . . . . . . . . . . . 14 |- ( ( a ` k ) e. CC -> ( CC X. { ( a ` k ) } ) : CC --> CC )
71	29, 70	syl 17	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( CC X. { ( a ` k ) } ) : CC --> CC )
72	3, 4, 67	pwselbasb 16148	. . . . . . . . . . . . . 14 |- ( (ℂfld e. Ring /\ CC e. _V ) -> ( ( CC X. { ( a ` k ) } ) e. ( Base ` (ℂfld ^s CC ) ) <-> ( CC X. { ( a ` k ) } ) : CC --> CC ) )
73	9, 6, 72	mp2an 708	. . . . . . . . . . . . 13 |- ( ( CC X. { ( a ` k ) } ) e. ( Base ` (ℂfld ^s CC ) ) <-> ( CC X. { ( a ` k ) } ) : CC --> CC )
74	71, 73	sylibr 224	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( CC X. { ( a ` k ) } ) e. ( Base ` (ℂfld ^s CC ) ) )
75	34	anass1rs 849	. . . . . . . . . . . . . 14 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( z ^ k ) e. CC )
76		eqid 2622	. . . . . . . . . . . . . 14 |- ( z e. CC |-> ( z ^ k ) ) = ( z e. CC |-> ( z ^ k ) )
77	75, 76	fmptd 6385	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( z ^ k ) ) : CC --> CC )
78	3, 4, 67	pwselbasb 16148	. . . . . . . . . . . . . 14 |- ( (ℂfld e. Ring /\ CC e. _V ) -> ( ( z e. CC |-> ( z ^ k ) ) e. ( Base ` (ℂfld ^s CC ) ) <-> ( z e. CC |-> ( z ^ k ) ) : CC --> CC ) )
79	9, 6, 78	mp2an 708	. . . . . . . . . . . . 13 |- ( ( z e. CC |-> ( z ^ k ) ) e. ( Base ` (ℂfld ^s CC ) ) <-> ( z e. CC |-> ( z ^ k ) ) : CC --> CC )
80	77, 79	sylibr 224	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( z ^ k ) ) e. ( Base ` (ℂfld ^s CC ) ) )
81		cnfldmul 19752	. . . . . . . . . . . 12 |- x. = ( .r ` ℂfld )
82		eqid 2622	. . . . . . . . . . . 12 |- ( .r ` (ℂfld ^s CC ) ) = ( .r ` (ℂfld ^s CC ) )
83	3, 67, 68, 69, 74, 80, 81, 82	pwsmulrval 16151	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( CC X. { ( a ` k ) } ) ( .r ` (ℂfld ^s CC ) ) ( z e. CC |-> ( z ^ k ) ) ) = ( ( CC X. { ( a ` k ) } ) oF x. ( z e. CC |-> ( z ^ k ) ) ) )
84	29	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( a ` k ) e. CC )
85		fconstmpt 5163	. . . . . . . . . . . . 13 |- ( CC X. { ( a ` k ) } ) = ( z e. CC |-> ( a ` k ) )
86	85	a1i 11	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( CC X. { ( a ` k ) } ) = ( z e. CC |-> ( a ` k ) ) )
87		eqidd 2623	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( z ^ k ) ) = ( z e. CC |-> ( z ^ k ) ) )
88	69, 84, 75, 86, 87	offval2 6914	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( CC X. { ( a ` k ) } ) oF x. ( z e. CC |-> ( z ^ k ) ) ) = ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) )
89	83, 88	eqtrd 2656	. . . . . . . . . 10 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( CC X. { ( a ` k ) } ) ( .r ` (ℂfld ^s CC ) ) ( z e. CC |-> ( z ^ k ) ) ) = ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) )
90	63	adantr 481	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) )
91		eqid 2622	. . . . . . . . . . . . . 14 |- (algSc ` (Poly1 ` ℂfld ) ) = (algSc ` (Poly1 ` ℂfld ) )
92	53, 54, 4, 91	evl1sca 19698	. . . . . . . . . . . . 13 |- ( (ℂfld e. CRing /\ ( a ` k ) e. CC ) -> ( E ` ( (algSc ` (Poly1 ` ℂfld ) ) ` ( a ` k ) ) ) = ( CC X. { ( a ` k ) } ) )
93	52, 29, 92	sylancr 695	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( (algSc ` (Poly1 ` ℂfld ) ) ` ( a ` k ) ) ) = ( CC X. { ( a ` k ) } ) )
94		eqid 2622	. . . . . . . . . . . . . . . 16 |- ( Base ` (Poly1 ` ℂfld ) ) = ( Base ` (Poly1 ` ℂfld ) )
95	94, 67	rhmf 18726	. . . . . . . . . . . . . . 15 |- ( E e. ( (Poly1 ` ℂfld ) RingHom (ℂfld ^s CC ) ) -> E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) )
96	56, 95	ax-mp 5	. . . . . . . . . . . . . 14 |- E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) )
97		ffn 6045	. . . . . . . . . . . . . 14 |- ( E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) -> E Fn ( Base ` (Poly1 ` ℂfld ) ) )
98	96, 97	mp1i 13	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> E Fn ( Base ` (Poly1 ` ℂfld ) ) )
99	94	subrgss 18781	. . . . . . . . . . . . . . 15 |- ( A e. (SubRing ` (Poly1 ` ℂfld ) ) -> A C_ ( Base ` (Poly1 ` ℂfld ) ) )
100	60, 99	syl 17	. . . . . . . . . . . . . 14 |- ( S e. (SubRing ` ℂfld ) -> A C_ ( Base ` (Poly1 ` ℂfld ) ) )
101	100	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> A C_ ( Base ` (Poly1 ` ℂfld ) ) )
102		simpll 790	. . . . . . . . . . . . . . 15 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> S e. (SubRing ` ℂfld ) )
103	54, 91, 57, 58, 102, 59, 4, 29	subrg1asclcl 19630	. . . . . . . . . . . . . 14 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( (algSc ` (Poly1 ` ℂfld ) ) ` ( a ` k ) ) e. A <-> ( a ` k ) e. S ) )
104	28, 103	mpbird 247	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( (algSc ` (Poly1 ` ℂfld ) ) ` ( a ` k ) ) e. A )
105		fnfvima 6496	. . . . . . . . . . . . 13 |- ( ( E Fn ( Base ` (Poly1 ` ℂfld ) ) /\ A C_ ( Base ` (Poly1 ` ℂfld ) ) /\ ( (algSc ` (Poly1 ` ℂfld ) ) ` ( a ` k ) ) e. A ) -> ( E ` ( (algSc ` (Poly1 ` ℂfld ) ) ` ( a ` k ) ) ) e. ( E " A ) )
106	98, 101, 104, 105	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( (algSc ` (Poly1 ` ℂfld ) ) ` ( a ` k ) ) ) e. ( E " A ) )
107	93, 106	eqeltrrd 2702	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( CC X. { ( a ` k ) } ) e. ( E " A ) )
108	67	subrgss 18781	. . . . . . . . . . . . . . . . 17 |- ( ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) -> ( E " A ) C_ ( Base ` (ℂfld ^s CC ) ) )
109	90, 108	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E " A ) C_ ( Base ` (ℂfld ^s CC ) ) )
110	60	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> A e. (SubRing ` (Poly1 ` ℂfld ) ) )
111		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 |- (mulGrp ` (Poly1 ` ℂfld ) ) = (mulGrp ` (Poly1 ` ℂfld ) )
112	111	subrgsubm 18793	. . . . . . . . . . . . . . . . . . 19 |- ( A e. (SubRing ` (Poly1 ` ℂfld ) ) -> A e. (SubMnd ` (mulGrp ` (Poly1 ` ℂfld ) ) ) )
113	110, 112	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> A e. (SubMnd ` (mulGrp ` (Poly1 ` ℂfld ) ) ) )
114	26	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> k e. NN0 )
115		eqid 2622	. . . . . . . . . . . . . . . . . . 19 |- (var1 ` ℂfld ) = (var1 ` ℂfld )
116	115, 102, 57, 58, 59	subrgvr1cl 19632	. . . . . . . . . . . . . . . . . 18 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> (var1 ` ℂfld ) e. A )
117		eqid 2622	. . . . . . . . . . . . . . . . . . 19 |- (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) = (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) )
118	117	submmulgcl 17585	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. (SubMnd ` (mulGrp ` (Poly1 ` ℂfld ) ) ) /\ k e. NN0 /\ (var1 ` ℂfld ) e. A ) -> ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. A )
119	113, 114, 116, 118	syl3anc 1326	. . . . . . . . . . . . . . . . 17 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. A )
120		fnfvima 6496	. . . . . . . . . . . . . . . . 17 |- ( ( E Fn ( Base ` (Poly1 ` ℂfld ) ) /\ A C_ ( Base ` (Poly1 ` ℂfld ) ) /\ ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. A ) -> ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) e. ( E " A ) )
121	98, 101, 119, 120	syl3anc 1326	. . . . . . . . . . . . . . . 16 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) e. ( E " A ) )
122	109, 121	sseldd 3604	. . . . . . . . . . . . . . 15 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) e. ( Base ` (ℂfld ^s CC ) ) )
123	3, 4, 67, 68, 69, 122	pwselbas 16149	. . . . . . . . . . . . . 14 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) : CC --> CC )
124	123	feqmptd 6249	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) = ( z e. CC |-> ( ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ` z ) ) )
125	52	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ℂfld e. CRing )
126		simpr 477	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> z e. CC )
127	53, 115, 4, 54, 94, 125, 126	evl1vard 19701	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( (var1 ` ℂfld ) e. ( Base ` (Poly1 ` ℂfld ) ) /\ ( ( E ` (var1 ` ℂfld ) ) ` z ) = z ) )
128		eqid 2622	. . . . . . . . . . . . . . . . 17 |- (.g ` (mulGrp ` ℂfld ) ) = (.g ` (mulGrp ` ℂfld ) )
129	114	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> k e. NN0 )
130	53, 54, 4, 94, 125, 126, 127, 117, 128, 129	evl1expd 19709	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. ( Base ` (Poly1 ` ℂfld ) ) /\ ( ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ` z ) = ( k (.g ` (mulGrp ` ℂfld ) ) z ) ) )
131	130	simprd 479	. . . . . . . . . . . . . . 15 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ` z ) = ( k (.g ` (mulGrp ` ℂfld ) ) z ) )
132		cnfldexp 19779	. . . . . . . . . . . . . . . 16 |- ( ( z e. CC /\ k e. NN0 ) -> ( k (.g ` (mulGrp ` ℂfld ) ) z ) = ( z ^ k ) )
133	126, 129, 132	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( k (.g ` (mulGrp ` ℂfld ) ) z ) = ( z ^ k ) )
134	131, 133	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ` z ) = ( z ^ k ) )
135	134	mpteq2dva 4744	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ` z ) ) = ( z e. CC |-> ( z ^ k ) ) )
136	124, 135	eqtrd 2656	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) = ( z e. CC |-> ( z ^ k ) ) )
137	136, 121	eqeltrrd 2702	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( z ^ k ) ) e. ( E " A ) )
138	82	subrgmcl 18792	. . . . . . . . . . 11 |- ( ( ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) /\ ( CC X. { ( a ` k ) } ) e. ( E " A ) /\ ( z e. CC |-> ( z ^ k ) ) e. ( E " A ) ) -> ( ( CC X. { ( a ` k ) } ) ( .r ` (ℂfld ^s CC ) ) ( z e. CC |-> ( z ^ k ) ) ) e. ( E " A ) )
139	90, 107, 137, 138	syl3anc 1326	. . . . . . . . . 10 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( CC X. { ( a ` k ) } ) ( .r ` (ℂfld ^s CC ) ) ( z e. CC |-> ( z ^ k ) ) ) e. ( E " A ) )
140	89, 139	eqeltrrd 2702	. . . . . . . . 9 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) e. ( E " A ) )
141	140, 36	fmptd 6385	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) : ( 0 ... n ) --> ( E " A ) )
142	36, 8, 140, 40	fsuppmptdm 8286	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) finSupp ( 0g ` (ℂfld ^s CC ) ) )
143	5, 51, 8, 66, 141, 142	gsumsubmcl 18319	. . . . . . 7 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( (ℂfld ^s CC ) gsumg ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) ) e. ( E " A ) )
144	47, 143	eqeltrrd 2702	. . . . . 6 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) e. ( E " A ) )
145		eleq1 2689	. . . . . 6 |- ( f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) -> ( f e. ( E " A ) <-> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) e. ( E " A ) ) )
146	144, 145	syl5ibrcom 237	. . . . 5 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) -> f e. ( E " A ) ) )
147	146	rexlimdvva 3038	. . . 4 |- ( S e. (SubRing ` ℂfld ) -> ( E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) -> f e. ( E " A ) ) )
148	2, 147	syl5 34	. . 3 |- ( S e. (SubRing ` ℂfld ) -> ( f e. (Poly ` S ) -> f e. ( E " A ) ) )
149		ffun 6048	. . . . . 6 |- ( E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) -> Fun E )
150	96, 149	ax-mp 5	. . . . 5 |- Fun E
151		fvelima 6248	. . . . 5 |- ( ( Fun E /\ f e. ( E " A ) ) -> E. a e. A ( E ` a ) = f )
152	150, 151	mpan 706	. . . 4 |- ( f e. ( E " A ) -> E. a e. A ( E ` a ) = f )
153	100	sselda 3603	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> a e. ( Base ` (Poly1 ` ℂfld ) ) )
154		eqid 2622	. . . . . . . . . . . 12 |- ( .s ` (Poly1 ` ℂfld ) ) = ( .s ` (Poly1 ` ℂfld ) )
155		eqid 2622	. . . . . . . . . . . 12 |- (coe1 ` a ) = (coe1 ` a )
156	54, 115, 94, 154, 111, 117, 155	ply1coe 19666	. . . . . . . . . . 11 |- ( (ℂfld e. Ring /\ a e. ( Base ` (Poly1 ` ℂfld ) ) ) -> a = ( (Poly1 ` ℂfld ) gsumg ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ) )
157	9, 153, 156	sylancr 695	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> a = ( (Poly1 ` ℂfld ) gsumg ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ) )
158	157	fveq2d 6195	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( E ` a ) = ( E ` ( (Poly1 ` ℂfld ) gsumg ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ) ) )
159		eqid 2622	. . . . . . . . . 10 |- ( 0g ` (Poly1 ` ℂfld ) ) = ( 0g ` (Poly1 ` ℂfld ) )
160	54	ply1ring 19618	. . . . . . . . . . . 12 |- (ℂfld e. Ring -> (Poly1 ` ℂfld ) e. Ring )
161	9, 160	ax-mp 5	. . . . . . . . . . 11 |- (Poly1 ` ℂfld ) e. Ring
162		ringcmn 18581	. . . . . . . . . . 11 |- ( (Poly1 ` ℂfld ) e. Ring -> (Poly1 ` ℂfld ) e. CMnd )
163	161, 162	mp1i 13	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (Poly1 ` ℂfld ) e. CMnd )
164		ringmnd 18556	. . . . . . . . . . 11 |- ( (ℂfld ^s CC ) e. Ring -> (ℂfld ^s CC ) e. Mnd )
165	49, 164	mp1i 13	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (ℂfld ^s CC ) e. Mnd )
166		nn0ex 11298	. . . . . . . . . . 11 |- NN0 e. _V
167	166	a1i 11	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> NN0 e. _V )
168		rhmghm 18725	. . . . . . . . . . . 12 |- ( E e. ( (Poly1 ` ℂfld ) RingHom (ℂfld ^s CC ) ) -> E e. ( (Poly1 ` ℂfld ) GrpHom (ℂfld ^s CC ) ) )
169	56, 168	ax-mp 5	. . . . . . . . . . 11 |- E e. ( (Poly1 ` ℂfld ) GrpHom (ℂfld ^s CC ) )
170		ghmmhm 17670	. . . . . . . . . . 11 |- ( E e. ( (Poly1 ` ℂfld ) GrpHom (ℂfld ^s CC ) ) -> E e. ( (Poly1 ` ℂfld ) MndHom (ℂfld ^s CC ) ) )
171	169, 170	mp1i 13	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> E e. ( (Poly1 ` ℂfld ) MndHom (ℂfld ^s CC ) ) )
172	54	ply1lmod 19622	. . . . . . . . . . . . 13 |- (ℂfld e. Ring -> (Poly1 ` ℂfld ) e. LMod )
173	9, 172	mp1i 13	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> (Poly1 ` ℂfld ) e. LMod )
174	12	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> S C_ CC )
175		eqid 2622	. . . . . . . . . . . . . . . . 17 |- ( Base ` R ) = ( Base ` R )
176	155, 59, 58, 175	coe1f 19581	. . . . . . . . . . . . . . . 16 |- ( a e. A -> (coe1 ` a ) : NN0 --> ( Base ` R ) )
177	57	subrgbas 18789	. . . . . . . . . . . . . . . . 17 |- ( S e. (SubRing ` ℂfld ) -> S = ( Base ` R ) )
178	177	feq3d 6032	. . . . . . . . . . . . . . . 16 |- ( S e. (SubRing ` ℂfld ) -> ( (coe1 ` a ) : NN0 --> S <-> (coe1 ` a ) : NN0 --> ( Base ` R ) ) )
179	176, 178	syl5ibr 236	. . . . . . . . . . . . . . 15 |- ( S e. (SubRing ` ℂfld ) -> ( a e. A -> (coe1 ` a ) : NN0 --> S ) )
180	179	imp 445	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) : NN0 --> S )
181	180	ffvelrnda 6359	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. S )
182	174, 181	sseldd 3604	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. CC )
183	111	ringmgp 18553	. . . . . . . . . . . . . 14 |- ( (Poly1 ` ℂfld ) e. Ring -> (mulGrp ` (Poly1 ` ℂfld ) ) e. Mnd )
184	161, 183	mp1i 13	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> (mulGrp ` (Poly1 ` ℂfld ) ) e. Mnd )
185		simpr 477	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> k e. NN0 )
186	115, 54, 94	vr1cl 19587	. . . . . . . . . . . . . 14 |- (ℂfld e. Ring -> (var1 ` ℂfld ) e. ( Base ` (Poly1 ` ℂfld ) ) )
187	9, 186	mp1i 13	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> (var1 ` ℂfld ) e. ( Base ` (Poly1 ` ℂfld ) ) )
188	111, 94	mgpbas 18495	. . . . . . . . . . . . . 14 |- ( Base ` (Poly1 ` ℂfld ) ) = ( Base ` (mulGrp ` (Poly1 ` ℂfld ) ) )
189	188, 117	mulgnn0cl 17558	. . . . . . . . . . . . 13 |- ( ( (mulGrp ` (Poly1 ` ℂfld ) ) e. Mnd /\ k e. NN0 /\ (var1 ` ℂfld ) e. ( Base ` (Poly1 ` ℂfld ) ) ) -> ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. ( Base ` (Poly1 ` ℂfld ) ) )
190	184, 185, 187, 189	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. ( Base ` (Poly1 ` ℂfld ) ) )
191	54	ply1sca 19623	. . . . . . . . . . . . . 14 |- (ℂfld e. Ring -> ℂfld = (Scalar ` (Poly1 ` ℂfld ) ) )
192	9, 191	ax-mp 5	. . . . . . . . . . . . 13 |- ℂfld = (Scalar ` (Poly1 ` ℂfld ) )
193	94, 192, 154, 4	lmodvscl 18880	. . . . . . . . . . . 12 |- ( ( (Poly1 ` ℂfld ) e. LMod /\ ( (coe1 ` a ) ` k ) e. CC /\ ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. ( Base ` (Poly1 ` ℂfld ) ) ) -> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) e. ( Base ` (Poly1 ` ℂfld ) ) )
194	173, 182, 190, 193	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) e. ( Base ` (Poly1 ` ℂfld ) ) )
195		eqid 2622	. . . . . . . . . . 11 |- ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) = ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) )
196	194, 195	fmptd 6385	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) : NN0 --> ( Base ` (Poly1 ` ℂfld ) ) )
197	166	mptex 6486	. . . . . . . . . . . . 13 |- ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) e. _V
198		funmpt 5926	. . . . . . . . . . . . 13 |- Fun ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) )
199		fvex 6201	. . . . . . . . . . . . 13 |- ( 0g ` (Poly1 ` ℂfld ) ) e. _V
200	197, 198, 199	3pm3.2i 1239	. . . . . . . . . . . 12 |- ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) /\ ( 0g ` (Poly1 ` ℂfld ) ) e. _V )
201	200	a1i 11	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) /\ ( 0g ` (Poly1 ` ℂfld ) ) e. _V ) )
202	155, 94, 54, 17	coe1sfi 19583	. . . . . . . . . . . . 13 |- ( a e. ( Base ` (Poly1 ` ℂfld ) ) -> (coe1 ` a ) finSupp 0 )
203	153, 202	syl 17	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) finSupp 0 )
204	203	fsuppimpd 8282	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (coe1 ` a ) supp 0 ) e. Fin )
205	180	feqmptd 6249	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) = ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) )
206	205	oveq1d 6665	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (coe1 ` a ) supp 0 ) = ( ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) supp 0 ) )
207		eqimss2 3658	. . . . . . . . . . . . 13 |- ( ( (coe1 ` a ) supp 0 ) = ( ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) supp 0 ) -> ( ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) supp 0 ) C_ ( (coe1 ` a ) supp 0 ) )
208	206, 207	syl 17	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) supp 0 ) C_ ( (coe1 ` a ) supp 0 ) )
209	9, 172	mp1i 13	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (Poly1 ` ℂfld ) e. LMod )
210	94, 192, 154, 17, 159	lmod0vs 18896	. . . . . . . . . . . . 13 |- ( ( (Poly1 ` ℂfld ) e. LMod /\ x e. ( Base ` (Poly1 ` ℂfld ) ) ) -> ( 0 ( .s ` (Poly1 ` ℂfld ) ) x ) = ( 0g ` (Poly1 ` ℂfld ) ) )
211	209, 210	sylan 488	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ x e. ( Base ` (Poly1 ` ℂfld ) ) ) -> ( 0 ( .s ` (Poly1 ` ℂfld ) ) x ) = ( 0g ` (Poly1 ` ℂfld ) ) )
212		c0ex 10034	. . . . . . . . . . . . 13 |- 0 e. _V
213	212	a1i 11	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> 0 e. _V )
214	208, 211, 181, 190, 213	suppssov1 7327	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) supp ( 0g ` (Poly1 ` ℂfld ) ) ) C_ ( (coe1 ` a ) supp 0 ) )
215		suppssfifsupp 8290	. . . . . . . . . . 11 |- ( ( ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) /\ ( 0g ` (Poly1 ` ℂfld ) ) e. _V ) /\ ( ( (coe1 ` a ) supp 0 ) e. Fin /\ ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) supp ( 0g ` (Poly1 ` ℂfld ) ) ) C_ ( (coe1 ` a ) supp 0 ) ) ) -> ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) finSupp ( 0g ` (Poly1 ` ℂfld ) ) )
216	201, 204, 214, 215	syl12anc 1324	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) finSupp ( 0g ` (Poly1 ` ℂfld ) ) )
217	94, 159, 163, 165, 167, 171, 196, 216	gsummhm 18338	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (ℂfld ^s CC ) gsumg ( E o. ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ) ) = ( E ` ( (Poly1 ` ℂfld ) gsumg ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ) ) )
218		eqidd 2623	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) = ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) )
219	96	a1i 11	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) )
220	219	feqmptd 6249	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> E = ( x e. ( Base ` (Poly1 ` ℂfld ) ) |-> ( E ` x ) ) )
221		fveq2 6191	. . . . . . . . . . . 12 |- ( x = ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) -> ( E ` x ) = ( E ` ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) )
222	194, 218, 220, 221	fmptco 6396	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( E o. ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ) = ( k e. NN0 |-> ( E ` ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ) )
223	9	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ℂfld e. Ring )
224	6	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> CC e. _V )
225	96	ffvelrni 6358	. . . . . . . . . . . . . . . 16 |- ( ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) e. ( Base ` (Poly1 ` ℂfld ) ) -> ( E ` ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) e. ( Base ` (ℂfld ^s CC ) ) )
226	194, 225	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( E ` ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) e. ( Base ` (ℂfld ^s CC ) ) )
227	3, 4, 67, 223, 224, 226	pwselbas 16149	. . . . . . . . . . . . . 14 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( E ` ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) : CC --> CC )
228	227	feqmptd 6249	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( E ` ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) = ( z e. CC |-> ( ( E ` ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ` z ) ) )
229	52	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ℂfld e. CRing )
230		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> z e. CC )
231	53, 115, 4, 54, 94, 229, 230	evl1vard 19701	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( (var1 ` ℂfld ) e. ( Base ` (Poly1 ` ℂfld ) ) /\ ( ( E ` (var1 ` ℂfld ) ) ` z ) = z ) )
232	185	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> k e. NN0 )
233	53, 54, 4, 94, 229, 230, 231, 117, 128, 232	evl1expd 19709	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. ( Base ` (Poly1 ` ℂfld ) ) /\ ( ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ` z ) = ( k (.g ` (mulGrp ` ℂfld ) ) z ) ) )
234	230, 232, 132	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( k (.g ` (mulGrp ` ℂfld ) ) z ) = ( z ^ k ) )
235	234	eqeq2d 2632	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ` z ) = ( k (.g ` (mulGrp ` ℂfld ) ) z ) <-> ( ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ` z ) = ( z ^ k ) ) )
236	235	anbi2d 740	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. ( Base ` (Poly1 ` ℂfld ) ) /\ ( ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ` z ) = ( k (.g ` (mulGrp ` ℂfld ) ) z ) ) <-> ( ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. ( Base ` (Poly1 ` ℂfld ) ) /\ ( ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ` z ) = ( z ^ k ) ) ) )
237	233, 236	mpbid 222	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. ( Base ` (Poly1 ` ℂfld ) ) /\ ( ( E ` ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ` z ) = ( z ^ k ) ) )
238	182	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( (coe1 ` a ) ` k ) e. CC )
239	53, 54, 4, 94, 229, 230, 237, 238, 154, 81	evl1vsd 19708	. . . . . . . . . . . . . . 15 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) e. ( Base ` (Poly1 ` ℂfld ) ) /\ ( ( E ` ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ` z ) = ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
240	239	simprd 479	. . . . . . . . . . . . . 14 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( E ` ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ` z ) = ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) )
241	240	mpteq2dva 4744	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( z e. CC |-> ( ( E ` ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ` z ) ) = ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
242	228, 241	eqtrd 2656	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( E ` ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) = ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
243	242	mpteq2dva 4744	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( k e. NN0 |-> ( E ` ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ) = ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) )
244	222, 243	eqtrd 2656	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( E o. ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ) = ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) )
245	244	oveq2d 6666	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (ℂfld ^s CC ) gsumg ( E o. ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) ) ) = ( (ℂfld ^s CC ) gsumg ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) ) )
246	158, 217, 245	3eqtr2d 2662	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( E ` a ) = ( (ℂfld ^s CC ) gsumg ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) ) )
247	6	a1i 11	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> CC e. _V )
248	9, 10	mp1i 13	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ℂfld e. CMnd )
249	182	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. CC )
250	33	adantll 750	. . . . . . . . . . 11 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( z ^ k ) e. CC )
251	249, 250	mulcld 10060	. . . . . . . . . 10 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) e. CC )
252	251	anasss 679	. . . . . . . . 9 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ ( z e. CC /\ k e. NN0 ) ) -> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) e. CC )
253	166	mptex 6486	. . . . . . . . . . . 12 |- ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V
254		funmpt 5926	. . . . . . . . . . . 12 |- Fun ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
255	253, 254, 39	3pm3.2i 1239	. . . . . . . . . . 11 |- ( ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) /\ ( 0g ` (ℂfld ^s CC ) ) e. _V )
256	255	a1i 11	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) /\ ( 0g ` (ℂfld ^s CC ) ) e. _V ) )
257		fzfid 12772	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) e. Fin )
258		eldifn 3733	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) -> -. k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) )
259	258	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> -. k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) )
260	153	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> a e. ( Base ` (Poly1 ` ℂfld ) ) )
261		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) -> k e. NN0 )
262	261	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> k e. NN0 )
263		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( deg1 ` ℂfld ) = ( deg1 ` ℂfld )
264	263, 54, 94, 17, 155	deg1ge 23858	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( a e. ( Base ` (Poly1 ` ℂfld ) ) /\ k e. NN0 /\ ( (coe1 ` a ) ` k ) =/= 0 ) -> k <_ ( ( deg1 ` ℂfld ) ` a ) )
265	264	3expia 1267	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a e. ( Base ` (Poly1 ` ℂfld ) ) /\ k e. NN0 ) -> ( ( (coe1 ` a ) ` k ) =/= 0 -> k <_ ( ( deg1 ` ℂfld ) ` a ) ) )
266	260, 262, 265	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( ( (coe1 ` a ) ` k ) =/= 0 -> k <_ ( ( deg1 ` ℂfld ) ` a ) ) )
267		0xr 10086	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. RR*
268	263, 54, 94	deg1xrcl 23842	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a e. ( Base ` (Poly1 ` ℂfld ) ) -> ( ( deg1 ` ℂfld ) ` a ) e. RR* )
269	153, 268	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( deg1 ` ℂfld ) ` a ) e. RR* )
270	269	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( ( deg1 ` ℂfld ) ` a ) e. RR* )
271		xrmax2 12007	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 0 e. RR* /\ ( ( deg1 ` ℂfld ) ` a ) e. RR* ) -> ( ( deg1 ` ℂfld ) ` a ) <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) )
272	267, 270, 271	sylancr 695	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( ( deg1 ` ℂfld ) ` a ) <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) )
273	262	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> k e. RR )
274	273	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> k e. RR* )
275		ifcl 4130	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( deg1 ` ℂfld ) ` a ) e. RR* /\ 0 e. RR* ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. RR* )
276	270, 267, 275	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. RR* )
277		xrletr 11989	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( k e. RR* /\ ( ( deg1 ` ℂfld ) ` a ) e. RR* /\ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. RR* ) -> ( ( k <_ ( ( deg1 ` ℂfld ) ` a ) /\ ( ( deg1 ` ℂfld ) ` a ) <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) -> k <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) )
278	274, 270, 276, 277	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( ( k <_ ( ( deg1 ` ℂfld ) ` a ) /\ ( ( deg1 ` ℂfld ) ` a ) <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) -> k <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) )
279	272, 278	mpan2d 710	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( k <_ ( ( deg1 ` ℂfld ) ` a ) -> k <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) )
280	266, 279	syld 47	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( ( (coe1 ` a ) ` k ) =/= 0 -> k <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) )
281	280, 262	jctild 566	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( ( (coe1 ` a ) ` k ) =/= 0 -> ( k e. NN0 /\ k <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) )
282	263, 54, 94	deg1cl 23843	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( a e. ( Base ` (Poly1 ` ℂfld ) ) -> ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) )
283	153, 282	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) )
284		elun 3753	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) <-> ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) )
285	283, 284	sylib 208	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) )
286		nn0ge0 11318	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> 0 <_ ( ( deg1 ` ℂfld ) ` a ) )
287	286	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = ( ( deg1 ` ℂfld ) ` a ) )
288		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> ( ( deg1 ` ℂfld ) ` a ) e. NN0 )
289	287, 288	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
290		mnflt0 11959	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- -oo < 0
291		mnfxr 10096	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- -oo e. RR*
292		xrltnle 10105	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( -oo e. RR* /\ 0 e. RR* ) -> ( -oo < 0 <-> -. 0 <_ -oo ) )
293	291, 267, 292	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -oo < 0 <-> -. 0 <_ -oo )
294	290, 293	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- -. 0 <_ -oo
295		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> ( ( deg1 ` ℂfld ) ` a ) = -oo )
296	295	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) <-> 0 <_ -oo ) )
297	294, 296	mtbiri 317	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> -. 0 <_ ( ( deg1 ` ℂfld ) ` a ) )
298	297	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = 0 )
299		0nn0 11307	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. NN0
300	298, 299	syl6eqel 2709	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
301	289, 300	jaoi 394	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
302	285, 301	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
303	302	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
304		fznn0 12432	. . . . . . . . . . . . . . . . . . . 20 |- ( if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 -> ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) <-> ( k e. NN0 /\ k <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) )
305	303, 304	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) <-> ( k e. NN0 /\ k <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) )
306	281, 305	sylibrd 249	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( ( (coe1 ` a ) ` k ) =/= 0 -> k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) )
307	306	necon1bd 2812	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( -. k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) -> ( (coe1 ` a ) ` k ) = 0 ) )
308	259, 307	mpd 15	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( (coe1 ` a ) ` k ) = 0 )
309	308	oveq1d 6665	. . . . . . . . . . . . . . 15 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) = ( 0 x. ( z ^ k ) ) )
310	261, 250	sylan2 491	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( z ^ k ) e. CC )
311	310	mul02d 10234	. . . . . . . . . . . . . . 15 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( 0 x. ( z ^ k ) ) = 0 )
312	309, 311	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) = 0 )
313	312	an32s 846	. . . . . . . . . . . . 13 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) /\ z e. CC ) -> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) = 0 )
314	313	mpteq2dva 4744	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> 0 ) )
315		fconstmpt 5163	. . . . . . . . . . . . 13 |- ( CC X. { 0 } ) = ( z e. CC |-> 0 )
316		ringmnd 18556	. . . . . . . . . . . . . . 15 |- (ℂfld e. Ring -> ℂfld e. Mnd )
317	9, 316	ax-mp 5	. . . . . . . . . . . . . 14 |- ℂfld e. Mnd
318	3, 17	pws0g 17326	. . . . . . . . . . . . . 14 |- ( (ℂfld e. Mnd /\ CC e. _V ) -> ( CC X. { 0 } ) = ( 0g ` (ℂfld ^s CC ) ) )
319	317, 6, 318	mp2an 708	. . . . . . . . . . . . 13 |- ( CC X. { 0 } ) = ( 0g ` (ℂfld ^s CC ) )
320	315, 319	eqtr3i 2646	. . . . . . . . . . . 12 |- ( z e. CC |-> 0 ) = ( 0g ` (ℂfld ^s CC ) )
321	314, 320	syl6eq 2672	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) = ( 0g ` (ℂfld ^s CC ) ) )
322	321, 167	suppss2 7329	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) supp ( 0g ` (ℂfld ^s CC ) ) ) C_ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) )
323		suppssfifsupp 8290	. . . . . . . . . 10 |- ( ( ( ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) /\ ( 0g ` (ℂfld ^s CC ) ) e. _V ) /\ ( ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) e. Fin /\ ( ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) supp ( 0g ` (ℂfld ^s CC ) ) ) C_ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) finSupp ( 0g ` (ℂfld ^s CC ) ) )
324	256, 257, 322, 323	syl12anc 1324	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) finSupp ( 0g ` (ℂfld ^s CC ) ) )
325	3, 4, 5, 247, 167, 248, 252, 324	pwsgsum 18378	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (ℂfld ^s CC ) gsumg ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) ) = ( z e. CC |-> (ℂfld gsumg ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) ) )
326		fz0ssnn0 12435	. . . . . . . . . . . 12 |- ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) C_ NN0
327		resmpt 5449	. . . . . . . . . . . 12 |- ( ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) C_ NN0 -> ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) |` ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) = ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
328	326, 327	ax-mp 5	. . . . . . . . . . 11 |- ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) |` ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) = ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) )
329	328	oveq2i 6661	. . . . . . . . . 10 |- (ℂfld gsumg ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) |` ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) = (ℂfld gsumg ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
330	9, 10	mp1i 13	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) -> ℂfld e. CMnd )
331	166	a1i 11	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) -> NN0 e. _V )
332		eqid 2622	. . . . . . . . . . . 12 |- ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) = ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) )
333	251, 332	fmptd 6385	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) -> ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) : NN0 --> CC )
334	312, 331	suppss2 7329	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) -> ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) supp 0 ) C_ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) )
335	166	mptex 6486	. . . . . . . . . . . . . 14 |- ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. _V
336		funmpt 5926	. . . . . . . . . . . . . 14 |- Fun ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) )
337	335, 336, 212	3pm3.2i 1239	. . . . . . . . . . . . 13 |- ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) /\ 0 e. _V )
338	337	a1i 11	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) -> ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) /\ 0 e. _V ) )
339		fzfid 12772	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) -> ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) e. Fin )
340		suppssfifsupp 8290	. . . . . . . . . . . 12 |- ( ( ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) /\ 0 e. _V ) /\ ( ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) e. Fin /\ ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) supp 0 ) C_ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) -> ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) finSupp 0 )
341	338, 339, 334, 340	syl12anc 1324	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) -> ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) finSupp 0 )
342	4, 17, 330, 331, 333, 334, 341	gsumres 18314	. . . . . . . . . 10 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) -> (ℂfld gsumg ( ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) |` ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) ) = (ℂfld gsumg ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) )
343		elfznn0 12433	. . . . . . . . . . . 12 |- ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) -> k e. NN0 )
344	343, 251	sylan2 491	. . . . . . . . . . 11 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) -> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) e. CC )
345	339, 344	gsumfsum 19813	. . . . . . . . . 10 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) -> (ℂfld gsumg ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) = sum_ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) )
346	329, 342, 345	3eqtr3a 2680	. . . . . . . . 9 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) -> (ℂfld gsumg ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) = sum_ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) )
347	346	mpteq2dva 4744	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( z e. CC |-> (ℂfld gsumg ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
348	246, 325, 347	3eqtrd 2660	. . . . . . 7 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( E ` a ) = ( z e. CC |-> sum_ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
349	12	adantr 481	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> S C_ CC )
350		elplyr 23957	. . . . . . . 8 |- ( ( S C_ CC /\ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 /\ (coe1 ` a ) : NN0 --> S ) -> ( z e. CC |-> sum_ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. (Poly ` S ) )
351	349, 302, 180, 350	syl3anc 1326	. . . . . . 7 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( z e. CC |-> sum_ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. (Poly ` S ) )
352	348, 351	eqeltrd 2701	. . . . . 6 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( E ` a ) e. (Poly ` S ) )
353		eleq1 2689	. . . . . 6 |- ( ( E ` a ) = f -> ( ( E ` a ) e. (Poly ` S ) <-> f e. (Poly ` S ) ) )
354	352, 353	syl5ibcom 235	. . . . 5 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( E ` a ) = f -> f e. (Poly ` S ) ) )
355	354	rexlimdva 3031	. . . 4 |- ( S e. (SubRing ` ℂfld ) -> ( E. a e. A ( E ` a ) = f -> f e. (Poly ` S ) ) )
356	152, 355	syl5 34	. . 3 |- ( S e. (SubRing ` ℂfld ) -> ( f e. ( E " A ) -> f e. (Poly ` S ) ) )
357	148, 356	impbid 202	. 2 |- ( S e. (SubRing ` ℂfld ) -> ( f e. (Poly ` S ) <-> f e. ( E " A ) ) )
358	357	eqrdv 2620	1 |- ( S e. (SubRing ` ℂfld ) -> (Poly ` S ) = ( E " A ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   E.wrex 2913   _Vcvv 3200   \ cdif 3571   u. cun 3572   C_ wss 3574   ifcif 4086   {csn 4177   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   |` cres 5116   "cima 5117   o. ccom 5118   Fun wfun 5882   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   oFcof 6895   supp csupp 7295   ^m cmap 7857   Fincfn 7955   finSupp cfsupp 8275   CCcc 9934   0cc0 9936   x. cmul 9941   -oocmnf 10072   RR*cxr 10073   < clt 10074   <_ cle 10075   NN0cn0 11292   ...cfz 12326   ^cexp 12860   sum_csu 14416   Basecbs 15857   ↾_s cress 15858   .rcmulr 15942  Scalarcsca 15944   .scvsca 15945   0gc0g 16100   gsum_g cgsu 16101   ^_s cpws 16107   Mndcmnd 17294   MndHom cmhm 17333  SubMndcsubmnd 17334  ._gcmg 17540  SubGrpcsubg 17588   GrpHom cghm 17657  CMndccmn 18193  mulGrpcmgp 18489   Ringcrg 18547   CRingccrg 18548   RingHom crh 18712  SubRingcsubrg 18776   LModclmod 18863  algSccascl 19311  var₁cv1 19546  Poly₁cpl1 19547  coe₁cco1 19548  eval₁ce1 19679  ℂ_fldccnfld 19746   deg₁ cdg1 23814  Polycply 23940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-ofr 6898  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-sup 8348  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-0g 16102  df-gsum 16103  df-prds 16108  df-pws 16110  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-ghm 17658  df-cntz 17750  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-srg 18506  df-ring 18549  df-cring 18550  df-rnghom 18715  df-subrg 18778  df-lmod 18865  df-lss 18933  df-lsp 18972  df-assa 19312  df-asp 19313  df-ascl 19314  df-psr 19356  df-mvr 19357  df-mpl 19358  df-opsr 19360  df-evls 19506  df-evl 19507  df-psr1 19550  df-vr1 19551  df-ply1 19552  df-coe1 19553  df-evl1 19681  df-cnfld 19747  df-mdeg 23815  df-deg1 23816  df-ply 23944

This theorem is referenced by: (None)