Theorem plypf1 22694

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 22677	. . . . 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 462	. . . 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 2382	. . . . . . . . 9 |- (ℂfld ^s CC ) = (ℂfld ^s CC )
4		cnfldbas 18537	. . . . . . . . 9 |- CC = ( Base ` ℂfld )
5		eqid 2382	. . . . . . . . 9 |- ( 0g ` (ℂfld ^s CC ) ) = ( 0g ` (ℂfld ^s CC ) )
6		cnex 9484	. . . . . . . . . 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 11986	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( 0 ... n ) e. Fin )
9		cnring 18553	. . . . . . . . . 10 |- ℂfld e. Ring
10		ringcmn 17342	. . . . . . . . . 10 |- (ℂfld e. Ring -> ℂfld e. CMnd )
11	9, 10	mp1i 12	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ℂfld e. CMnd )
12	4	subrgss 17543	. . . . . . . . . . . . 13 |- ( S e. (SubRing ` ℂfld ) -> S C_ CC )
13	12	ad2antrr 723	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> S C_ CC )
14		elmapi 7359	. . . . . . . . . . . . . . 15 |- ( a e. ( ( S u. { 0 } ) ^m NN0 ) -> a : NN0 --> ( S u. { 0 } ) )
15	14	ad2antll 726	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> a : NN0 --> ( S u. { 0 } ) )
16		subrgsubg 17548	. . . . . . . . . . . . . . . . . . 19 |- ( S e. (SubRing ` ℂfld ) -> S e. (SubGrp ` ℂfld ) )
17		cnfld0 18555	. . . . . . . . . . . . . . . . . . . 20 |- 0 = ( 0g ` ℂfld )
18	17	subg0cl 16326	. . . . . . . . . . . . . . . . . . 19 |- ( S e. (SubGrp ` ℂfld ) -> 0 e. S )
19	16, 18	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( S e. (SubRing ` ℂfld ) -> 0 e. S )
20	19	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> 0 e. S )
21	20	snssd 4089	. . . . . . . . . . . . . . . 16 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> { 0 } C_ S )
22		ssequn2 3591	. . . . . . . . . . . . . . . 16 |- ( { 0 } C_ S <-> ( S u. { 0 } ) = S )
23	21, 22	sylib 196	. . . . . . . . . . . . . . 15 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( S u. { 0 } ) = S )
24	23	feq3d 5627	. . . . . . . . . . . . . 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 210	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> a : NN0 --> S )
26		elfznn0 11693	. . . . . . . . . . . . 13 |- ( k e. ( 0 ... n ) -> k e. NN0 )
27		ffvelrn 5931	. . . . . . . . . . . . 13 |- ( ( a : NN0 --> S /\ k e. NN0 ) -> ( a ` k ) e. S )
28	25, 26, 27	syl2an 475	. . . . . . . . . . . 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 3418	. . . . . . . . . . 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 713	. . . . . . . . . 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 754	. . . . . . . . . . 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 726	. . . . . . . . . . 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 12087	. . . . . . . . . . 11 |- ( ( z e. CC /\ k e. NN0 ) -> ( z ^ k ) e. CC )
34	31, 32, 33	syl2anc 659	. . . . . . . . . 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 9527	. . . . . . . . 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 2382	. . . . . . . . . 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 6044	. . . . . . . . . . 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 5784	. . . . . . . . . . 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 7755	. . . . . . . . 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 17122	. . . . . . . 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 11986	. . . . . . . . . 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 646	. . . . . . . . . 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 18597	. . . . . . . . 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 4453	. . . . . . . 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 2423	. . . . . . 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 17377	. . . . . . . . . 10 |- ( (ℂfld e. Ring /\ CC e. _V ) -> (ℂfld ^s CC ) e. Ring )
49	9, 6, 48	mp2an 670	. . . . . . . . 9 |- (ℂfld ^s CC ) e. Ring
50		ringcmn 17342	. . . . . . . . 9 |- ( (ℂfld ^s CC ) e. Ring -> (ℂfld ^s CC ) e. CMnd )
51	49, 50	mp1i 12	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> (ℂfld ^s CC ) e. CMnd )
52		cncrng 18552	. . . . . . . . . . 11 |- ℂfld e. CRing
53		plypf1.e	. . . . . . . . . . . 12 |- E = (eval1 ` ℂfld )
54		eqid 2382	. . . . . . . . . . . 12 |- (Poly1 ` ℂfld ) = (Poly1 ` ℂfld )
55	53, 54, 3, 4	evl1rhm 18481	. . . . . . . . . . 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 18387	. . . . . . . . . . 11 |- ( S e. (SubRing ` ℂfld ) -> A e. (SubRing ` (Poly1 ` ℂfld ) ) )
61	60	adantr 463	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> A e. (SubRing ` (Poly1 ` ℂfld ) ) )
62		rhmima 17573	. . . . . . . . . 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 661	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) )
64		subrgsubg 17548	. . . . . . . . 9 |- ( ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) -> ( E " A ) e. (SubGrp ` (ℂfld ^s CC ) ) )
65		subgsubm 16340	. . . . . . . . 9 |- ( ( E " A ) e. (SubGrp ` (ℂfld ^s CC ) ) -> ( E " A ) e. (SubMnd ` (ℂfld ^s CC ) ) )
66	63, 64, 65	3syl 20	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( E " A ) e. (SubMnd ` (ℂfld ^s CC ) ) )
67		eqid 2382	. . . . . . . . . . . 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 5682	. . . . . . . . . . . . . 14 |- ( ( a ` k ) e. CC -> ( CC X. { ( a ` k ) } ) : CC --> CC )
71	29, 70	syl 16	. . . . . . . . . . . . 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 14895	. . . . . . . . . . . . . 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 670	. . . . . . . . . . . . 13 |- ( ( CC X. { ( a ` k ) } ) e. ( Base ` (ℂfld ^s CC ) ) <-> ( CC X. { ( a ` k ) } ) : CC --> CC )
74	71, 73	sylibr 212	. . . . . . . . . . . 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 805	. . . . . . . . . . . . . 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 2382	. . . . . . . . . . . . . 14 |- ( z e. CC |-> ( z ^ k ) ) = ( z e. CC |-> ( z ^ k ) )
77	75, 76	fmptd 5957	. . . . . . . . . . . . 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 14895	. . . . . . . . . . . . . 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 670	. . . . . . . . . . . . 13 |- ( ( z e. CC |-> ( z ^ k ) ) e. ( Base ` (ℂfld ^s CC ) ) <-> ( z e. CC |-> ( z ^ k ) ) : CC --> CC )
80	77, 79	sylibr 212	. . . . . . . . . . . 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 18539	. . . . . . . . . . . 12 |- x. = ( .r ` ℂfld )
82		eqid 2382	. . . . . . . . . . . 12 |- ( .r ` (ℂfld ^s CC ) ) = ( .r ` (ℂfld ^s CC ) )
83	3, 67, 68, 69, 74, 80, 81, 82	pwsmulrval 14898	. . . . . . . . . . 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 463	. . . . . . . . . . . 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 4957	. . . . . . . . . . . . 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 2383	. . . . . . . . . . . 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 6455	. . . . . . . . . . 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 2423	. . . . . . . . . 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 463	. . . . . . . . . . 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 2382	. . . . . . . . . . . . . 14 |- (algSc ` (Poly1 ` ℂfld ) ) = (algSc ` (Poly1 ` ℂfld ) )
92	53, 54, 4, 91	evl1sca 18483	. . . . . . . . . . . . 13 |- ( (ℂfld e. CRing /\ ( a ` k ) e. CC ) -> ( E ` ( (algSc ` (Poly1 ` ℂfld ) ) ` ( a ` k ) ) ) = ( CC X. { ( a ` k ) } ) )
93	52, 29, 92	sylancr 661	. . . . . . . . . . . 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 2382	. . . . . . . . . . . . . . . 16 |- ( Base ` (Poly1 ` ℂfld ) ) = ( Base ` (Poly1 ` ℂfld ) )
95	94, 67	rhmf 17488	. . . . . . . . . . . . . . 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 5639	. . . . . . . . . . . . . 14 |- ( E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) -> E Fn ( Base ` (Poly1 ` ℂfld ) ) )
98	96, 97	mp1i 12	. . . . . . . . . . . . 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 17543	. . . . . . . . . . . . . . 15 |- ( A e. (SubRing ` (Poly1 ` ℂfld ) ) -> A C_ ( Base ` (Poly1 ` ℂfld ) ) )
100	60, 99	syl 16	. . . . . . . . . . . . . 14 |- ( S e. (SubRing ` ℂfld ) -> A C_ ( Base ` (Poly1 ` ℂfld ) ) )
101	100	ad2antrr 723	. . . . . . . . . . . . 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 751	. . . . . . . . . . . . . . 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 18414	. . . . . . . . . . . . . 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 232	. . . . . . . . . . . . 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 6051	. . . . . . . . . . . . 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 1226	. . . . . . . . . . . 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 2471	. . . . . . . . . . 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 17543	. . . . . . . . . . . . . . . . 17 |- ( ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) -> ( E " A ) C_ ( Base ` (ℂfld ^s CC ) ) )
109	90, 108	syl 16	. . . . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . . . . . . 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 2382	. . . . . . . . . . . . . . . . . . . 20 |- (mulGrp ` (Poly1 ` ℂfld ) ) = (mulGrp ` (Poly1 ` ℂfld ) )
112	111	subrgsubm 17555	. . . . . . . . . . . . . . . . . . 19 |- ( A e. (SubRing ` (Poly1 ` ℂfld ) ) -> A e. (SubMnd ` (mulGrp ` (Poly1 ` ℂfld ) ) ) )
113	110, 112	syl 16	. . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . . 18 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> k e. NN0 )
115		eqid 2382	. . . . . . . . . . . . . . . . . . 19 |- (var1 ` ℂfld ) = (var1 ` ℂfld )
116	115, 102, 57, 58, 59	subrgvr1cl 18416	. . . . . . . . . . . . . . . . . 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 2382	. . . . . . . . . . . . . . . . . . 19 |- (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) = (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) )
118	117	submmulgcl 16293	. . . . . . . . . . . . . . . . . 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 1226	. . . . . . . . . . . . . . . . 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 6051	. . . . . . . . . . . . . . . . 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 1226	. . . . . . . . . . . . . . . 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 3418	. . . . . . . . . . . . . . 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 14896	. . . . . . . . . . . . . 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 5827	. . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . . 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 18486	. . . . . . . . . . . . . . . . 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 2382	. . . . . . . . . . . . . . . . 17 |- (.g ` (mulGrp ` ℂfld ) ) = (.g ` (mulGrp ` ℂfld ) )
129	114	adantr 463	. . . . . . . . . . . . . . . . 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 18494	. . . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . . 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 18564	. . . . . . . . . . . . . . . 16 |- ( ( z e. CC /\ k e. NN0 ) -> ( k (.g ` (mulGrp ` ℂfld ) ) z ) = ( z ^ k ) )
133	126, 129, 132	syl2anc 659	. . . . . . . . . . . . . . 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 2423	. . . . . . . . . . . . . 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 4453	. . . . . . . . . . . . 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 2423	. . . . . . . . . . . 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 2471	. . . . . . . . . . 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 17554	. . . . . . . . . . 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 1226	. . . . . . . . . 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 2471	. . . . . . . . 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 5957	. . . . . . . 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 7755	. . . . . . . 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 17047	. . . . . . 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 2471	. . . . . 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 2454	. . . . . 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 222	. . . . 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 2881	. . . 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 32	. . 3 |- ( S e. (SubRing ` ℂfld ) -> ( f e. (Poly ` S ) -> f e. ( E " A ) ) )
149		ffun 5641	. . . . . 6 |- ( E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) -> Fun E )
150	96, 149	ax-mp 5	. . . . 5 |- Fun E
151		fvelima 5826	. . . . 5 |- ( ( Fun E /\ f e. ( E " A ) ) -> E. a e. A ( E ` a ) = f )
152	150, 151	mpan 668	. . . 4 |- ( f e. ( E " A ) -> E. a e. A ( E ` a ) = f )
153	100	sselda 3417	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> a e. ( Base ` (Poly1 ` ℂfld ) ) )
154		eqid 2382	. . . . . . . . . . . 12 |- ( .s ` (Poly1 ` ℂfld ) ) = ( .s ` (Poly1 ` ℂfld ) )
155		eqid 2382	. . . . . . . . . . . 12 |- (coe1 ` a ) = (coe1 ` a )
156	54, 115, 94, 154, 111, 117, 155	ply1coe 18450	. . . . . . . . . . 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 661	. . . . . . . . . 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 5778	. . . . . . . . 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 2382	. . . . . . . . . 10 |- ( 0g ` (Poly1 ` ℂfld ) ) = ( 0g ` (Poly1 ` ℂfld ) )
160	54	ply1ring 18402	. . . . . . . . . . . 12 |- (ℂfld e. Ring -> (Poly1 ` ℂfld ) e. Ring )
161	9, 160	ax-mp 5	. . . . . . . . . . 11 |- (Poly1 ` ℂfld ) e. Ring
162		ringcmn 17342	. . . . . . . . . . 11 |- ( (Poly1 ` ℂfld ) e. Ring -> (Poly1 ` ℂfld ) e. CMnd )
163	161, 162	mp1i 12	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (Poly1 ` ℂfld ) e. CMnd )
164		ringmnd 17320	. . . . . . . . . . 11 |- ( (ℂfld ^s CC ) e. Ring -> (ℂfld ^s CC ) e. Mnd )
165	49, 164	mp1i 12	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (ℂfld ^s CC ) e. Mnd )
166		nn0ex 10718	. . . . . . . . . . 11 |- NN0 e. _V
167	166	a1i 11	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> NN0 e. _V )
168		rhmghm 17487	. . . . . . . . . . . 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 16394	. . . . . . . . . . 11 |- ( E e. ( (Poly1 ` ℂfld ) GrpHom (ℂfld ^s CC ) ) -> E e. ( (Poly1 ` ℂfld ) MndHom (ℂfld ^s CC ) ) )
171	169, 170	mp1i 12	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> E e. ( (Poly1 ` ℂfld ) MndHom (ℂfld ^s CC ) ) )
172	54	ply1lmod 18406	. . . . . . . . . . . . 13 |- (ℂfld e. Ring -> (Poly1 ` ℂfld ) e. LMod )
173	9, 172	mp1i 12	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> (Poly1 ` ℂfld ) e. LMod )
174	12	ad2antrr 723	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> S C_ CC )
175		eqid 2382	. . . . . . . . . . . . . . . . 17 |- ( Base ` R ) = ( Base ` R )
176	155, 59, 58, 175	coe1f 18363	. . . . . . . . . . . . . . . 16 |- ( a e. A -> (coe1 ` a ) : NN0 --> ( Base ` R ) )
177	57	subrgbas 17551	. . . . . . . . . . . . . . . . 17 |- ( S e. (SubRing ` ℂfld ) -> S = ( Base ` R ) )
178	177	feq3d 5627	. . . . . . . . . . . . . . . 16 |- ( S e. (SubRing ` ℂfld ) -> ( (coe1 ` a ) : NN0 --> S <-> (coe1 ` a ) : NN0 --> ( Base ` R ) ) )
179	176, 178	syl5ibr 221	. . . . . . . . . . . . . . 15 |- ( S e. (SubRing ` ℂfld ) -> ( a e. A -> (coe1 ` a ) : NN0 --> S ) )
180	179	imp 427	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) : NN0 --> S )
181	180	ffvelrnda 5933	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. S )
182	174, 181	sseldd 3418	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. CC )
183	111	ringmgp 17317	. . . . . . . . . . . . . 14 |- ( (Poly1 ` ℂfld ) e. Ring -> (mulGrp ` (Poly1 ` ℂfld ) ) e. Mnd )
184	161, 183	mp1i 12	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> (mulGrp ` (Poly1 ` ℂfld ) ) e. Mnd )
185		simpr 459	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> k e. NN0 )
186	115, 54, 94	vr1cl 18371	. . . . . . . . . . . . . 14 |- (ℂfld e. Ring -> (var1 ` ℂfld ) e. ( Base ` (Poly1 ` ℂfld ) ) )
187	9, 186	mp1i 12	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> (var1 ` ℂfld ) e. ( Base ` (Poly1 ` ℂfld ) ) )
188	111, 94	mgpbas 17260	. . . . . . . . . . . . . 14 |- ( Base ` (Poly1 ` ℂfld ) ) = ( Base ` (mulGrp ` (Poly1 ` ℂfld ) ) )
189	188, 117	mulgnn0cl 16275	. . . . . . . . . . . . 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 1226	. . . . . . . . . . . 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 18407	. . . . . . . . . . . . . 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 17642	. . . . . . . . . . . 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 1226	. . . . . . . . . . 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 2382	. . . . . . . . . . 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 5957	. . . . . . . . . 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 6044	. . . . . . . . . . . . 13 |- ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) e. _V
198		funmpt 5532	. . . . . . . . . . . . 13 |- Fun ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) )
199		fvex 5784	. . . . . . . . . . . . 13 |- ( 0g ` (Poly1 ` ℂfld ) ) e. _V
200	197, 198, 199	3pm3.2i 1172	. . . . . . . . . . . 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 18365	. . . . . . . . . . . . 13 |- ( a e. ( Base ` (Poly1 ` ℂfld ) ) -> (coe1 ` a ) finSupp 0 )
203	153, 202	syl 16	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) finSupp 0 )
204	203	fsuppimpd 7751	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (coe1 ` a ) supp 0 ) e. Fin )
205	180	feqmptd 5827	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) = ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) )
206	205	oveq1d 6211	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (coe1 ` a ) supp 0 ) = ( ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) supp 0 ) )
207		eqimss2 3470	. . . . . . . . . . . . 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 16	. . . . . . . . . . . 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 12	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (Poly1 ` ℂfld ) e. LMod )
210	94, 192, 154, 17, 159	lmod0vs 17658	. . . . . . . . . . . . 13 |- ( ( (Poly1 ` ℂfld ) e. LMod /\ x e. ( Base ` (Poly1 ` ℂfld ) ) ) -> ( 0 ( .s ` (Poly1 ` ℂfld ) ) x ) = ( 0g ` (Poly1 ` ℂfld ) ) )
211	209, 210	sylan 469	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ x e. ( Base ` (Poly1 ` ℂfld ) ) ) -> ( 0 ( .s ` (Poly1 ` ℂfld ) ) x ) = ( 0g ` (Poly1 ` ℂfld ) ) )
212		c0ex 9501	. . . . . . . . . . . . 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 6850	. . . . . . . . . . 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 7759	. . . . . . . . . . 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 1224	. . . . . . . . . 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 17075	. . . . . . . . 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 2383	. . . . . . . . . . . 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 5827	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> E = ( x e. ( Base ` (Poly1 ` ℂfld ) ) |-> ( E ` x ) ) )
221		fveq2 5774	. . . . . . . . . . . 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 5966	. . . . . . . . . . 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 5932	. . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . 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 14896	. . . . . . . . . . . . . 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 5827	. . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . 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 18486	. . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . 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 18494	. . . . . . . . . . . . . . . . 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 659	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( k (.g ` (mulGrp ` ℂfld ) ) z ) = ( z ^ k ) )
235	234	eqeq2d 2396	. . . . . . . . . . . . . . . . . 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 701	. . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . 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 18493	. . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . 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 4453	. . . . . . . . . . . . 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 2423	. . . . . . . . . . . 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 4453	. . . . . . . . . . 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 2423	. . . . . . . . . 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 6212	. . . . . . . . 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 2429	. . . . . . . 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 12	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ℂfld e. CMnd )
249	182	adantlr 712	. . . . . . . . . . 11 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. CC )
250	33	adantll 711	. . . . . . . . . . 11 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( z ^ k ) e. CC )
251	249, 250	mulcld 9527	. . . . . . . . . 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 645	. . . . . . . . 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 6044	. . . . . . . . . . . 12 |- ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V
254		funmpt 5532	. . . . . . . . . . . 12 |- Fun ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
255	253, 254, 39	3pm3.2i 1172	. . . . . . . . . . 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 11986	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) e. Fin )
258		eldifn 3541	. . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . . . . . . . . . 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 3540	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) -> k e. NN0 )
262	261	adantl 464	. . . . . . . . . . . . . . . . . . . . . 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 2382	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( deg1 ` ℂfld ) = ( deg1 ` ℂfld )
264	263, 54, 94, 17, 155	deg1ge 22584	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( a e. ( Base ` (Poly1 ` ℂfld ) ) /\ k e. NN0 /\ ( (coe1 ` a ) ` k ) =/= 0 ) -> k <_ ( ( deg1 ` ℂfld ) ` a ) )
265	264	3expia 1196	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a e. ( Base ` (Poly1 ` ℂfld ) ) /\ k e. NN0 ) -> ( ( (coe1 ` a ) ` k ) =/= 0 -> k <_ ( ( deg1 ` ℂfld ) ` a ) ) )
266	260, 262, 265	syl2anc 659	. . . . . . . . . . . . . . . . . . . . 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 9551	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. RR*
268	263, 54, 94	deg1xrcl 22567	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a e. ( Base ` (Poly1 ` ℂfld ) ) -> ( ( deg1 ` ℂfld ) ` a ) e. RR* )
269	153, 268	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( deg1 ` ℂfld ) ` a ) e. RR* )
270	269	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 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 11298	. . . . . . . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . . . . . . 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 10770	. . . . . . . . . . . . . . . . . . . . . . . 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 9554	. . . . . . . . . . . . . . . . . . . . . . 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 3899	. . . . . . . . . . . . . . . . . . . . . . . 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 660	. . . . . . . . . . . . . . . . . . . . . . 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 11282	. . . . . . . . . . . . . . . . . . . . . . 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 1226	. . . . . . . . . . . . . . . . . . . . . 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 672	. . . . . . . . . . . . . . . . . . . . 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 44	. . . . . . . . . . . . . . . . . . . 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 541	. . . . . . . . . . . . . . . . . . 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 22568	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( a e. ( Base ` (Poly1 ` ℂfld ) ) -> ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) )
283	153, 282	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) )
284		elun 3559	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) <-> ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) )
285	283, 284	sylib 196	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) )
286		nn0ge0 10738	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> 0 <_ ( ( deg1 ` ℂfld ) ` a ) )
287	286	iftrued 3865	. . . . . . . . . . . . . . . . . . . . . . . 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 2470	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
290		mnflt0 11255	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- -oo < 0
291		mnfxr 11244	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- -oo e. RR*
292		xrltnle 9564	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( -oo e. RR* /\ 0 e. RR* ) -> ( -oo < 0 <-> -. 0 <_ -oo ) )
293	291, 267, 292	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -oo < 0 <-> -. 0 <_ -oo )
294	290, 293	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- -. 0 <_ -oo
295		elsni 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> ( ( deg1 ` ℂfld ) ` a ) = -oo )
296	295	breq2d 4379	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) <-> 0 <_ -oo ) )
297	294, 296	mtbiri 301	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> -. 0 <_ ( ( deg1 ` ℂfld ) ` a ) )
298	297	iffalsed 3868	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = 0 )
299		0nn0 10727	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. NN0
300	298, 299	syl6eqel 2478	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
301	289, 300	jaoi 377	. . . . . . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
303	302	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 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 11692	. . . . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . . . 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 234	. . . . . . . . . . . . . . . . . 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 2600	. . . . . . . . . . . . . . . . 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 6211	. . . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . . . 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 9689	. . . . . . . . . . . . . . 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 2423	. . . . . . . . . . . . . 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 802	. . . . . . . . . . . . 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 4453	. . . . . . . . . . . 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 4957	. . . . . . . . . . . . 13 |- ( CC X. { 0 } ) = ( z e. CC |-> 0 )
316		ringmnd 17320	. . . . . . . . . . . . . . 15 |- (ℂfld e. Ring -> ℂfld e. Mnd )
317	9, 316	ax-mp 5	. . . . . . . . . . . . . 14 |- ℂfld e. Mnd
318	3, 17	pws0g 16073	. . . . . . . . . . . . . 14 |- ( (ℂfld e. Mnd /\ CC e. _V ) -> ( CC X. { 0 } ) = ( 0g ` (ℂfld ^s CC ) ) )
319	317, 6, 318	mp2an 670	. . . . . . . . . . . . 13 |- ( CC X. { 0 } ) = ( 0g ` (ℂfld ^s CC ) )
320	315, 319	eqtr3i 2413	. . . . . . . . . . . 12 |- ( z e. CC |-> 0 ) = ( 0g ` (ℂfld ^s CC ) )
321	314, 320	syl6eq 2439	. . . . . . . . . . 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 6852	. . . . . . . . . 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 7759	. . . . . . . . . 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 1224	. . . . . . . . 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 17122	. . . . . . . 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 11693	. . . . . . . . . . . . 13 |- ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) -> k e. NN0 )
327	326	ssriv 3421	. . . . . . . . . . . 12 |- ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) C_ NN0
328		resmpt 5235	. . . . . . . . . . . 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 6207	. . . . . . . . . 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 12	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) -> ℂfld e. CMnd )
332	166	a1i 11	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing