Theorem plypf1 22337

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 22320	. . . . 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 464	. . . 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 2460	. . . . . . . . 9 |- (ℂfld ^s CC ) = (ℂfld ^s CC )
4		cnfldbas 18188	. . . . . . . . 9 |- CC = ( Base ` ℂfld )
5		eqid 2460	. . . . . . . . 9 |- ( 0g ` (ℂfld ^s CC ) ) = ( 0g ` (ℂfld ^s CC ) )
6		cnex 9562	. . . . . . . . . 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 12039	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( 0 ... n ) e. Fin )
9		cnrng 18204	. . . . . . . . . 10 |- ℂfld e. Ring
10		rngcmn 17009	. . . . . . . . . 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 17206	. . . . . . . . . . . . 13 |- ( S e. (SubRing ` ℂfld ) -> S C_ CC )
13	12	ad2antrr 725	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> S C_ CC )
14		elmapi 7430	. . . . . . . . . . . . . . 15 |- ( a e. ( ( S u. { 0 } ) ^m NN0 ) -> a : NN0 --> ( S u. { 0 } ) )
15	14	ad2antll 728	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> a : NN0 --> ( S u. { 0 } ) )
16		subrgsubg 17211	. . . . . . . . . . . . . . . . . . 19 |- ( S e. (SubRing ` ℂfld ) -> S e. (SubGrp ` ℂfld ) )
17		cnfld0 18206	. . . . . . . . . . . . . . . . . . . 20 |- 0 = ( 0g ` ℂfld )
18	17	subg0cl 15997	. . . . . . . . . . . . . . . . . . 19 |- ( S e. (SubGrp ` ℂfld ) -> 0 e. S )
19	16, 18	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( S e. (SubRing ` ℂfld ) -> 0 e. S )
20	19	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> 0 e. S )
21	20	snssd 4165	. . . . . . . . . . . . . . . 16 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> { 0 } C_ S )
22		ssequn2 3670	. . . . . . . . . . . . . . . 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		feq3 5706	. . . . . . . . . . . . . . 15 |- ( ( S u. { 0 } ) = S -> ( a : NN0 --> ( S u. { 0 } ) <-> a : NN0 --> S ) )
25	23, 24	syl 16	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( a : NN0 --> ( S u. { 0 } ) <-> a : NN0 --> S ) )
26	15, 25	mpbid 210	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> a : NN0 --> S )
27		elfznn0 11759	. . . . . . . . . . . . 13 |- ( k e. ( 0 ... n ) -> k e. NN0 )
28		ffvelrn 6010	. . . . . . . . . . . . 13 |- ( ( a : NN0 --> S /\ k e. NN0 ) -> ( a ` k ) e. S )
29	26, 27, 28	syl2an 477	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( a ` k ) e. S )
30	13, 29	sseldd 3498	. . . . . . . . . . 11 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( a ` k ) e. CC )
31	30	adantrl 715	. . . . . . . . . 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 )
32		simprl 755	. . . . . . . . . . 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 )
33	27	ad2antll 728	. . . . . . . . . . 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 )
34		expcl 12140	. . . . . . . . . . 11 |- ( ( z e. CC /\ k e. NN0 ) -> ( z ^ k ) e. CC )
35	32, 33, 34	syl2anc 661	. . . . . . . . . 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 )
36	31, 35	mulcld 9605	. . . . . . . . 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 )
37		eqid 2460	. . . . . . . . . 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 ) ) ) )
38	6	mptex 6122	. . . . . . . . . . 11 |- ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) e. _V
39	38	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 )
40		fvex 5867	. . . . . . . . . . 11 |- ( 0g ` (ℂfld ^s CC ) ) e. _V
41	40	a1i 11	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( 0g ` (ℂfld ^s CC ) ) e. _V )
42	37, 8, 39, 41	fsuppmptdm 7829	. . . . . . . . 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 ) ) )
43	3, 4, 5, 7, 8, 11, 36, 42	pwsgsum 16793	. . . . . . . 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 ) ) ) ) ) )
44		fzfid 12039	. . . . . . . . . 10 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) -> ( 0 ... n ) e. Fin )
45	36	anassrs 648	. . . . . . . . . 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 )
46	44, 45	gsumfsum 18245	. . . . . . . . 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 ) ) )
47	46	mpteq2dva 4526	. . . . . . . 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 ) ) ) )
48	43, 47	eqtrd 2501	. . . . . . 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 ) ) ) )
49	3	pwsrng 17041	. . . . . . . . . 10 |- ( (ℂfld e. Ring /\ CC e. _V ) -> (ℂfld ^s CC ) e. Ring )
50	9, 6, 49	mp2an 672	. . . . . . . . 9 |- (ℂfld ^s CC ) e. Ring
51		rngcmn 17009	. . . . . . . . 9 |- ( (ℂfld ^s CC ) e. Ring -> (ℂfld ^s CC ) e. CMnd )
52	50, 51	mp1i 12	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> (ℂfld ^s CC ) e. CMnd )
53		cncrng 18203	. . . . . . . . . . 11 |- ℂfld e. CRing
54		plypf1.e	. . . . . . . . . . . 12 |- E = (eval1 ` ℂfld )
55		eqid 2460	. . . . . . . . . . . 12 |- (Poly1 ` ℂfld ) = (Poly1 ` ℂfld )
56	54, 55, 3, 4	evl1rhm 18132	. . . . . . . . . . 11 |- (ℂfld e. CRing -> E e. ( (Poly1 ` ℂfld ) RingHom (ℂfld ^s CC ) ) )
57	53, 56	ax-mp 5	. . . . . . . . . 10 |- E e. ( (Poly1 ` ℂfld ) RingHom (ℂfld ^s CC ) )
58		plypf1.r	. . . . . . . . . . . 12 |- R = (ℂfld ↾s S )
59		plypf1.p	. . . . . . . . . . . 12 |- P = (Poly1 ` R )
60		plypf1.a	. . . . . . . . . . . 12 |- A = ( Base ` P )
61	55, 58, 59, 60	subrgply1 18038	. . . . . . . . . . 11 |- ( S e. (SubRing ` ℂfld ) -> A e. (SubRing ` (Poly1 ` ℂfld ) ) )
62	61	adantr 465	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> A e. (SubRing ` (Poly1 ` ℂfld ) ) )
63		rhmima 17236	. . . . . . . . . 10 |- ( ( E e. ( (Poly1 ` ℂfld ) RingHom (ℂfld ^s CC ) ) /\ A e. (SubRing ` (Poly1 ` ℂfld ) ) ) -> ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) )
64	57, 62, 63	sylancr 663	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) )
65		subrgsubg 17211	. . . . . . . . 9 |- ( ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) -> ( E " A ) e. (SubGrp ` (ℂfld ^s CC ) ) )
66		subgsubm 16011	. . . . . . . . 9 |- ( ( E " A ) e. (SubGrp ` (ℂfld ^s CC ) ) -> ( E " A ) e. (SubMnd ` (ℂfld ^s CC ) ) )
67	64, 65, 66	3syl 20	. . . . . . . 8 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( E " A ) e. (SubMnd ` (ℂfld ^s CC ) ) )
68		eqid 2460	. . . . . . . . . . . 12 |- ( Base ` (ℂfld ^s CC ) ) = ( Base ` (ℂfld ^s CC ) )
69	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 )
70	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 )
71		fconst6g 5765	. . . . . . . . . . . . . 14 |- ( ( a ` k ) e. CC -> ( CC X. { ( a ` k ) } ) : CC --> CC )
72	30, 71	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 )
73	3, 4, 68	pwselbasb 14732	. . . . . . . . . . . . . 14 |- ( (ℂfld e. Ring /\ CC e. _V ) -> ( ( CC X. { ( a ` k ) } ) e. ( Base ` (ℂfld ^s CC ) ) <-> ( CC X. { ( a ` k ) } ) : CC --> CC ) )
74	9, 6, 73	mp2an 672	. . . . . . . . . . . . 13 |- ( ( CC X. { ( a ` k ) } ) e. ( Base ` (ℂfld ^s CC ) ) <-> ( CC X. { ( a ` k ) } ) : CC --> CC )
75	72, 74	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 ) ) )
76	35	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 )
77		eqid 2460	. . . . . . . . . . . . . 14 |- ( z e. CC |-> ( z ^ k ) ) = ( z e. CC |-> ( z ^ k ) )
78	76, 77	fmptd 6036	. . . . . . . . . . . . 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 )
79	3, 4, 68	pwselbasb 14732	. . . . . . . . . . . . . 14 |- ( (ℂfld e. Ring /\ CC e. _V ) -> ( ( z e. CC |-> ( z ^ k ) ) e. ( Base ` (ℂfld ^s CC ) ) <-> ( z e. CC |-> ( z ^ k ) ) : CC --> CC ) )
80	9, 6, 79	mp2an 672	. . . . . . . . . . . . 13 |- ( ( z e. CC |-> ( z ^ k ) ) e. ( Base ` (ℂfld ^s CC ) ) <-> ( z e. CC |-> ( z ^ k ) ) : CC --> CC )
81	78, 80	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 ) ) )
82		cnfldmul 18190	. . . . . . . . . . . 12 |- x. = ( .r ` ℂfld )
83		eqid 2460	. . . . . . . . . . . 12 |- ( .r ` (ℂfld ^s CC ) ) = ( .r ` (ℂfld ^s CC ) )
84	3, 68, 69, 70, 75, 81, 82, 83	pwsmulrval 14735	. . . . . . . . . . 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 ) ) ) )
85	30	adantr 465	. . . . . . . . . . . 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 )
86		fconstmpt 5035	. . . . . . . . . . . . 13 |- ( CC X. { ( a ` k ) } ) = ( z e. CC |-> ( a ` k ) )
87	86	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 ) ) )
88		eqidd 2461	. . . . . . . . . . . 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 ) ) )
89	70, 85, 76, 87, 88	offval2 6531	. . . . . . . . . . 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 ) ) ) )
90	84, 89	eqtrd 2501	. . . . . . . . . 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 ) ) ) )
91	64	adantr 465	. . . . . . . . . . 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 ) ) )
92		eqid 2460	. . . . . . . . . . . . . 14 |- (algSc ` (Poly1 ` ℂfld ) ) = (algSc ` (Poly1 ` ℂfld ) )
93	54, 55, 4, 92	evl1sca 18134	. . . . . . . . . . . . 13 |- ( (ℂfld e. CRing /\ ( a ` k ) e. CC ) -> ( E ` ( (algSc ` (Poly1 ` ℂfld ) ) ` ( a ` k ) ) ) = ( CC X. { ( a ` k ) } ) )
94	53, 30, 93	sylancr 663	. . . . . . . . . . . 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 ) } ) )
95		eqid 2460	. . . . . . . . . . . . . . . 16 |- ( Base ` (Poly1 ` ℂfld ) ) = ( Base ` (Poly1 ` ℂfld ) )
96	95, 68	rhmf 17152	. . . . . . . . . . . . . . 15 |- ( E e. ( (Poly1 ` ℂfld ) RingHom (ℂfld ^s CC ) ) -> E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) )
97	57, 96	ax-mp 5	. . . . . . . . . . . . . 14 |- E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) )
98		ffn 5722	. . . . . . . . . . . . . 14 |- ( E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) -> E Fn ( Base ` (Poly1 ` ℂfld ) ) )
99	97, 98	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 ) ) )
100	95	subrgss 17206	. . . . . . . . . . . . . . 15 |- ( A e. (SubRing ` (Poly1 ` ℂfld ) ) -> A C_ ( Base ` (Poly1 ` ℂfld ) ) )
101	61, 100	syl 16	. . . . . . . . . . . . . 14 |- ( S e. (SubRing ` ℂfld ) -> A C_ ( Base ` (Poly1 ` ℂfld ) ) )
102	101	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> A C_ ( Base ` (Poly1 ` ℂfld ) ) )
103		simpll 753	. . . . . . . . . . . . . . 15 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> S e. (SubRing ` ℂfld ) )
104	55, 92, 58, 59, 103, 60, 4, 30	subrg1asclcl 18065	. . . . . . . . . . . . . 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 ) )
105	29, 104	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 )
106		fnfvima 6129	. . . . . . . . . . . . 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 ) )
107	99, 102, 105, 106	syl3anc 1223	. . . . . . . . . . . 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 ) )
108	94, 107	eqeltrrd 2549	. . . . . . . . . . 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 ) )
109	68	subrgss 17206	. . . . . . . . . . . . . . . . 17 |- ( ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) -> ( E " A ) C_ ( Base ` (ℂfld ^s CC ) ) )
110	91, 109	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 ) ) )
111	61	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> A e. (SubRing ` (Poly1 ` ℂfld ) ) )
112		eqid 2460	. . . . . . . . . . . . . . . . . . . 20 |- (mulGrp ` (Poly1 ` ℂfld ) ) = (mulGrp ` (Poly1 ` ℂfld ) )
113	112	subrgsubm 17218	. . . . . . . . . . . . . . . . . . 19 |- ( A e. (SubRing ` (Poly1 ` ℂfld ) ) -> A e. (SubMnd ` (mulGrp ` (Poly1 ` ℂfld ) ) ) )
114	111, 113	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 ) ) ) )
115	27	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> k e. NN0 )
116		eqid 2460	. . . . . . . . . . . . . . . . . . 19 |- (var1 ` ℂfld ) = (var1 ` ℂfld )
117	116, 103, 58, 59, 60	subrgvr1cl 18067	. . . . . . . . . . . . . . . . . 18 |- ( ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> (var1 ` ℂfld ) e. A )
118		eqid 2460	. . . . . . . . . . . . . . . . . . 19 |- (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) = (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) )
119	118	submmulgcl 15969	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. (SubMnd ` (mulGrp ` (Poly1 ` ℂfld ) ) ) /\ k e. NN0 /\ (var1 ` ℂfld ) e. A ) -> ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. A )
120	114, 115, 117, 119	syl3anc 1223	. . . . . . . . . . . . . . . . 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 )
121		fnfvima 6129	. . . . . . . . . . . . . . . . 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 ) )
122	99, 102, 120, 121	syl3anc 1223	. . . . . . . . . . . . . . . 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 ) )
123	110, 122	sseldd 3498	. . . . . . . . . . . . . . 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 ) ) )
124	3, 4, 68, 69, 70, 123	pwselbas 14733	. . . . . . . . . . . . . 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 )
125	124	feqmptd 5911	. . . . . . . . . . . . 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 ) ) )
126	53	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 )
127		simpr 461	. . . . . . . . . . . . . . . . 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 )
128	54, 116, 4, 55, 95, 126, 127	evl1vard 18137	. . . . . . . . . . . . . . . . 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 ) )
129		eqid 2460	. . . . . . . . . . . . . . . . 17 |- (.g ` (mulGrp ` ℂfld ) ) = (.g ` (mulGrp ` ℂfld ) )
130	115	adantr 465	. . . . . . . . . . . . . . . . 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 )
131	54, 55, 4, 95, 126, 127, 128, 118, 129, 130	evl1expd 18145	. . . . . . . . . . . . . . . 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 ) ) )
132	131	simprd 463	. . . . . . . . . . . . . . 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 ) )
133		cnfldexp 18215	. . . . . . . . . . . . . . . 16 |- ( ( z e. CC /\ k e. NN0 ) -> ( k (.g ` (mulGrp ` ℂfld ) ) z ) = ( z ^ k ) )
134	127, 130, 133	syl2anc 661	. . . . . . . . . . . . . . 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 ) )
135	132, 134	eqtrd 2501	. . . . . . . . . . . . . 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 ) )
136	135	mpteq2dva 4526	. . . . . . . . . . . . 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 ) ) )
137	125, 136	eqtrd 2501	. . . . . . . . . . . 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 ) ) )
138	137, 122	eqeltrrd 2549	. . . . . . . . . . 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 ) )
139	83	subrgmcl 17217	. . . . . . . . . . 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 ) )
140	91, 108, 138, 139	syl3anc 1223	. . . . . . . . . 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 ) )
141	90, 140	eqeltrrd 2549	. . . . . . . . 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 ) )
142	141, 37	fmptd 6036	. . . . . . . 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 ) )
143	37, 8, 141, 41	fsuppmptdm 7829	. . . . . . . 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 ) ) )
144	5, 52, 8, 67, 142, 143	gsumsubmcl 16714	. . . . . . 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 ) )
145	48, 144	eqeltrrd 2549	. . . . . 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 ) )
146		eleq1 2532	. . . . . 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 ) ) )
147	145, 146	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 ) ) )
148	147	rexlimdvva 2955	. . . 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 ) ) )
149	2, 148	syl5 32	. . 3 |- ( S e. (SubRing ` ℂfld ) -> ( f e. (Poly ` S ) -> f e. ( E " A ) ) )
150		ffun 5724	. . . . . 6 |- ( E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) -> Fun E )
151	97, 150	ax-mp 5	. . . . 5 |- Fun E
152		fvelima 5910	. . . . 5 |- ( ( Fun E /\ f e. ( E " A ) ) -> E. a e. A ( E ` a ) = f )
153	151, 152	mpan 670	. . . 4 |- ( f e. ( E " A ) -> E. a e. A ( E ` a ) = f )
154	101	sselda 3497	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> a e. ( Base ` (Poly1 ` ℂfld ) ) )
155		eqid 2460	. . . . . . . . . . . 12 |- ( .s ` (Poly1 ` ℂfld ) ) = ( .s ` (Poly1 ` ℂfld ) )
156		eqid 2460	. . . . . . . . . . . 12 |- (coe1 ` a ) = (coe1 ` a )
157	55, 116, 95, 155, 112, 118, 156	ply1coe 18101	. . . . . . . . . . 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 ) ) ) ) ) )
158	9, 154, 157	sylancr 663	. . . . . . . . . 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 ) ) ) ) ) )
159	158	fveq2d 5861	. . . . . . . . 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 ) ) ) ) ) ) )
160		eqid 2460	. . . . . . . . . 10 |- ( 0g ` (Poly1 ` ℂfld ) ) = ( 0g ` (Poly1 ` ℂfld ) )
161	55	ply1rng 18053	. . . . . . . . . . . 12 |- (ℂfld e. Ring -> (Poly1 ` ℂfld ) e. Ring )
162	9, 161	ax-mp 5	. . . . . . . . . . 11 |- (Poly1 ` ℂfld ) e. Ring
163		rngcmn 17009	. . . . . . . . . . 11 |- ( (Poly1 ` ℂfld ) e. Ring -> (Poly1 ` ℂfld ) e. CMnd )
164	162, 163	mp1i 12	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (Poly1 ` ℂfld ) e. CMnd )
165		rngmnd 16988	. . . . . . . . . . 11 |- ( (ℂfld ^s CC ) e. Ring -> (ℂfld ^s CC ) e. Mnd )
166	50, 165	mp1i 12	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (ℂfld ^s CC ) e. Mnd )
167		nn0ex 10790	. . . . . . . . . . 11 |- NN0 e. _V
168	167	a1i 11	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> NN0 e. _V )
169		rhmghm 17151	. . . . . . . . . . . 12 |- ( E e. ( (Poly1 ` ℂfld ) RingHom (ℂfld ^s CC ) ) -> E e. ( (Poly1 ` ℂfld ) GrpHom (ℂfld ^s CC ) ) )
170	57, 169	ax-mp 5	. . . . . . . . . . 11 |- E e. ( (Poly1 ` ℂfld ) GrpHom (ℂfld ^s CC ) )
171		ghmmhm 16065	. . . . . . . . . . 11 |- ( E e. ( (Poly1 ` ℂfld ) GrpHom (ℂfld ^s CC ) ) -> E e. ( (Poly1 ` ℂfld ) MndHom (ℂfld ^s CC ) ) )
172	170, 171	mp1i 12	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> E e. ( (Poly1 ` ℂfld ) MndHom (ℂfld ^s CC ) ) )
173	55	ply1lmod 18057	. . . . . . . . . . . . 13 |- (ℂfld e. Ring -> (Poly1 ` ℂfld ) e. LMod )
174	9, 173	mp1i 12	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> (Poly1 ` ℂfld ) e. LMod )
175	12	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> S C_ CC )
176		eqid 2460	. . . . . . . . . . . . . . . . 17 |- ( Base ` R ) = ( Base ` R )
177	156, 60, 59, 176	coe1f 18014	. . . . . . . . . . . . . . . 16 |- ( a e. A -> (coe1 ` a ) : NN0 --> ( Base ` R ) )
178	58	subrgbas 17214	. . . . . . . . . . . . . . . . 17 |- ( S e. (SubRing ` ℂfld ) -> S = ( Base ` R ) )
179		feq3 5706	. . . . . . . . . . . . . . . . 17 |- ( S = ( Base ` R ) -> ( (coe1 ` a ) : NN0 --> S <-> (coe1 ` a ) : NN0 --> ( Base ` R ) ) )
180	178, 179	syl 16	. . . . . . . . . . . . . . . 16 |- ( S e. (SubRing ` ℂfld ) -> ( (coe1 ` a ) : NN0 --> S <-> (coe1 ` a ) : NN0 --> ( Base ` R ) ) )
181	177, 180	syl5ibr 221	. . . . . . . . . . . . . . 15 |- ( S e. (SubRing ` ℂfld ) -> ( a e. A -> (coe1 ` a ) : NN0 --> S ) )
182	181	imp 429	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) : NN0 --> S )
183	182	ffvelrnda 6012	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. S )
184	175, 183	sseldd 3498	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. CC )
185	112	rngmgp 16985	. . . . . . . . . . . . . 14 |- ( (Poly1 ` ℂfld ) e. Ring -> (mulGrp ` (Poly1 ` ℂfld ) ) e. Mnd )
186	162, 185	mp1i 12	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> (mulGrp ` (Poly1 ` ℂfld ) ) e. Mnd )
187		simpr 461	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> k e. NN0 )
188	116, 55, 95	vr1cl 18022	. . . . . . . . . . . . . 14 |- (ℂfld e. Ring -> (var1 ` ℂfld ) e. ( Base ` (Poly1 ` ℂfld ) ) )
189	9, 188	mp1i 12	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> (var1 ` ℂfld ) e. ( Base ` (Poly1 ` ℂfld ) ) )
190	112, 95	mgpbas 16930	. . . . . . . . . . . . . 14 |- ( Base ` (Poly1 ` ℂfld ) ) = ( Base ` (mulGrp ` (Poly1 ` ℂfld ) ) )
191	190, 118	mulgnn0cl 15951	. . . . . . . . . . . . 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 ) ) )
192	186, 187, 189, 191	syl3anc 1223	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. ( Base ` (Poly1 ` ℂfld ) ) )
193	55	ply1sca 18058	. . . . . . . . . . . . . 14 |- (ℂfld e. Ring -> ℂfld = (Scalar ` (Poly1 ` ℂfld ) ) )
194	9, 193	ax-mp 5	. . . . . . . . . . . . 13 |- ℂfld = (Scalar ` (Poly1 ` ℂfld ) )
195	95, 194, 155, 4	lmodvscl 17305	. . . . . . . . . . . 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 ) ) )
196	174, 184, 192, 195	syl3anc 1223	. . . . . . . . . . 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 ) ) )
197		eqid 2460	. . . . . . . . . . 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 ) ) ) )
198	196, 197	fmptd 6036	. . . . . . . . . 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 ) ) )
199	167	mptex 6122	. . . . . . . . . . . . 13 |- ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) e. _V
200		funmpt 5615	. . . . . . . . . . . . 13 |- Fun ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) )
201		fvex 5867	. . . . . . . . . . . . 13 |- ( 0g ` (Poly1 ` ℂfld ) ) e. _V
202	199, 200, 201	3pm3.2i 1169	. . . . . . . . . . . 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 )
203	202	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 ) )
204	156, 95, 55, 17	coe1sfi 18016	. . . . . . . . . . . . 13 |- ( a e. ( Base ` (Poly1 ` ℂfld ) ) -> (coe1 ` a ) finSupp 0 )
205	154, 204	syl 16	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) finSupp 0 )
206	205	fsuppimpd 7825	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (coe1 ` a ) supp 0 ) e. Fin )
207	182	feqmptd 5911	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) = ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) )
208	207	oveq1d 6290	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (coe1 ` a ) supp 0 ) = ( ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) supp 0 ) )
209		eqimss2 3550	. . . . . . . . . . . . 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 ) )
210	208, 209	syl 16	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) supp 0 ) C_ ( (coe1 ` a ) supp 0 ) )
211	9, 173	mp1i 12	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (Poly1 ` ℂfld ) e. LMod )
212	95, 194, 155, 17, 160	lmod0vs 17321	. . . . . . . . . . . . 13 |- ( ( (Poly1 ` ℂfld ) e. LMod /\ x e. ( Base ` (Poly1 ` ℂfld ) ) ) -> ( 0 ( .s ` (Poly1 ` ℂfld ) ) x ) = ( 0g ` (Poly1 ` ℂfld ) ) )
213	211, 212	sylan 471	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ x e. ( Base ` (Poly1 ` ℂfld ) ) ) -> ( 0 ( .s ` (Poly1 ` ℂfld ) ) x ) = ( 0g ` (Poly1 ` ℂfld ) ) )
214		c0ex 9579	. . . . . . . . . . . . 13 |- 0 e. _V
215	214	a1i 11	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> 0 e. _V )
216	210, 213, 183, 192, 215	suppssov1 6922	. . . . . . . . . . 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 ) )
217		suppssfifsupp 7833	. . . . . . . . . . 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 ) ) )
218	203, 206, 216, 217	syl12anc 1221	. . . . . . . . . 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 ) ) )
219	95, 160, 164, 166, 168, 172, 198, 218	gsummhm 16743	. . . . . . . . 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 ) ) ) ) ) ) )
220		eqidd 2461	. . . . . . . . . . . 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 ) ) ) ) )
221	97	a1i 11	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) )
222	221	feqmptd 5911	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> E = ( x e. ( Base ` (Poly1 ` ℂfld ) ) |-> ( E ` x ) ) )
223		fveq2 5857	. . . . . . . . . . . 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 ) ) ) ) )
224	196, 220, 222, 223	fmptco 6045	. . . . . . . . . . 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 ) ) ) ) ) )
225	9	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ℂfld e. Ring )
226	6	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> CC e. _V )
227	97	ffvelrni 6011	. . . . . . . . . . . . . . . 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 ) ) )
228	196, 227	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 ) ) )
229	3, 4, 68, 225, 226, 228	pwselbas 14733	. . . . . . . . . . . . . 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 )
230	229	feqmptd 5911	. . . . . . . . . . . . 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 ) ) )
231	53	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ℂfld e. CRing )
232		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> z e. CC )
233	54, 116, 4, 55, 95, 231, 232	evl1vard 18137	. . . . . . . . . . . . . . . . . 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 ) )
234	187	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> k e. NN0 )
235	54, 55, 4, 95, 231, 232, 233, 118, 129, 234	evl1expd 18145	. . . . . . . . . . . . . . . . 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 ) ) )
236	232, 234, 133	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( k (.g ` (mulGrp ` ℂfld ) ) z ) = ( z ^ k ) )
237	236	eqeq2d 2474	. . . . . . . . . . . . . . . . . 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 ) ) )
238	237	anbi2d 703	. . . . . . . . . . . . . . . . 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 ) ) ) )
239	235, 238	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 ) ) )
240	184	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( (coe1 ` a ) ` k ) e. CC )
241	54, 55, 4, 95, 231, 232, 239, 240, 155, 82	evl1vsd 18144	. . . . . . . . . . . . . . 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 ) ) ) )
242	241	simprd 463	. . . . . . . . . . . . . 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 ) ) )
243	242	mpteq2dva 4526	. . . . . . . . . . . . 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 ) ) ) )
244	230, 243	eqtrd 2501	. . . . . . . . . . . 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 ) ) ) )
245	244	mpteq2dva 4526	. . . . . . . . . . 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 ) ) ) ) )
246	224, 245	eqtrd 2501	. . . . . . . . . 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 ) ) ) ) )
247	246	oveq2d 6291	. . . . . . . . 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 ) ) ) ) ) )
248	159, 219, 247	3eqtr2d 2507	. . . . . . . 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 ) ) ) ) ) )
249	6	a1i 11	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> CC e. _V )
250	9, 10	mp1i 12	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ℂfld e. CMnd )
251	184	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. CC )
252	34	adantll 713	. . . . . . . . . . 11 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( z ^ k ) e. CC )
253	251, 252	mulcld 9605	. . . . . . . . . 10 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) e. CC )
254	253	anasss 647	. . . . . . . . 9 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ ( z e. CC /\ k e. NN0 ) ) -> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) e. CC )
255	167	mptex 6122	. . . . . . . . . . . 12 |- ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V
256		funmpt 5615	. . . . . . . . . . . 12 |- Fun ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
257	255, 256, 40	3pm3.2i 1169	. . . . . . . . . . 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 )
258	257	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 ) )
259		fzfid 12039	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) e. Fin )
260		eldifn 3620	. . . . . . . . . . . . . . . . . 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 ) ) )
261	260	adantl 466	. . . . . . . . . . . . . . . . 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 ) ) )
262	154	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 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 ) ) )
263		eldifi 3619	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) -> k e. NN0 )
264	263	adantl 466	. . . . . . . . . . . . . . . . . . . . . 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 )
265		eqid 2460	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( deg1 ` ℂfld ) = ( deg1 ` ℂfld )
266	265, 55, 95, 17, 156	deg1ge 22227	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( a e. ( Base ` (Poly1 ` ℂfld ) ) /\ k e. NN0 /\ ( (coe1 ` a ) ` k ) =/= 0 ) -> k <_ ( ( deg1 ` ℂfld ) ` a ) )
267	266	3expia 1193	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a e. ( Base ` (Poly1 ` ℂfld ) ) /\ k e. NN0 ) -> ( ( (coe1 ` a ) ` k ) =/= 0 -> k <_ ( ( deg1 ` ℂfld ) ` a ) ) )
268	262, 264, 267	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
269		0xr 9629	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. RR*
270	265, 55, 95	deg1xrcl 22210	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a e. ( Base ` (Poly1 ` ℂfld ) ) -> ( ( deg1 ` ℂfld ) ` a ) e. RR* )
271	154, 270	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( deg1 ` ℂfld ) ` a ) e. RR* )
272	271	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 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* )
273		xrmax2 11366	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 0 e. RR* /\ ( ( deg1 ` ℂfld ) ` a ) e. RR* ) -> ( ( deg1 ` ℂfld ) ` a ) <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) )
274	269, 272, 273	sylancr 663	. . . . . . . . . . . . . . . . . . . . . 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 ) )
275	264	nn0red 10842	. . . . . . . . . . . . . . . . . . . . . . . 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 )
276	275	rexrd 9632	. . . . . . . . . . . . . . . . . . . . . . 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* )
277		ifcl 3974	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( deg1 ` ℂfld ) ` a ) e. RR* /\ 0 e. RR* ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. RR* )
278	272, 269, 277	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . 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* )
279		xrletr 11350	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
280	276, 272, 278, 279	syl3anc 1223	. . . . . . . . . . . . . . . . . . . . . 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 ) ) )
281	274, 280	mpan2d 674	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
282	268, 281	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 ) ) )
283	282, 264	jctild 543	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
284	265, 55, 95	deg1cl 22211	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( a e. ( Base ` (Poly1 ` ℂfld ) ) -> ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) )
285	154, 284	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) )
286		elun 3638	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) <-> ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) )
287	285, 286	sylib 196	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) )
288		nn0ge0 10810	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> 0 <_ ( ( deg1 ` ℂfld ) ` a ) )
289		iftrue 3938	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = ( ( deg1 ` ℂfld ) ` a ) )
290	288, 289	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = ( ( deg1 ` ℂfld ) ` a ) )
291		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> ( ( deg1 ` ℂfld ) ` a ) e. NN0 )
292	290, 291	eqeltrd 2548	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
293		mnflt0 11323	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- -oo < 0
294		mnfxr 11312	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- -oo e. RR*
295		xrltnle 9642	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( -oo e. RR* /\ 0 e. RR* ) -> ( -oo < 0 <-> -. 0 <_ -oo ) )
296	294, 269, 295	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -oo < 0 <-> -. 0 <_ -oo )
297	293, 296	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- -. 0 <_ -oo
298		elsni 4045	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> ( ( deg1 ` ℂfld ) ` a ) = -oo )
299	298	breq2d 4452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) <-> 0 <_ -oo ) )
300	297, 299	mtbiri 303	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> -. 0 <_ ( ( deg1 ` ℂfld ) ` a ) )
301		iffalse 3941	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. 0 <_ ( ( deg1 ` ℂfld ) ` a ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = 0 )
302	300, 301	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = 0 )
303		0nn0 10799	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. NN0
304	302, 303	syl6eqel 2556	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
305	292, 304	jaoi 379	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
306	287, 305	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
307	306	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 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 )
308		fznn0 11758	. . . . . . . . . . . . . . . . . . . 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 ) ) ) )
309	307, 308	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 ) ) ) )
310	283, 309	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 ) ) ) )
311	310	necon1bd 2678	. . . . . . . . . . . . . . . . 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 ) )
312	261, 311	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 )
313	312	oveq1d 6290	. . . . . . . . . . . . . . 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 ) ) )
314	263, 252	sylan2 474	. . . . . . . . . . . . . . . 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 )
315	314	mul02d 9766	. . . . . . . . . . . . . . 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 )
316	313, 315	eqtrd 2501	. . . . . . . . . . . . . 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 )
317	316	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 )
318	317	mpteq2dva 4526	. . . . . . . . . . . 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 ) )
319		fconstmpt 5035	. . . . . . . . . . . . 13 |- ( CC X. { 0 } ) = ( z e. CC |-> 0 )
320		rngmnd 16988	. . . . . . . . . . . . . . 15 |- (ℂfld e. Ring -> ℂfld e. Mnd )
321	9, 320	ax-mp 5	. . . . . . . . . . . . . 14 |- ℂfld e. Mnd
322	3, 17	pws0g 15763	. . . . . . . . . . . . . 14 |- ( (ℂfld e. Mnd /\ CC e. _V ) -> ( CC X. { 0 } ) = ( 0g ` (ℂfld ^s CC ) ) )
323	321, 6, 322	mp2an 672	. . . . . . . . . . . . 13 |- ( CC X. { 0 } ) = ( 0g ` (ℂfld ^s CC ) )
324	319, 323	eqtr3i 2491	. . . . . . . . . . . 12 |- ( z e. CC |-> 0 ) = ( 0g ` (ℂfld ^s CC ) )
325	318, 324	syl6eq 2517	. . . . . . . . . . 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 ) ) )
326	325, 168	suppss2 6924	. . . . . . . . . 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 ) ) )
327		suppssfifsupp 7833	. . . . . . . . . 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 ) ) )
328	258, 259, 326, 327	syl12anc 1221	. . . . . . . . 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 ) ) )
329	3, 4, 5, 249, 168, 250, 254, 328	pwsgsum 16793	. . . . . . . 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 ) ) ) ) ) )
330		elfznn0 11759	. . . . . . . . . . . . 13 |- ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) -> k e. NN0 )
331	330	ssriv 3501	. . . . . . . . . . . 12 |- ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) C_ NN0
332		resmpt 5314	. . . . . . . . . . . 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 ) ) ) )
333	331, 332	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