Theorem plypf1 21649

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

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 21632	. . . . 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 2437	. . . . . . . . 9 |- (ℂfld ^s CC ) = (ℂfld ^s CC )
4		cnfldbas 17791	. . . . . . . . 9 |- CC = ( Base ` ℂfld )
5		eqid 2437	. . . . . . . . 9 |- ( 0g ` (ℂfld ^s CC ) ) = ( 0g ` (ℂfld ^s CC ) )
6		cnex 9355	. . . . . . . . . 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 11787	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( 0 ... n ) e. Fin )
9		cnrng 17807	. . . . . . . . . 10 |- ℂfld e. Ring
10		rngcmn 16661	. . . . . . . . . 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 16842	. . . . . . . . . . . . 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 7226	. . . . . . . . . . . . . . 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 16847	. . . . . . . . . . . . . . . . . . 19 |- ( S e. (SubRing ` ℂfld ) -> S e. (SubGrp ` ℂfld ) )
17		cnfld0 17809	. . . . . . . . . . . . . . . . . . . 20 |- 0 = ( 0g ` ℂfld )
18	17	subg0cl 15678	. . . . . . . . . . . . . . . . . . 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 4011	. . . . . . . . . . . . . . . 16 |- ( ( S e. (SubRing ` ℂfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> { 0 } C_ S )
22		ssequn2 3522	. . . . . . . . . . . . . . . 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 5537	. . . . . . . . . . . . . . 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 11473	. . . . . . . . . . . . 13 |- ( k e. ( 0 ... n ) -> k e. NN0 )
28		ffvelrn 5834	. . . . . . . . . . . . 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 3350	. . . . . . . . . . 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 11875	. . . . . . . . . . 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 9398	. . . . . . . . 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 2437	. . . . . . . . . 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 5941	. . . . . . . . . . 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 5694	. . . . . . . . . . 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 7623	. . . . . . . . 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 16459	. . . . . . . 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 11787	. . . . . . . . . 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 17848	. . . . . . . . 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 4371	. . . . . . . 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 2469	. . . . . . 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 16693	. . . . . . . . . 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 16661	. . . . . . . . 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 17806	. . . . . . . . . . 11 |- ℂfld e. CRing
54		plypf1.e	. . . . . . . . . . . 12 |- E = (eval1 ` ℂfld )
55		eqid 2437	. . . . . . . . . . . 12 |- (Poly1 ` ℂfld ) = (Poly1 ` ℂfld )
56	54, 55, 3, 4	evl1rhm 17735	. . . . . . . . . . 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 17659	. . . . . . . . . . 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 16872	. . . . . . . . . 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 16847	. . . . . . . . 9 |- ( ( E " A ) e. (SubRing ` (ℂfld ^s CC ) ) -> ( E " A ) e. (SubGrp ` (ℂfld ^s CC ) ) )
66		subgsubm 15692	. . . . . . . . 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 2437	. . . . . . . . . . . 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 5592	. . . . . . . . . . . . . 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 14418	. . . . . . . . . . . . . 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 2437	. . . . . . . . . . . . . 14 |- ( z e. CC |-> ( z ^ k ) ) = ( z e. CC |-> ( z ^ k ) )
78	76, 77	fmptd 5860	. . . . . . . . . . . . 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 14418	. . . . . . . . . . . . . 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 17793	. . . . . . . . . . . 12 |- x. = ( .r ` ℂfld )
83		eqid 2437	. . . . . . . . . . . 12 |- ( .r ` (ℂfld ^s CC ) ) = ( .r ` (ℂfld ^s CC ) )
84	3, 68, 69, 70, 75, 81, 82, 83	pwsmulrval 14421	. . . . . . . . . . 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 4874	. . . . . . . . . . . . 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 2438	. . . . . . . . . . . 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 6331	. . . . . . . . . . 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 2469	. . . . . . . . . 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 2437	. . . . . . . . . . . . . 14 |- (algSc ` (Poly1 ` ℂfld ) ) = (algSc ` (Poly1 ` ℂfld ) )
93	54, 55, 4, 92	evl1sca 17737	. . . . . . . . . . . . 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 2437	. . . . . . . . . . . . . . . 16 |- ( Base ` (Poly1 ` ℂfld ) ) = ( Base ` (Poly1 ` ℂfld ) )
96	95, 68	rhmf 16800	. . . . . . . . . . . . . . 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 5552	. . . . . . . . . . . . . 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 16842	. . . . . . . . . . . . . . 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 17685	. . . . . . . . . . . . . 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 5948	. . . . . . . . . . . . 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 1218	. . . . . . . . . . . 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 2512	. . . . . . . . . . 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 16842	. . . . . . . . . . . . . . . . 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 2437	. . . . . . . . . . . . . . . . . . . 20 |- (mulGrp ` (Poly1 ` ℂfld ) ) = (mulGrp ` (Poly1 ` ℂfld ) )
113	112	subrgsubm 16854	. . . . . . . . . . . . . . . . . . 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 2437	. . . . . . . . . . . . . . . . . . 19 |- (var1 ` ℂfld ) = (var1 ` ℂfld )
117	116, 103, 58, 59, 60	subrgvr1cl 17687	. . . . . . . . . . . . . . . . . 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 2437	. . . . . . . . . . . . . . . . . . 19 |- (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) = (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) )
119	118	submmulgcl 15650	. . . . . . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . . . . . 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 5948	. . . . . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . . . . 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 3350	. . . . . . . . . . . . . . 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 14419	. . . . . . . . . . . . . 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 5737	. . . . . . . . . . . . 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 17740	. . . . . . . . . . . . . . . . 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 2437	. . . . . . . . . . . . . . . . 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 17748	. . . . . . . . . . . . . . . 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 17818	. . . . . . . . . . . . . . . 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 2469	. . . . . . . . . . . . . 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 4371	. . . . . . . . . . . . 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 2469	. . . . . . . . . . . 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 2512	. . . . . . . . . . 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 16853	. . . . . . . . . . 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 1218	. . . . . . . . . 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 2512	. . . . . . . . 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 5860	. . . . . . . 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 7623	. . . . . . . 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 16393	. . . . . . 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 2512	. . . . . 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 2497	. . . . . 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 2842	. . . 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 5554	. . . . . 6 |- ( E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) -> Fun E )
151	97, 150	ax-mp 5	. . . . 5 |- Fun E
152		fvelima 5736	. . . . 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 3349	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> a e. ( Base ` (Poly1 ` ℂfld ) ) )
155		eqid 2437	. . . . . . . . . . . 12 |- ( .s ` (Poly1 ` ℂfld ) ) = ( .s ` (Poly1 ` ℂfld ) )
156		eqid 2437	. . . . . . . . . . . 12 |- (coe1 ` a ) = (coe1 ` a )
157		cnfldex 17790	. . . . . . . . . . . 12 |- ℂfld e. _V
158	55, 116, 95, 155, 112, 118, 156, 157	ply1coe 17716	. . . . . . . . . . 11 |- ( (ℂfld e. CRing /\ 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 ) ) ) ) ) )
159	53, 154, 158	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 ) ) ) ) ) )
160	159	fveq2d 5688	. . . . . . . . 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 ) ) ) ) ) ) )
161		eqid 2437	. . . . . . . . . 10 |- ( 0g ` (Poly1 ` ℂfld ) ) = ( 0g ` (Poly1 ` ℂfld ) )
162	55	ply1rng 17674	. . . . . . . . . . . 12 |- (ℂfld e. Ring -> (Poly1 ` ℂfld ) e. Ring )
163	9, 162	ax-mp 5	. . . . . . . . . . 11 |- (Poly1 ` ℂfld ) e. Ring
164		rngcmn 16661	. . . . . . . . . . 11 |- ( (Poly1 ` ℂfld ) e. Ring -> (Poly1 ` ℂfld ) e. CMnd )
165	163, 164	mp1i 12	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (Poly1 ` ℂfld ) e. CMnd )
166		rngmnd 16640	. . . . . . . . . . 11 |- ( (ℂfld ^s CC ) e. Ring -> (ℂfld ^s CC ) e. Mnd )
167	50, 166	mp1i 12	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (ℂfld ^s CC ) e. Mnd )
168		nn0ex 10577	. . . . . . . . . . 11 |- NN0 e. _V
169	168	a1i 11	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> NN0 e. _V )
170		rhmghm 16799	. . . . . . . . . . . 12 |- ( E e. ( (Poly1 ` ℂfld ) RingHom (ℂfld ^s CC ) ) -> E e. ( (Poly1 ` ℂfld ) GrpHom (ℂfld ^s CC ) ) )
171	57, 170	ax-mp 5	. . . . . . . . . . 11 |- E e. ( (Poly1 ` ℂfld ) GrpHom (ℂfld ^s CC ) )
172		ghmmhm 15746	. . . . . . . . . . 11 |- ( E e. ( (Poly1 ` ℂfld ) GrpHom (ℂfld ^s CC ) ) -> E e. ( (Poly1 ` ℂfld ) MndHom (ℂfld ^s CC ) ) )
173	171, 172	mp1i 12	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> E e. ( (Poly1 ` ℂfld ) MndHom (ℂfld ^s CC ) ) )
174	55	ply1lmod 17678	. . . . . . . . . . . . 13 |- (ℂfld e. Ring -> (Poly1 ` ℂfld ) e. LMod )
175	9, 174	mp1i 12	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> (Poly1 ` ℂfld ) e. LMod )
176	12	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> S C_ CC )
177		eqid 2437	. . . . . . . . . . . . . . . . 17 |- ( Base ` R ) = ( Base ` R )
178	156, 60, 59, 177	coe1f 17639	. . . . . . . . . . . . . . . 16 |- ( a e. A -> (coe1 ` a ) : NN0 --> ( Base ` R ) )
179	58	subrgbas 16850	. . . . . . . . . . . . . . . . 17 |- ( S e. (SubRing ` ℂfld ) -> S = ( Base ` R ) )
180		feq3 5537	. . . . . . . . . . . . . . . . 17 |- ( S = ( Base ` R ) -> ( (coe1 ` a ) : NN0 --> S <-> (coe1 ` a ) : NN0 --> ( Base ` R ) ) )
181	179, 180	syl 16	. . . . . . . . . . . . . . . 16 |- ( S e. (SubRing ` ℂfld ) -> ( (coe1 ` a ) : NN0 --> S <-> (coe1 ` a ) : NN0 --> ( Base ` R ) ) )
182	178, 181	syl5ibr 221	. . . . . . . . . . . . . . 15 |- ( S e. (SubRing ` ℂfld ) -> ( a e. A -> (coe1 ` a ) : NN0 --> S ) )
183	182	imp 429	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) : NN0 --> S )
184	183	ffvelrnda 5836	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. S )
185	176, 184	sseldd 3350	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. CC )
186	112	rngmgp 16637	. . . . . . . . . . . . . 14 |- ( (Poly1 ` ℂfld ) e. Ring -> (mulGrp ` (Poly1 ` ℂfld ) ) e. Mnd )
187	163, 186	mp1i 12	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> (mulGrp ` (Poly1 ` ℂfld ) ) e. Mnd )
188		simpr 461	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> k e. NN0 )
189	116, 55, 95	vr1cl 17643	. . . . . . . . . . . . . 14 |- (ℂfld e. Ring -> (var1 ` ℂfld ) e. ( Base ` (Poly1 ` ℂfld ) ) )
190	9, 189	mp1i 12	. . . . . . . . . . . . 13 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> (var1 ` ℂfld ) e. ( Base ` (Poly1 ` ℂfld ) ) )
191	112, 95	mgpbas 16583	. . . . . . . . . . . . . 14 |- ( Base ` (Poly1 ` ℂfld ) ) = ( Base ` (mulGrp ` (Poly1 ` ℂfld ) ) )
192	191, 118	mulgnn0cl 15632	. . . . . . . . . . . . 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 ) ) )
193	187, 188, 190, 192	syl3anc 1218	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) e. ( Base ` (Poly1 ` ℂfld ) ) )
194	55	ply1sca 17679	. . . . . . . . . . . . . 14 |- (ℂfld e. Ring -> ℂfld = (Scalar ` (Poly1 ` ℂfld ) ) )
195	9, 194	ax-mp 5	. . . . . . . . . . . . 13 |- ℂfld = (Scalar ` (Poly1 ` ℂfld ) )
196	95, 195, 155, 4	lmodvscl 16941	. . . . . . . . . . . 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 ) ) )
197	175, 185, 193, 196	syl3anc 1218	. . . . . . . . . . 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 ) ) )
198		eqid 2437	. . . . . . . . . . 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 ) ) ) )
199	197, 198	fmptd 5860	. . . . . . . . . 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 ) ) )
200	168	mptex 5941	. . . . . . . . . . . . 13 |- ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) ) e. _V
201		funmpt 5447	. . . . . . . . . . . . 13 |- Fun ( k e. NN0 |-> ( ( (coe1 ` a ) ` k ) ( .s ` (Poly1 ` ℂfld ) ) ( k (.g ` (mulGrp ` (Poly1 ` ℂfld ) ) ) (var1 ` ℂfld ) ) ) )
202		fvex 5694	. . . . . . . . . . . . 13 |- ( 0g ` (Poly1 ` ℂfld ) ) e. _V
203	200, 201, 202	3pm3.2i 1166	. . . . . . . . . . . 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 )
204	203	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 ) )
205	156, 95, 55, 17	coe1sfi 17640	. . . . . . . . . . . . 13 |- ( a e. ( Base ` (Poly1 ` ℂfld ) ) -> (coe1 ` a ) finSupp 0 )
206	154, 205	syl 16	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) finSupp 0 )
207	206	fsuppimpd 7619	. . . . . . . . . . 11 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (coe1 ` a ) supp 0 ) e. Fin )
208	183	feqmptd 5737	. . . . . . . . . . . . . 14 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (coe1 ` a ) = ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) )
209	208	oveq1d 6101	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( (coe1 ` a ) supp 0 ) = ( ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) supp 0 ) )
210		eqimss2 3402	. . . . . . . . . . . . 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 ) )
211	209, 210	syl 16	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( (coe1 ` a ) ` k ) ) supp 0 ) C_ ( (coe1 ` a ) supp 0 ) )
212	9, 174	mp1i 12	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> (Poly1 ` ℂfld ) e. LMod )
213	95, 195, 155, 17, 161	lmod0vs 16957	. . . . . . . . . . . . 13 |- ( ( (Poly1 ` ℂfld ) e. LMod /\ x e. ( Base ` (Poly1 ` ℂfld ) ) ) -> ( 0 ( .s ` (Poly1 ` ℂfld ) ) x ) = ( 0g ` (Poly1 ` ℂfld ) ) )
214	212, 213	sylan 471	. . . . . . . . . . . 12 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ x e. ( Base ` (Poly1 ` ℂfld ) ) ) -> ( 0 ( .s ` (Poly1 ` ℂfld ) ) x ) = ( 0g ` (Poly1 ` ℂfld ) ) )
215		c0ex 9372	. . . . . . . . . . . . 13 |- 0 e. _V
216	215	a1i 11	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> 0 e. _V )
217	211, 214, 184, 193, 216	suppssov1 6716	. . . . . . . . . . 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 ) )
218		suppssfifsupp 7627	. . . . . . . . . . 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 ) ) )
219	204, 207, 217, 218	syl12anc 1216	. . . . . . . . . 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 ) ) )
220	95, 161, 165, 167, 169, 173, 199, 219	gsummhm 16420	. . . . . . . . 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 ) ) ) ) ) ) )
221		eqidd 2438	. . . . . . . . . . . 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 ) ) ) ) )
222	97	a1i 11	. . . . . . . . . . . . 13 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> E : ( Base ` (Poly1 ` ℂfld ) ) --> ( Base ` (ℂfld ^s CC ) ) )
223	222	feqmptd 5737	. . . . . . . . . . . 12 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> E = ( x e. ( Base ` (Poly1 ` ℂfld ) ) |-> ( E ` x ) ) )
224		fveq2 5684	. . . . . . . . . . . 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 ) ) ) ) )
225	197, 221, 223, 224	fmptco 5869	. . . . . . . . . . 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 ) ) ) ) ) )
226	9	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> ℂfld e. Ring )
227	6	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) -> CC e. _V )
228	97	ffvelrni 5835	. . . . . . . . . . . . . . . 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 ) ) )
229	197, 228	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 ) ) )
230	3, 4, 68, 226, 227, 229	pwselbas 14419	. . . . . . . . . . . . . 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 )
231	230	feqmptd 5737	. . . . . . . . . . . . 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 ) ) )
232	53	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ℂfld e. CRing )
233		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> z e. CC )
234	54, 116, 4, 55, 95, 232, 233	evl1vard 17740	. . . . . . . . . . . . . . . . . 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 ) )
235	188	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> k e. NN0 )
236	54, 55, 4, 95, 232, 233, 234, 118, 129, 235	evl1expd 17748	. . . . . . . . . . . . . . . . 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 ) ) )
237	233, 235, 133	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( k (.g ` (mulGrp ` ℂfld ) ) z ) = ( z ^ k ) )
238	237	eqeq2d 2448	. . . . . . . . . . . . . . . . . 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 ) ) )
239	238	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 ) ) ) )
240	236, 239	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 ) ) )
241	185	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( (coe1 ` a ) ` k ) e. CC )
242	54, 55, 4, 95, 232, 233, 240, 241, 155, 82	evl1vsd 17747	. . . . . . . . . . . . . . 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 ) ) ) )
243	242	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 ) ) )
244	243	mpteq2dva 4371	. . . . . . . . . . . . 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 ) ) ) )
245	231, 244	eqtrd 2469	. . . . . . . . . . . 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 ) ) ) )
246	245	mpteq2dva 4371	. . . . . . . . . . 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 ) ) ) ) )
247	225, 246	eqtrd 2469	. . . . . . . . . 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 ) ) ) ) )
248	247	oveq2d 6102	. . . . . . . . 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 ) ) ) ) ) )
249	160, 220, 248	3eqtr2d 2475	. . . . . . . 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 ) ) ) ) ) )
250	6	a1i 11	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> CC e. _V )
251	9, 10	mp1i 12	. . . . . . . . 9 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ℂfld e. CMnd )
252	185	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( (coe1 ` a ) ` k ) e. CC )
253	34	adantll 713	. . . . . . . . . . 11 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( z ^ k ) e. CC )
254	252, 253	mulcld 9398	. . . . . . . . . 10 |- ( ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) e. CC )
255	254	anasss 647	. . . . . . . . 9 |- ( ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) /\ ( z e. CC /\ k e. NN0 ) ) -> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) e. CC )
256	168	mptex 5941	. . . . . . . . . . . 12 |- ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V
257		funmpt 5447	. . . . . . . . . . . 12 |- Fun ( k e. NN0 |-> ( z e. CC |-> ( ( (coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
258	256, 257, 40	3pm3.2i 1166	. . . . . . . . . . 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 )
259	258	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 ) )
260		fzfid 11787	. . . . . . . . . 10 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) e. Fin )
261		eldifn 3472	. . . . . . . . . . . . . . . . . 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 ) ) )
262	261	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 ) ) )
263	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 ) ) )
264		eldifi 3471	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) ) -> k e. NN0 )
265	264	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 )
266		eqid 2437	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( deg1 ` ℂfld ) = ( deg1 ` ℂfld )
267	266, 55, 95, 17, 156	deg1ge 21539	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( a e. ( Base ` (Poly1 ` ℂfld ) ) /\ k e. NN0 /\ ( (coe1 ` a ) ` k ) =/= 0 ) -> k <_ ( ( deg1 ` ℂfld ) ` a ) )
268	267	3expia 1189	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a e. ( Base ` (Poly1 ` ℂfld ) ) /\ k e. NN0 ) -> ( ( (coe1 ` a ) ` k ) =/= 0 -> k <_ ( ( deg1 ` ℂfld ) ` a ) ) )
269	263, 265, 268	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 ) ) )
270		0xr 9422	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. RR*
271	266, 55, 95	deg1xrcl 21522	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a e. ( Base ` (Poly1 ` ℂfld ) ) -> ( ( deg1 ` ℂfld ) ` a ) e. RR* )
272	154, 271	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( deg1 ` ℂfld ) ` a ) e. RR* )
273	272	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* )
274		xrmax2 11140	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 0 e. RR* /\ ( ( deg1 ` ℂfld ) ` a ) e. RR* ) -> ( ( deg1 ` ℂfld ) ` a ) <_ if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) )
275	270, 273, 274	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 ) )
276	265	nn0red 10629	. . . . . . . . . . . . . . . . . . . . . . . 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 )
277	276	rexrd 9425	. . . . . . . . . . . . . . . . . . . . . . 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* )
278		ifcl 3824	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( deg1 ` ℂfld ) ` a ) e. RR* /\ 0 e. RR* ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. RR* )
279	273, 270, 278	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* )
280		xrletr 11124	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
281	277, 273, 279, 280	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . 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 ) ) )
282	275, 281	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 ) ) )
283	269, 282	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 ) ) )
284	283, 265	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 ) ) ) )
285	266, 55, 95	deg1cl 21523	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( a e. ( Base ` (Poly1 ` ℂfld ) ) -> ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) )
286	154, 285	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) )
287		elun 3490	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. ( NN0 u. { -oo } ) <-> ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) )
288	286, 287	sylib 196	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) )
289		nn0ge0 10597	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> 0 <_ ( ( deg1 ` ℂfld ) ` a ) )
290		iftrue 3790	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = ( ( deg1 ` ℂfld ) ` a ) )
291	289, 290	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = ( ( deg1 ` ℂfld ) ` a ) )
292		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> ( ( deg1 ` ℂfld ) ` a ) e. NN0 )
293	291, 292	eqeltrd 2511	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
294		mnflt0 11097	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- -oo < 0
295		mnfxr 11086	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- -oo e. RR*
296		xrltnle 9435	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( -oo e. RR* /\ 0 e. RR* ) -> ( -oo < 0 <-> -. 0 <_ -oo ) )
297	295, 270, 296	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -oo < 0 <-> -. 0 <_ -oo )
298	294, 297	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- -. 0 <_ -oo
299		elsni 3895	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> ( ( deg1 ` ℂfld ) ` a ) = -oo )
300	299	breq2d 4297	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) <-> 0 <_ -oo ) )
301	298, 300	mtbiri 303	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> -. 0 <_ ( ( deg1 ` ℂfld ) ` a ) )
302		iffalse 3792	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. 0 <_ ( ( deg1 ` ℂfld ) ` a ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = 0 )
303	301, 302	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) = 0 )
304		0nn0 10586	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. NN0
305	303, 304	syl6eqel 2525	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( deg1 ` ℂfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
306	293, 305	jaoi 379	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( deg1 ` ℂfld ) ` a ) e. NN0 \/ ( ( deg1 ` ℂfld ) ` a ) e. { -oo } ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
307	288, 306	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( S e. (SubRing ` ℂfld ) /\ a e. A ) -> if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) e. NN0 )
308	307	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 )
309		fznn0 11516	. . . . . . . . . . . . . . . . . . . 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 ) ) ) )
310	308, 309	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 ) ) ) )
311	284, 310	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 ) ) ) )
312	311	necon1bd 2673	. . . . . . . . . . . . . . . . 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 ) )
313	262, 312	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 )
314	313	oveq1d 6101	. . . . . . . . . . . . . . 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 ) ) )
315	264, 253	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 )
316	315	mul02d 9559	. . . . . . . . . . . . . . 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 )
317	314, 316	eqtrd 2469	. . . . . . . . . . . . . 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 )
318	317	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 )
319	318	mpteq2dva 4371	. . . . . . . . . . . 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 ) )
320		fconstmpt 4874	. . . . . . . . . . . . 13 |- ( CC X. { 0 } ) = ( z e. CC |-> 0 )
321		rngmnd 16640	. . . . . . . . . . . . . . 15 |- (ℂfld e. Ring -> ℂfld e. Mnd )
322	9, 321	ax-mp 5	. . . . . . . . . . . . . 14 |- ℂfld e. Mnd
323	3, 17	pws0g 15449	. . . . . . . . . . . . . 14 |- ( (ℂfld e. Mnd /\ CC e. _V ) -> ( CC X. { 0 } ) = ( 0g ` (ℂfld ^s CC ) ) )
324	322, 6, 323	mp2an 672	. . . . . . . . . . . . 13 |- ( CC X. { 0 } ) = ( 0g ` (ℂfld ^s CC ) )
325	320, 324	eqtr3i 2459	. . . . . . . . . . . 12 |- ( z e. CC |-> 0 ) = ( 0g ` (ℂfld ^s CC ) )
326	319, 325	syl6eq 2485	. . . . . . . . . . 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 ) ) )
327	326, 169	suppss2 6718	. . . . . . . . . 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 ) ) )
328		suppssfifsupp 7627	. . . . . . . . . 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 ) ) )
329	259, 260, 327, 328	syl12anc 1216	. . . . . . . . 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 ) ) )
330	3, 4, 5, 250, 169, 251, 255, 329	pwsgsum 16459	. . . . . . . 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 ) ) ) ) ) )
331		elfznn0 11473	. . . . . . . . . . . . 13 |- ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) -> k e. NN0 )
332	331	ssriv 3353	. . . . . . . . . . . 12 |- ( 0 ... if ( 0 <_ ( ( deg1 ` ℂfld ) ` a ) , ( ( deg1 ` ℂfld ) ` a ) , 0 ) ) C_ NN0
333		resmpt 5149	. . . . . . . . . . . 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 ) ) ) )
334	332, 333	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 ) , (