Theorem plypf1 23152

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 23135	. . . . 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 465	. . . 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 2422	. . . . . . . . 9 |- (ℂfld ^s CC ) = (ℂfld ^s CC )
4		cnfldbas 18961	. . . . . . . . 9 |- CC = ( Base ` ℂfld )
5		eqid 2422	. . . . . . . . 9 |- ( 0g ` (ℂfld ^s CC ) ) = ( 0g ` (ℂfld ^s CC ) )
6		cnex 9620	. . . . . . . . . 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 12185	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( 0 ... n ) e. Fin )
9		cnring 18977	. . . . . . . . . 10 |- ℂfld e. Ring
10		ringcmn 17798	. . . . . . . . . 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 17996	. . . . . . . . . . . . 13 |- ( S e. (SubRing ` ℂfld ) -> S C_ CC )
13	12	ad2antrr 730	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> S C_ CC )
14		elmapi 7497	. . . . . . . . . . . . . . 15 |- ( a e. ( ( S u. { 0 } ) ^m NN0 ) -> a : NN0 --> ( S u. { 0 } ) )
15	14	ad2antll 733	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> a : NN0 --> ( S u. { 0 } ) )
16		subrgsubg 18001	. . . . . . . . . . . . . . . . . . 19 |- ( S e. (SubRing ` ℂfld ) -> S e. (SubGrp ` ℂfld ) )
17		cnfld0 18979	. . . . . . . . . . . . . . . . . . . 20 |- 0 = ( 0g ` ℂfld )
18	17	subg0cl 16812	. . . . . . . . . . . . . . . . . . 19 |- ( S e. (SubGrp ` ℂfld ) -> 0 e. S )
19	16, 18	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( S e. (SubRing ` ℂfld ) -> 0 e. S )
20	19	adantr 466	. . . . . . . . . . . . . . . . 17 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> 0 e. S )
21	20	snssd 4142	. . . . . . . . . . . . . . . 16 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> { 0 } C_ S )
22		ssequn2 3639	. . . . . . . . . . . . . . . 16 |- ( { 0 } C_ S <-> ( S u. { 0 } ) = S )
23	21, 22	sylib 199	. . . . . . . . . . . . . . 15 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( S u. { 0 } ) = S )
24	23	feq3d 5730	. . . . . . . . . . . . . 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 213	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> a : NN0 --> S )
26		elfznn0 11887	. . . . . . . . . . . . 13 |- ( k e. ( 0 ... n ) -> k e. NN0 )
27		ffvelrn 6031	. . . . . . . . . . . . 13 |- ( ( a : NN0 --> S /\ k e. NN0 ) -> ( a ` k ) e. S )
28	25, 26, 27	syl2an 479	. . . . . . . . . . . 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 3465	. . . . . . . . . . 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 720	. . . . . . . . . 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 762	. . . . . . . . . . 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 733	. . . . . . . . . . 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 12289	. . . . . . . . . . 11 |- ( ( z e. CC /\ k e. NN0 ) -> ( z ^ k ) e. CC )
34	31, 32, 33	syl2anc 665	. . . . . . . . . 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 9663	. . . . . . . . 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 2422	. . . . . . . . . 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 6147	. . . . . . . . . . 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 5887	. . . . . . . . . . 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 7896	. . . . . . . . 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 17598	. . . . . . . 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 12185	. . . . . . . . . 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 652	. . . . . . . . . 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 19021	. . . . . . . . 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 4507	. . . . . . . 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 2463	. . . . . . 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 17830	. . . . . . . . . 10 |- ( (ℂfld e. Ring /\ CC e. _V ) -> (ℂfld ^s CC ) e. Ring )
49	9, 6, 48	mp2an 676	. . . . . . . . 9 |- (ℂfld ^s CC ) e. Ring
50		ringcmn 17798	. . . . . . . . 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 18976	. . . . . . . . . . 11 |- ℂfld e. CRing
53		plypf1.e	. . . . . . . . . . . 12 |- E = (eval1 ` ℂfld )
54		eqid 2422	. . . . . . . . . . . 12 |- (Poly1 ` ℂfld ) = (Poly1 ` ℂfld )
55	53, 54, 3, 4	evl1rhm 18907	. . . . . . . . . . 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 18813	. . . . . . . . . . 11 |- ( S e. (SubRing ` ℂfld ) -> A e. (SubRing ` (Poly1 ` ℂfld ) ) )
61	60	adantr 466	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> A e. (SubRing ` (Poly1 ` ℂfld ) ) )
62		rhmima 18026	. . . . . . . . . 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 667	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) )
64		subrgsubg 18001	. . . . . . . . 9 |- ( ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) -> ( E " A ) e. (SubGrp ` (ℂfld ^s CC ) ) )
65		subgsubm 16826	. . . . . . . . 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 2422	. . . . . . . . . . . 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 5785	. . . . . . . . . . . . . 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 15373	. . . . . . . . . . . . . 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 676	. . . . . . . . . . . . 13 |- ( ( CC X. { ( a ` k ) } ) e. ( Base ` (ℂfld ^s CC ) ) <-> ( CC X. { ( a ` k ) } ) : CC --> CC )
74	71, 73	sylibr 215	. . . . . . . . . . . 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 814	. . . . . . . . . . . . . 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 2422	. . . . . . . . . . . . . 14 |- ( z e. CC |-> ( z ^ k ) ) = ( z e. CC |-> ( z ^ k ) )
77	75, 76	fmptd 6057	. . . . . . . . . . . . 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 15373	. . . . . . . . . . . . . 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 676	. . . . . . . . . . . . 13 |- ( ( z e. CC |-> ( z ^ k ) ) e. ( Base ` (ℂfld ^s CC ) ) <-> ( z e. CC |-> ( z ^ k ) ) : CC --> CC )
80	77, 79	sylibr 215	. . . . . . . . . . . 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 18963	. . . . . . . . . . . 12 |- x. = ( .r ` ℂfld )
82		eqid 2422	. . . . . . . . . . . 12 |- ( .r ` (ℂfld ^s CC ) ) = ( .r ` (ℂfld ^s CC ) )
83	3, 67, 68, 69, 74, 80, 81, 82	pwsmulrval 15376	. . . . . . . . . . 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 466	. . . . . . . . . . . 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 4893	. . . . . . . . . . . . 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 2423	. . . . . . . . . . . 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 6558	. . . . . . . . . . 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 2463	. . . . . . . . . 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 466	. . . . . . . . . . 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 2422	. . . . . . . . . . . . . 14 |- (algSc ` (Poly1 ` ℂfld ) ) = (algSc ` (Poly1 ` ℂfld ) )
92	53, 54, 4, 91	evl1sca 18909	. . . . . . . . . . . . 13 |- ( (ℂfld e. CRing /\ ( a ` k ) e. CC ) -> ( E ` ( (algSc ` (Poly1 ` ℂfld ) ) ` ( a ` k ) ) ) = ( CC X. { ( a ` k ) } ) )
93	52, 29, 92	sylancr 667	. . . . . . . . . . . 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 2422	. . . . . . . . . . . . . . . 16 |- ( Base ` (Poly1 ` ℂfld ) ) = ( Base ` (Poly1 ` ℂfld ) )
95	94, 67	rhmf 17941	. . . . . . . . . . . . . . 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 5742	. . . . . . . . . . . . . 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 17996	. . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . 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 758	. . . . . . . . . . . . . . 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 18840	. . . . . . . . . . . . . 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 235	. . . . . . . . . . . . 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 6154	. . . . . . . . . . . . 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 1264	. . . . . . . . . . . 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 2511	. . . . . . . . . . 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 17996	. . . . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . . 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 2422	. . . . . . . . . . . . . . . . . . . 20 |- (mulGrp ` (Poly1 ` ℂfld ) ) = (mulGrp ` (Poly1 ` ℂfld ) )
112	111	subrgsubm 18008	. . . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> k e. NN0 )
115		eqid 2422	. . . . . . . . . . . . . . . . . . 19 |- (var1 ` ℂfld ) = (var1 ` ℂfld )
116	115, 102, 57, 58, 59	subrgvr1cl 18842	. . . . . . . . . . . . . . . . . 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 2422	. . . . . . . . . . . . . . . . . . 19 |- (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) = (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) )
118	117	submmulgcl 16779	. . . . . . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . . . . . 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 6154	. . . . . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . . . . 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 3465	. . . . . . . . . . . . . . 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 15374	. . . . . . . . . . . . . 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 5930	. . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . 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 18912	. . . . . . . . . . . . . . . . 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 2422	. . . . . . . . . . . . . . . . 17 |- (.g ` (mulGrp ` ℂfld ) ) = (.g ` (mulGrp ` ℂfld ) )
129	114	adantr 466	. . . . . . . . . . . . . . . . 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 18920	. . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . 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 18988	. . . . . . . . . . . . . . . 16 |- ( ( z e. CC /\ k e. NN0 ) -> ( k (.g ` (mulGrp ` ℂfld ) ) z ) = ( z ^ k ) )
133	126, 129, 132	syl2anc 665	. . . . . . . . . . . . . . 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 2463	. . . . . . . . . . . . . 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 4507	. . . . . . . . . . . . 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 2463	. . . . . . . . . . . 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 2511	. . . . . . . . . . 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 18007	. . . . . . . . . . 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 1264	. . . . . . . . . 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 2511	. . . . . . . . 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 6057	. . . . . . . 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 7896	. . . . . . . 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 17539	. . . . . . 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 2511	. . . . . 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 2494	. . . . . 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 225	. . . . 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 2924	. . . 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 33	. . 3 |- ( S e. (SubRing ` ℂfld ) -> ( f e. (Poly ` S ) -> f e. ( E " A ) ) )
149		ffun 5744	. . . . . 6 |- ( E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) -> Fun E )
150	96, 149	ax-mp 5	. . . . 5 |- Fun E
151		fvelima 5929	. . . . 5 |- ( ( Fun E /\ f e. ( E " A ) ) -> E. a e. A ( E ` a ) = f )
152	150, 151	mpan 674	. . . 4 |- ( f e. ( E " A ) -> E. a e. A ( E ` a ) = f )
153	100	sselda 3464	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> a e. ( Base ` (Poly1 ` ℂfld ) ) )
154		eqid 2422	. . . . . . . . . . . 12 |- ( .s ` (Poly1 ` ℂfld ) ) = ( .s ` (Poly1 ` ℂfld ) )
155		eqid 2422	. . . . . . . . . . . 12 |- (coe1 ` a ) = (coe1 ` a )
156	54, 115, 94, 154, 111, 117, 155	ply1coe 18876	. . . . . . . . . . 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 667	. . . . . . . . . 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 5881	. . . . . . . . 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 2422	. . . . . . . . . 10 |- ( 0g ` (Poly1 ` ℂfld ) ) = ( 0g ` (Poly1 ` ℂfld ) )
160	54	ply1ring 18828	. . . . . . . . . . . 12 |- (ℂfld e. Ring -> (Poly1 ` ℂfld ) e. Ring )
161	9, 160	ax-mp 5	. . . . . . . . . . 11 |- (Poly1 ` ℂfld ) e. Ring
162		ringcmn 17798	. . . . . . . . . . 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 17776	. . . . . . . . . . 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 10875	. . . . . . . . . . 11 |- NN0 e. _V
167	166	a1i 11	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> NN0 e. _V )
168		rhmghm 17940	. . . . . . . . . . . 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 16880	. . . . . . . . . . 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 18832	. . . . . . . . . . . . 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 730	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> S C_ CC )
175		eqid 2422	. . . . . . . . . . . . . . . . 17 |- ( Base ` R ) = ( Base ` R )
176	155, 59, 58, 175	coe1f 18791	. . . . . . . . . . . . . . . 16 |- ( a e. A -> (coe1 ` a ) : NN0 --> ( Base ` R ) )
177	57	subrgbas 18004	. . . . . . . . . . . . . . . . 17 |- ( S e. (SubRing ` ℂfld ) -> S = ( Base ` R ) )
178	177	feq3d 5730	. . . . . . . . . . . . . . . 16 |- ( S e. (SubRing ` ℂfld ) -> ( (coe1 ` a ) : NN0 --> S <-> (coe1 ` a ) : NN0 --> ( Base ` R ) ) )
179	176, 178	syl5ibr 224	. . . . . . . . . . . . . . 15 |- ( S e. (SubRing ` ℂfld ) -> ( a e. A -> (coe1 ` a ) : NN0 --> S ) )
180	179	imp 430	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) : NN0 --> S )
181	180	ffvelrnda 6033	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. S )
182	174, 181	sseldd 3465	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. CC )
183	111	ringmgp 17773	. . . . . . . . . . . . . 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 462	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> k e. NN0 )
186	115, 54, 94	vr1cl 18797	. . . . . . . . . . . . . 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 17716	. . . . . . . . . . . . . 14 |- ( Base ` (Poly1 ` ℂfld ) ) = ( Base ` (mulGrp ` (Poly1 ` ℂfld ) ) )
189	188, 117	mulgnn0cl 16761	. . . . . . . . . . . . 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 1264	. . . . . . . . . . . 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 18833	. . . . . . . . . . . . . 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 18095	. . . . . . . . . . . 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 1264	. . . . . . . . . . 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 2422	. . . . . . . . . . 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 6057	. . . . . . . . . 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 6147	. . . . . . . . . . . . 13 |- ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) e. _V
198		funmpt 5633	. . . . . . . . . . . . 13 |- Fun ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) )
199		fvex 5887	. . . . . . . . . . . . 13 |- ( 0g ` (Poly1 ` ℂfld ) ) e. _V
200	197, 198, 199	3pm3.2i 1183	. . . . . . . . . . . 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 18793	. . . . . . . . . . . . 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 7892	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (coe1 ` a ) supp 0 ) e. Fin )
205	180	feqmptd 5930	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) = ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) )
206	205	oveq1d 6316	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (coe1 ` a ) supp 0 ) = ( ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) supp 0 ) )
207		eqimss2 3517	. . . . . . . . . . . . 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 18111	. . . . . . . . . . . . 13 |- ( ( (Poly1 ` ℂfld ) e. LMod /\ x e. ( Base ` (Poly1 ` ℂfld ) ) ) -> ( 0 ( .s ` (Poly1 ` ℂfld ) ) x ) = ( 0g ` (Poly1 ` ℂfld ) ) )
211	209, 210	sylan 473	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ x e. ( Base ` (Poly1 ` ℂfld ) ) ) -> ( 0 ( .s ` (Poly1 ` ℂfld ) ) x ) = ( 0g ` (Poly1 ` ℂfld ) ) )
212		c0ex 9637	. . . . . . . . . . . . 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 6954	. . . . . . . . . . 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 7900	. . . . . . . . . . 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 1262	. . . . . . . . . 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 17558	. . . . . . . . 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 2423	. . . . . . . . . . . 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 5930	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> E = ( x e. ( Base ` (Poly1 ` ℂfld ) ) |-> ( E ` x ) ) )
221		fveq2 5877	. . . . . . . . . . . 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 6067	. . . . . . . . . . 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 6032	. . . . . . . . . . . . . . . 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 15374	. . . . . . . . . . . . . 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 5930	. . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . 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 18912	. . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . 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 18920	. . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( k (.g ` (mulGrp ` ℂfld ) ) z ) = ( z ^ k ) )
235	234	eqeq2d 2436	. . . . . . . . . . . . . . . . . 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 708	. . . . . . . . . . . . . . . . 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 213	. . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . 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 18919	. . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . 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 4507	. . . . . . . . . . . . 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 2463	. . . . . . . . . . . 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 4507	. . . . . . . . . . 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 2463	. . . . . . . . . 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 6317	. . . . . . . . 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 2469	. . . . . . . 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 719	. . . . . . . . . . 11 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. CC )
250	33	adantll 718	. . . . . . . . . . 11 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( z ^ k ) e. CC )
251	249, 250	mulcld 9663	. . . . . . . . . 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 651	. . . . . . . . 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 6147	. . . . . . . . . . . 12 |- ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V
254		funmpt 5633	. . . . . . . . . . . 12 |- Fun ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
255	253, 254, 39	3pm3.2i 1183	. . . . . . . . . . 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 12185	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) e. Fin )
258		eldifn 3588	. . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . . . . . 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 3587	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) -> k e. NN0 )
262	261	adantl 467	. . . . . . . . . . . . . . . . . . . . . 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 2422	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( deg1 ` ℂfld ) = ( deg1 ` ℂfld )
264	263, 54, 94, 17, 155	deg1ge 23033	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( a e. ( Base ` (Poly1 ` ℂfld ) ) /\ k e. NN0 /\ ( (coe1 ` a ) ` k ) =/= 0 ) -> k <_ ( ( deg1 ` ℂfld ) ` a ) )
265	264	3expia 1207	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a e. ( Base ` (Poly1 ` ℂfld ) ) /\ k e. NN0 ) -> ( ( (coe1 ` a ) ` k ) =/= 0 -> k <_ ( ( deg1 ` ℂfld ) ` a ) ) )
266	260, 262, 265	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 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 9687	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. RR*
268	263, 54, 94	deg1xrcl 23017	. . . . . . . . . . . . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . . . . . . 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 11471	. . . . . . . . . . . . . . . . . . . . . . 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 667	. . . . . . . . . . . . . . . . . . . . . 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 10926	. . . . . . . . . . . . . . . . . . . . . . . 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 9690	. . . . . . . . . . . . . . . . . . . . . . 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 3951	. . . . . . . . . . . . . . . . . . . . . . . 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 666	. . . . . . . . . . . . . . . . . . . . . . 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 11455	. . . . . . . . . . . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . . . . . . . . . . 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 678	. . . . . . . . . . . . . . . . . . . . 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 45	. . . . . . . . . . . . . . . . . . . 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 545	. . . . . . . . . . . . . . . . . . 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 23018	. . . . . . . . . . . . . . . . . . . . . . . 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 3606	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) <-> ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) )
285	283, 284	sylib 199	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) )
286		nn0ge0 10895	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> 0 <_ ( ( deg1 ` ℂfld ) ` a ) )
287	286	iftrued 3917	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = ( ( deg1 ` ℂfld ) ` a ) )
288		id 23	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> ( ( deg1 ` ℂfld ) ` a ) e. NN0 )
289	287, 288	eqeltrd 2510	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
290		mnflt0 11427	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- -oo < 0
291		mnfxr 11414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- -oo e. RR*
292		xrltnle 9701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( -oo e. RR* /\ 0 e. RR* ) -> ( -oo < 0 <-> -. 0 <_ -oo ) )
293	291, 267, 292	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -oo < 0 <-> -. 0 <_ -oo )
294	290, 293	mpbi 211	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- -. 0 <_ -oo
295		elsni 4021	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> ( ( deg1 ` ℂfld ) ` a ) = -oo )
296	295	breq2d 4432	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) <-> 0 <_ -oo ) )
297	294, 296	mtbiri 304	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> -. 0 <_ ( ( deg1 ` ℂfld ) ` a ) )
298	297	iffalsed 3920	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = 0 )
299		0nn0 10884	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. NN0
300	298, 299	syl6eqel 2518	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
301	289, 300	jaoi 380	. . . . . . . . . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . . . 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 11886	. . . . . . . . . . . . . . . . . . . 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 237	. . . . . . . . . . . . . . . . . 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 2642	. . . . . . . . . . . . . . . . 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 6316	. . . . . . . . . . . . . . 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 476	. . . . . . . . . . . . . . . 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 9831	. . . . . . . . . . . . . . 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 2463	. . . . . . . . . . . . . 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 811	. . . . . . . . . . . . 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 4507	. . . . . . . . . . . 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 4893	. . . . . . . . . . . . 13 |- ( CC X. { 0 } ) = ( z e. CC |-> 0 )
316		ringmnd 17776	. . . . . . . . . . . . . . 15 |- (ℂfld e. Ring -> ℂfld e. Mnd )
317	9, 316	ax-mp 5	. . . . . . . . . . . . . 14 |- ℂfld e. Mnd
318	3, 17	pws0g 16559	. . . . . . . . . . . . . 14 |- ( (ℂfld e. Mnd /\ CC e. _V ) -> ( CC X. { 0 } ) = ( 0g ` (ℂfld ^s CC ) ) )
319	317, 6, 318	mp2an 676	. . . . . . . . . . . . 13 |- ( CC X. { 0 } ) = ( 0g ` (ℂfld ^s CC ) )
320	315, 319	eqtr3i 2453	. . . . . . . . . . . 12 |- ( z e. CC |-> 0 ) = ( 0g ` (ℂfld ^s CC ) )
321	314, 320	syl6eq 2479	. . . . . . . . . . 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 6956	. . . . . . . . . 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 7900	. . . . . . . . . 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 1262	. . . . . . . . 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 17598	. . . . . . . 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		elfznn0 11887	. . . . . . . . . . . . 13 |- ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) -> k e. NN0 )
327	326	ssriv 3468	. . . . . . . . . . . 12 |- ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) C_ NN0
328		resmpt 5169	. . . . . . . . . . . 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 ) ) ) )
329	327, 328	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 ) ) )
330	329	oveq2i 6312	. . . . . . . . . 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 ) ) ) )
331	9, 10	mp1i 13	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) -> ℂfld e. CMnd )
332	166	a1i 11	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing