plypf1

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)

	Ref	Expression
Hypotheses	plypf1.r	$⊢ R = ℂ_{fld} ↾_{𝑠} S$
	plypf1.p	$⊢ P = {Poly}_{1} (R)$
	plypf1.a	$⊢ A = {Base}_{P}$
	plypf1.e	$⊢ E = {eval}_{1} (ℂ_{fld})$
Assertion	plypf1	$⊢ S \in SubRing (ℂ_{fld}) \to Poly (S) = E [A]$

Proof

Step	Hyp	Ref	Expression
1		plypf1.r	$⊢ R = ℂ_{fld} ↾_{𝑠} S$
2		plypf1.p	$⊢ P = {Poly}_{1} (R)$
3		plypf1.a	$⊢ A = {Base}_{P}$
4		plypf1.e	$⊢ E = {eval}_{1} (ℂ_{fld})$
5		elply	$⊢ f \in Poly (S) \leftrightarrow (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) f = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
6	5	simprbi	$⊢ f \in Poly (S) \to \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) f = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
7		eqid	$⊢ ℂ_{fld} ↑_{𝑠} ℂ = ℂ_{fld} ↑_{𝑠} ℂ$
8		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
9		eqid	$⊢ 0_{(ℂ_{fld} ↑_{𝑠} ℂ)} = 0_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
10		cnex	$⊢ ℂ \in V$
11	10	a1i	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to ℂ \in V$
12		fzfid	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to (0 \dots n) \in Fin$
13		cnring	$⊢ ℂ_{fld} \in Ring$
14		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
15	13 14	mp1i	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to ℂ_{fld} \in CMnd$
16	8	subrgss	$⊢ S \in SubRing (ℂ_{fld}) \to S \subseteq ℂ$
17	16	ad2antrr	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to S \subseteq ℂ$
18		elmapi	$⊢ a \in ({(S \cup \{0\})}^{ℕ_{0}}) \to a : ℕ_{0} ⟶ S \cup \{0\}$
19	18	ad2antll	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to a : ℕ_{0} ⟶ S \cup \{0\}$
20		subrgsubg	$⊢ S \in SubRing (ℂ_{fld}) \to S \in SubGrp (ℂ_{fld})$
21		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
22	21	subg0cl	$⊢ S \in SubGrp (ℂ_{fld}) \to 0 \in S$
23	20 22	syl	$⊢ S \in SubRing (ℂ_{fld}) \to 0 \in S$
24	23	adantr	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to 0 \in S$
25	24	snssd	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to \{0\} \subseteq S$
26		ssequn2	$⊢ \{0\} \subseteq S \leftrightarrow S \cup \{0\} = S$
27	25 26	sylib	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to S \cup \{0\} = S$
28	27	feq3d	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to (a : ℕ_{0} ⟶ S \cup \{0\} \leftrightarrow a : ℕ_{0} ⟶ S)$
29	19 28	mpbid	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to a : ℕ_{0} ⟶ S$
30		elfznn0	$⊢ k \in (0 \dots n) \to k \in ℕ_{0}$
31		ffvelrn	$⊢ (a : ℕ_{0} ⟶ S \land k \in ℕ_{0}) \to a (k) \in S$
32	29 30 31	syl2an	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to a (k) \in S$
33	17 32	sseldd	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to a (k) \in ℂ$
34	33	adantrl	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (z \in ℂ \land k \in (0 \dots n))) \to a (k) \in ℂ$
35		simprl	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (z \in ℂ \land k \in (0 \dots n))) \to z \in ℂ$
36	30	ad2antll	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (z \in ℂ \land k \in (0 \dots n))) \to k \in ℕ_{0}$
37		expcl	$⊢ (z \in ℂ \land k \in ℕ_{0}) \to z^{k} \in ℂ$
38	35 36 37	syl2anc	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (z \in ℂ \land k \in (0 \dots n))) \to z^{k} \in ℂ$
39	34 38	mulcld	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (z \in ℂ \land k \in (0 \dots n))) \to a (k) z^{k} \in ℂ$
40		eqid	$⊢ (k \in (0 \dots n) ⟼ (z \in ℂ ⟼ a (k) z^{k})) = (k \in (0 \dots n) ⟼ (z \in ℂ ⟼ a (k) z^{k}))$
41	10	mptex	$⊢ (z \in ℂ ⟼ a (k) z^{k}) \in V$
42	41	a1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (z \in ℂ ⟼ a (k) z^{k}) \in V$
43		fvex	$⊢ 0_{(ℂ_{fld} ↑_{𝑠} ℂ)} \in V$
44	43	a1i	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to 0_{(ℂ_{fld} ↑_{𝑠} ℂ)} \in V$
45	40 12 42 44	fsuppmptdm	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to {finSupp}_{0_{(ℂ_{fld} ↑_{𝑠} ℂ)}} ((k \in (0 \dots n) ⟼ (z \in ℂ ⟼ a (k) z^{k})))$
46	7 8 9 11 12 15 39 45	pwsgsum	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to {\sum_{ℂ_{fld} ↑_{𝑠} ℂ}}_{k = 0}^{n} (z \in ℂ ⟼ a (k) z^{k}) = (z \in ℂ ⟼ {\sum_{ℂ_{fld}}}_{k = 0}^{n} a (k) z^{k})$
47		fzfid	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \to (0 \dots n) \in Fin$
48	39	anassrs	$⊢ (((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \land k \in (0 \dots n)) \to a (k) z^{k} \in ℂ$
49	47 48	gsumfsum	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \to {\sum_{ℂ_{fld}}}_{k = 0}^{n} a (k) z^{k} = \sum_{k = 0}^{n} a (k) z^{k}$
50	49	mpteq2dva	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to (z \in ℂ ⟼ {\sum_{ℂ_{fld}}}_{k = 0}^{n} a (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
51	46 50	eqtrd	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to {\sum_{ℂ_{fld} ↑_{𝑠} ℂ}}_{k = 0}^{n} (z \in ℂ ⟼ a (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
52	7	pwsring	$⊢ (ℂ_{fld} \in Ring \land ℂ \in V) \to ℂ_{fld} ↑_{𝑠} ℂ \in Ring$
53	13 10 52	mp2an	$⊢ ℂ_{fld} ↑_{𝑠} ℂ \in Ring$
54		ringcmn	$⊢ ℂ_{fld} ↑_{𝑠} ℂ \in Ring \to ℂ_{fld} ↑_{𝑠} ℂ \in CMnd$
55	53 54	mp1i	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to ℂ_{fld} ↑_{𝑠} ℂ \in CMnd$
56		cncrng	$⊢ ℂ_{fld} \in CRing$
57		eqid	$⊢ {Poly}_{1} (ℂ_{fld}) = {Poly}_{1} (ℂ_{fld})$
58	4 57 7 8	evl1rhm	$⊢ ℂ_{fld} \in CRing \to E \in ({Poly}_{1} (ℂ_{fld}) RingHom (ℂ_{fld} ↑_{𝑠} ℂ))$
59	56 58	ax-mp	$⊢ E \in ({Poly}_{1} (ℂ_{fld}) RingHom (ℂ_{fld} ↑_{𝑠} ℂ))$
60	57 1 2 3	subrgply1	$⊢ S \in SubRing (ℂ_{fld}) \to A \in SubRing ({Poly}_{1} (ℂ_{fld}))$
61	60	adantr	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to A \in SubRing ({Poly}_{1} (ℂ_{fld}))$
62		rhmima	$⊢ (E \in ({Poly}_{1} (ℂ_{fld}) RingHom (ℂ_{fld} ↑_{𝑠} ℂ)) \land A \in SubRing ({Poly}_{1} (ℂ_{fld}))) \to E [A] \in SubRing (ℂ_{fld} ↑_{𝑠} ℂ)$
63	59 61 62	sylancr	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to E [A] \in SubRing (ℂ_{fld} ↑_{𝑠} ℂ)$
64		subrgsubg	$⊢ E [A] \in SubRing (ℂ_{fld} ↑_{𝑠} ℂ) \to E [A] \in SubGrp (ℂ_{fld} ↑_{𝑠} ℂ)$
65		subgsubm	$⊢ E [A] \in SubGrp (ℂ_{fld} ↑_{𝑠} ℂ) \to E [A] \in SubMnd (ℂ_{fld} ↑_{𝑠} ℂ)$
66	63 64 65	3syl	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to E [A] \in SubMnd (ℂ_{fld} ↑_{𝑠} ℂ)$
67		eqid	$⊢ {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)} = {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
68	13	a1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to ℂ_{fld} \in Ring$
69	10	a1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to ℂ \in V$
70		fconst6g	$⊢ a (k) \in ℂ \to (ℂ \times \{a (k)\}) : ℂ ⟶ ℂ$
71	33 70	syl	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (ℂ \times \{a (k)\}) : ℂ ⟶ ℂ$
72	7 8 67	pwselbasb	$⊢ (ℂ_{fld} \in Ring \land ℂ \in V) \to (ℂ \times \{a (k)\} \in {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)} \leftrightarrow (ℂ \times \{a (k)\}) : ℂ ⟶ ℂ)$
73	13 10 72	mp2an	$⊢ ℂ \times \{a (k)\} \in {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)} \leftrightarrow (ℂ \times \{a (k)\}) : ℂ ⟶ ℂ$
74	71 73	sylibr	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to ℂ \times \{a (k)\} \in {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
75	38	anass1rs	$⊢ (((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \land z \in ℂ) \to z^{k} \in ℂ$
76	75	fmpttd	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (z \in ℂ ⟼ z^{k}) : ℂ ⟶ ℂ$
77	7 8 67	pwselbasb	$⊢ (ℂ_{fld} \in Ring \land ℂ \in V) \to ((z \in ℂ ⟼ z^{k}) \in {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)} \leftrightarrow (z \in ℂ ⟼ z^{k}) : ℂ ⟶ ℂ)$
78	13 10 77	mp2an	$⊢ (z \in ℂ ⟼ z^{k}) \in {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)} \leftrightarrow (z \in ℂ ⟼ z^{k}) : ℂ ⟶ ℂ$
79	76 78	sylibr	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (z \in ℂ ⟼ z^{k}) \in {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
80		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
81		eqid	$⊢ \cdot_{(ℂ_{fld} ↑_{𝑠} ℂ)} = \cdot_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
82	7 67 68 69 74 79 80 81	pwsmulrval	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (ℂ \times \{a (k)\}) \cdot_{(ℂ_{fld} ↑_{𝑠} ℂ)} (z \in ℂ ⟼ z^{k}) = (ℂ \times \{a (k)\}) \times_{f} (z \in ℂ ⟼ z^{k})$
83	33	adantr	$⊢ (((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \land z \in ℂ) \to a (k) \in ℂ$
84		fconstmpt	$⊢ ℂ \times \{a (k)\} = (z \in ℂ ⟼ a (k))$
85	84	a1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to ℂ \times \{a (k)\} = (z \in ℂ ⟼ a (k))$
86		eqidd	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (z \in ℂ ⟼ z^{k}) = (z \in ℂ ⟼ z^{k})$
87	69 83 75 85 86	offval2	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (ℂ \times \{a (k)\}) \times_{f} (z \in ℂ ⟼ z^{k}) = (z \in ℂ ⟼ a (k) z^{k})$
88	82 87	eqtrd	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (ℂ \times \{a (k)\}) \cdot_{(ℂ_{fld} ↑_{𝑠} ℂ)} (z \in ℂ ⟼ z^{k}) = (z \in ℂ ⟼ a (k) z^{k})$
89	63	adantr	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to E [A] \in SubRing (ℂ_{fld} ↑_{𝑠} ℂ)$
90		eqid	$⊢ algSc ({Poly}_{1} (ℂ_{fld})) = algSc ({Poly}_{1} (ℂ_{fld}))$
91	4 57 8 90	evl1sca	$⊢ (ℂ_{fld} \in CRing \land a (k) \in ℂ) \to E (algSc ({Poly}_{1} (ℂ_{fld})) (a (k))) = ℂ \times \{a (k)\}$
92	56 33 91	sylancr	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to E (algSc ({Poly}_{1} (ℂ_{fld})) (a (k))) = ℂ \times \{a (k)\}$
93		eqid	$⊢ {Base}_{{Poly}_{1} (ℂ_{fld})} = {Base}_{{Poly}_{1} (ℂ_{fld})}$
94	93 67	rhmf	$⊢ E \in ({Poly}_{1} (ℂ_{fld}) RingHom (ℂ_{fld} ↑_{𝑠} ℂ)) \to E : {Base}_{{Poly}_{1} (ℂ_{fld})} ⟶ {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
95	59 94	ax-mp	$⊢ E : {Base}_{{Poly}_{1} (ℂ_{fld})} ⟶ {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
96		ffn	$⊢ E : {Base}_{{Poly}_{1} (ℂ_{fld})} ⟶ {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)} \to E Fn {Base}_{{Poly}_{1} (ℂ_{fld})}$
97	95 96	mp1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to E Fn {Base}_{{Poly}_{1} (ℂ_{fld})}$
98	93	subrgss	$⊢ A \in SubRing ({Poly}_{1} (ℂ_{fld})) \to A \subseteq {Base}_{{Poly}_{1} (ℂ_{fld})}$
99	60 98	syl	$⊢ S \in SubRing (ℂ_{fld}) \to A \subseteq {Base}_{{Poly}_{1} (ℂ_{fld})}$
100	99	ad2antrr	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to A \subseteq {Base}_{{Poly}_{1} (ℂ_{fld})}$
101		simpll	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to S \in SubRing (ℂ_{fld})$
102	57 90 1 2 101 3 8 33	subrg1asclcl	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (algSc ({Poly}_{1} (ℂ_{fld})) (a (k)) \in A \leftrightarrow a (k) \in S)$
103	32 102	mpbird	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to algSc ({Poly}_{1} (ℂ_{fld})) (a (k)) \in A$
104		fnfvima	$⊢ (E Fn {Base}_{{Poly}_{1} (ℂ_{fld})} \land A \subseteq {Base}_{{Poly}_{1} (ℂ_{fld})} \land algSc ({Poly}_{1} (ℂ_{fld})) (a (k)) \in A) \to E (algSc ({Poly}_{1} (ℂ_{fld})) (a (k))) \in E [A]$
105	97 100 103 104	syl3anc	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to E (algSc ({Poly}_{1} (ℂ_{fld})) (a (k))) \in E [A]$
106	92 105	eqeltrrd	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to ℂ \times \{a (k)\} \in E [A]$
107	67	subrgss	$⊢ E [A] \in SubRing (ℂ_{fld} ↑_{𝑠} ℂ) \to E [A] \subseteq {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
108	89 107	syl	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to E [A] \subseteq {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
109	60	ad2antrr	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to A \in SubRing ({Poly}_{1} (ℂ_{fld}))$
110		eqid	$⊢ {mulGrp}_{{Poly}_{1} (ℂ_{fld})} = {mulGrp}_{{Poly}_{1} (ℂ_{fld})}$
111	110	subrgsubm	$⊢ A \in SubRing ({Poly}_{1} (ℂ_{fld})) \to A \in SubMnd ({mulGrp}_{{Poly}_{1} (ℂ_{fld})})$
112	109 111	syl	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to A \in SubMnd ({mulGrp}_{{Poly}_{1} (ℂ_{fld})})$
113	30	adantl	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to k \in ℕ_{0}$
114		eqid	$⊢ {var}_{1} (ℂ_{fld}) = {var}_{1} (ℂ_{fld})$
115	114 101 1 2 3	subrgvr1cl	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to {var}_{1} (ℂ_{fld}) \in A$
116		eqid	$⊢ \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} = \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}}$
117	116	submmulgcl	$⊢ (A \in SubMnd ({mulGrp}_{{Poly}_{1} (ℂ_{fld})}) \land k \in ℕ_{0} \land {var}_{1} (ℂ_{fld}) \in A) \to k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}) \in A$
118	112 113 115 117	syl3anc	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}) \in A$
119		fnfvima	$⊢ (E Fn {Base}_{{Poly}_{1} (ℂ_{fld})} \land A \subseteq {Base}_{{Poly}_{1} (ℂ_{fld})} \land k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}) \in A) \to E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) \in E [A]$
120	97 100 118 119	syl3anc	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) \in E [A]$
121	108 120	sseldd	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) \in {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
122	7 8 67 68 69 121	pwselbas	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) : ℂ ⟶ ℂ$
123	122	feqmptd	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) = (z \in ℂ ⟼ E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) (z))$
124	56	a1i	$⊢ (((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \land z \in ℂ) \to ℂ_{fld} \in CRing$
125		simpr	$⊢ (((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \land z \in ℂ) \to z \in ℂ$
126	4 114 8 57 93 124 125	evl1vard	$⊢ (((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \land z \in ℂ) \to ({var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})} \land E ({var}_{1} (ℂ_{fld})) (z) = z)$
127		eqid	$⊢ \cdot_{{mulGrp}_{ℂ_{fld}}} = \cdot_{{mulGrp}_{ℂ_{fld}}}$
128	113	adantr	$⊢ (((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \land z \in ℂ) \to k \in ℕ_{0}$
129	4 57 8 93 124 125 126 116 127 128	evl1expd	$⊢ (((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \land z \in ℂ) \to (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})} \land E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) (z) = k \cdot_{{mulGrp}_{ℂ_{fld}}} z)$
130	129	simprd	$⊢ (((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \land z \in ℂ) \to E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) (z) = k \cdot_{{mulGrp}_{ℂ_{fld}}} z$
131		cnfldexp	$⊢ (z \in ℂ \land k \in ℕ_{0}) \to k \cdot_{{mulGrp}_{ℂ_{fld}}} z = z^{k}$
132	125 128 131	syl2anc	$⊢ (((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \land z \in ℂ) \to k \cdot_{{mulGrp}_{ℂ_{fld}}} z = z^{k}$
133	130 132	eqtrd	$⊢ (((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \land z \in ℂ) \to E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) (z) = z^{k}$
134	133	mpteq2dva	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (z \in ℂ ⟼ E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) (z)) = (z \in ℂ ⟼ z^{k})$
135	123 134	eqtrd	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) = (z \in ℂ ⟼ z^{k})$
136	135 120	eqeltrrd	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (z \in ℂ ⟼ z^{k}) \in E [A]$
137	81	subrgmcl	$⊢ (E [A] \in SubRing (ℂ_{fld} ↑_{𝑠} ℂ) \land ℂ \times \{a (k)\} \in E [A] \land (z \in ℂ ⟼ z^{k}) \in E [A]) \to (ℂ \times \{a (k)\}) \cdot_{(ℂ_{fld} ↑_{𝑠} ℂ)} (z \in ℂ ⟼ z^{k}) \in E [A]$
138	89 106 136 137	syl3anc	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (ℂ \times \{a (k)\}) \cdot_{(ℂ_{fld} ↑_{𝑠} ℂ)} (z \in ℂ ⟼ z^{k}) \in E [A]$
139	88 138	eqeltrrd	$⊢ ((S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land k \in (0 \dots n)) \to (z \in ℂ ⟼ a (k) z^{k}) \in E [A]$
140	139	fmpttd	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to (k \in (0 \dots n) ⟼ (z \in ℂ ⟼ a (k) z^{k})) : (0 \dots n) ⟶ E [A]$
141	40 12 139 44	fsuppmptdm	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to {finSupp}_{0_{(ℂ_{fld} ↑_{𝑠} ℂ)}} ((k \in (0 \dots n) ⟼ (z \in ℂ ⟼ a (k) z^{k})))$
142	9 55 12 66 140 141	gsumsubmcl	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to {\sum_{ℂ_{fld} ↑_{𝑠} ℂ}}_{k = 0}^{n} (z \in ℂ ⟼ a (k) z^{k}) \in E [A]$
143	51 142	eqeltrrd	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) \in E [A]$
144		eleq1	$⊢ f = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) \to (f \in E [A] \leftrightarrow (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) \in E [A])$
145	143 144	syl5ibrcom	$⊢ (S \in SubRing (ℂ_{fld}) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to (f = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) \to f \in E [A])$
146	145	rexlimdvva	$⊢ S \in SubRing (ℂ_{fld}) \to (\exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) f = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) \to f \in E [A])$
147	6 146	syl5	$⊢ S \in SubRing (ℂ_{fld}) \to (f \in Poly (S) \to f \in E [A])$
148		ffun	$⊢ E : {Base}_{{Poly}_{1} (ℂ_{fld})} ⟶ {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)} \to Fun E$
149	95 148	ax-mp	$⊢ Fun E$
150		fvelima	$⊢ (Fun E \land f \in E [A]) \to \exists a \in A E (a) = f$
151	149 150	mpan	$⊢ f \in E [A] \to \exists a \in A E (a) = f$
152	99	sselda	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to a \in {Base}_{{Poly}_{1} (ℂ_{fld})}$
153		eqid	$⊢ \cdot_{{Poly}_{1} (ℂ_{fld})} = \cdot_{{Poly}_{1} (ℂ_{fld})}$
154		eqid	$⊢ {coe}_{1} (a) = {coe}_{1} (a)$
155	57 114 93 153 110 116 154	ply1coe	$⊢ (ℂ_{fld} \in Ring \land a \in {Base}_{{Poly}_{1} (ℂ_{fld})}) \to a = \underset{k \in ℕ_{0}}{\sum_{{Poly}_{1} (ℂ_{fld})}} ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})))$
156	13 152 155	sylancr	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to a = \underset{k \in ℕ_{0}}{\sum_{{Poly}_{1} (ℂ_{fld})}} ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})))$
157	156	fveq2d	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to E (a) = E (\underset{k \in ℕ_{0}}{\sum_{{Poly}_{1} (ℂ_{fld})}} ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))))$
158		eqid	$⊢ 0_{{Poly}_{1} (ℂ_{fld})} = 0_{{Poly}_{1} (ℂ_{fld})}$
159	57	ply1ring	$⊢ ℂ_{fld} \in Ring \to {Poly}_{1} (ℂ_{fld}) \in Ring$
160	13 159	ax-mp	$⊢ {Poly}_{1} (ℂ_{fld}) \in Ring$
161		ringcmn	$⊢ {Poly}_{1} (ℂ_{fld}) \in Ring \to {Poly}_{1} (ℂ_{fld}) \in CMnd$
162	160 161	mp1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {Poly}_{1} (ℂ_{fld}) \in CMnd$
163		ringmnd	$⊢ ℂ_{fld} ↑_{𝑠} ℂ \in Ring \to ℂ_{fld} ↑_{𝑠} ℂ \in Mnd$
164	53 163	mp1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to ℂ_{fld} ↑_{𝑠} ℂ \in Mnd$
165		nn0ex	$⊢ ℕ_{0} \in V$
166	165	a1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to ℕ_{0} \in V$
167		rhmghm	$⊢ E \in ({Poly}_{1} (ℂ_{fld}) RingHom (ℂ_{fld} ↑_{𝑠} ℂ)) \to E \in ({Poly}_{1} (ℂ_{fld}) GrpHom (ℂ_{fld} ↑_{𝑠} ℂ))$
168	59 167	ax-mp	$⊢ E \in ({Poly}_{1} (ℂ_{fld}) GrpHom (ℂ_{fld} ↑_{𝑠} ℂ))$
169		ghmmhm	$⊢ E \in ({Poly}_{1} (ℂ_{fld}) GrpHom (ℂ_{fld} ↑_{𝑠} ℂ)) \to E \in ({Poly}_{1} (ℂ_{fld}) MndHom (ℂ_{fld} ↑_{𝑠} ℂ))$
170	168 169	mp1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to E \in ({Poly}_{1} (ℂ_{fld}) MndHom (ℂ_{fld} ↑_{𝑠} ℂ))$
171	57	ply1lmod	$⊢ ℂ_{fld} \in Ring \to {Poly}_{1} (ℂ_{fld}) \in LMod$
172	13 171	mp1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to {Poly}_{1} (ℂ_{fld}) \in LMod$
173	16	ad2antrr	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to S \subseteq ℂ$
174		eqid	$⊢ {Base}_{R} = {Base}_{R}$
175	154 3 2 174	coe1f	$⊢ a \in A \to {coe}_{1} (a) : ℕ_{0} ⟶ {Base}_{R}$
176	1	subrgbas	$⊢ S \in SubRing (ℂ_{fld}) \to S = {Base}_{R}$
177	176	feq3d	$⊢ S \in SubRing (ℂ_{fld}) \to ({coe}_{1} (a) : ℕ_{0} ⟶ S \leftrightarrow {coe}_{1} (a) : ℕ_{0} ⟶ {Base}_{R})$
178	175 177	syl5ibr	$⊢ S \in SubRing (ℂ_{fld}) \to (a \in A \to {coe}_{1} (a) : ℕ_{0} ⟶ S)$
179	178	imp	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {coe}_{1} (a) : ℕ_{0} ⟶ S$
180	179	ffvelrnda	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to {coe}_{1} (a) (k) \in S$
181	173 180	sseldd	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to {coe}_{1} (a) (k) \in ℂ$
182	110	ringmgp	$⊢ {Poly}_{1} (ℂ_{fld}) \in Ring \to {mulGrp}_{{Poly}_{1} (ℂ_{fld})} \in Mnd$
183	160 182	mp1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to {mulGrp}_{{Poly}_{1} (ℂ_{fld})} \in Mnd$
184		simpr	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
185	114 57 93	vr1cl	$⊢ ℂ_{fld} \in Ring \to {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})}$
186	13 185	mp1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})}$
187	110 93	mgpbas	$⊢ {Base}_{{Poly}_{1} (ℂ_{fld})} = {Base}_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}}$
188	187 116	mulgnn0cl	$⊢ ({mulGrp}_{{Poly}_{1} (ℂ_{fld})} \in Mnd \land k \in ℕ_{0} \land {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})}) \to k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})}$
189	183 184 186 188	syl3anc	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})}$
190	57	ply1sca	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} = Scalar ({Poly}_{1} (ℂ_{fld}))$
191	13 190	ax-mp	$⊢ ℂ_{fld} = Scalar ({Poly}_{1} (ℂ_{fld}))$
192	93 191 153 8	lmodvscl	$⊢ ({Poly}_{1} (ℂ_{fld}) \in LMod \land {coe}_{1} (a) (k) \in ℂ \land k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})}) \to {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) \in {Base}_{{Poly}_{1} (ℂ_{fld})}$
193	172 181 189 192	syl3anc	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) \in {Base}_{{Poly}_{1} (ℂ_{fld})}$
194	193	fmpttd	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) : ℕ_{0} ⟶ {Base}_{{Poly}_{1} (ℂ_{fld})}$
195	165	mptex	$⊢ (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) \in V$
196		funmpt	$⊢ Fun (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})))$
197		fvex	$⊢ 0_{{Poly}_{1} (ℂ_{fld})} \in V$
198	195 196 197	3pm3.2i	$⊢ ((k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) \in V \land Fun (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) \land 0_{{Poly}_{1} (ℂ_{fld})} \in V)$
199	198	a1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to ((k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) \in V \land Fun (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) \land 0_{{Poly}_{1} (ℂ_{fld})} \in V)$
200	154 93 57 21	coe1sfi	$⊢ a \in {Base}_{{Poly}_{1} (ℂ_{fld})} \to {finSupp}_{0} ({coe}_{1} (a))$
201	152 200	syl	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {finSupp}_{0} ({coe}_{1} (a))$
202	201	fsuppimpd	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {coe}_{1} (a) supp 0 \in Fin$
203	179	feqmptd	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {coe}_{1} (a) = (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k))$
204	203	oveq1d	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {coe}_{1} (a) supp 0 = (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k)) supp 0$
205		eqimss2	$⊢ {coe}_{1} (a) supp 0 = (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k)) supp 0 \to (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k)) supp 0 \subseteq {coe}_{1} (a) supp 0$
206	204 205	syl	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k)) supp 0 \subseteq {coe}_{1} (a) supp 0$
207	13 171	mp1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {Poly}_{1} (ℂ_{fld}) \in LMod$
208	93 191 153 21 158	lmod0vs	$⊢ ({Poly}_{1} (ℂ_{fld}) \in LMod \land x \in {Base}_{{Poly}_{1} (ℂ_{fld})}) \to 0 \cdot_{{Poly}_{1} (ℂ_{fld})} x = 0_{{Poly}_{1} (ℂ_{fld})}$
209	207 208	sylan	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land x \in {Base}_{{Poly}_{1} (ℂ_{fld})}) \to 0 \cdot_{{Poly}_{1} (ℂ_{fld})} x = 0_{{Poly}_{1} (ℂ_{fld})}$
210		c0ex	$⊢ 0 \in V$
211	210	a1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to 0 \in V$
212	206 209 180 189 211	suppssov1	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) supp 0_{{Poly}_{1} (ℂ_{fld})} \subseteq {coe}_{1} (a) supp 0$
213		suppssfifsupp	$⊢ (((k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) \in V \land Fun (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) \land 0_{{Poly}_{1} (ℂ_{fld})} \in V) \land ({coe}_{1} (a) supp 0 \in Fin \land (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) supp 0_{{Poly}_{1} (ℂ_{fld})} \subseteq {coe}_{1} (a) supp 0)) \to {finSupp}_{0_{{Poly}_{1} (ℂ_{fld})}} ((k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))))$
214	199 202 212 213	syl12anc	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {finSupp}_{0_{{Poly}_{1} (ℂ_{fld})}} ((k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))))$
215	93 158 162 164 166 170 194 214	gsummhm	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to \sum_{ℂ_{fld} ↑_{𝑠} ℂ} (E \circ (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})))) = E (\underset{k \in ℕ_{0}}{\sum_{{Poly}_{1} (ℂ_{fld})}} ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))))$
216	95	a1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to E : {Base}_{{Poly}_{1} (ℂ_{fld})} ⟶ {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
217	216 193	cofmpt	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to E \circ (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) = (k \in ℕ_{0} ⟼ E ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))))$
218	13	a1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to ℂ_{fld} \in Ring$
219	10	a1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to ℂ \in V$
220	95	ffvelrni	$⊢ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) \in {Base}_{{Poly}_{1} (ℂ_{fld})} \to E ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) \in {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
221	193 220	syl	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to E ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) \in {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
222	7 8 67 218 219 221	pwselbas	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to E ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) : ℂ ⟶ ℂ$
223	222	feqmptd	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to E ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) = (z \in ℂ ⟼ E ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) (z))$
224	56	a1i	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to ℂ_{fld} \in CRing$
225		simpr	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to z \in ℂ$
226	4 114 8 57 93 224 225	evl1vard	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to ({var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})} \land E ({var}_{1} (ℂ_{fld})) (z) = z)$
227	184	adantr	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to k \in ℕ_{0}$
228	4 57 8 93 224 225 226 116 127 227	evl1expd	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})} \land E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) (z) = k \cdot_{{mulGrp}_{ℂ_{fld}}} z)$
229	225 227 131	syl2anc	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to k \cdot_{{mulGrp}_{ℂ_{fld}}} z = z^{k}$
230	229	eqeq2d	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to (E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) (z) = k \cdot_{{mulGrp}_{ℂ_{fld}}} z \leftrightarrow E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) (z) = z^{k})$
231	230	anbi2d	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to ((k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})} \land E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) (z) = k \cdot_{{mulGrp}_{ℂ_{fld}}} z) \leftrightarrow (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})} \land E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) (z) = z^{k}))$
232	228 231	mpbid	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})} \land E (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) (z) = z^{k})$
233	181	adantr	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to {coe}_{1} (a) (k) \in ℂ$
234	4 57 8 93 224 225 232 233 153 80	evl1vsd	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})) \in {Base}_{{Poly}_{1} (ℂ_{fld})} \land E ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) (z) = {coe}_{1} (a) (k) z^{k})$
235	234	simprd	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to E ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) (z) = {coe}_{1} (a) (k) z^{k}$
236	235	mpteq2dva	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to (z \in ℂ ⟼ E ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) (z)) = (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})$
237	223 236	eqtrd	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to E ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) = (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})$
238	237	mpteq2dva	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to (k \in ℕ_{0} ⟼ E ({coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})))) = (k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k}))$
239	217 238	eqtrd	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to E \circ (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) = (k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k}))$
240	239	oveq2d	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to \sum_{ℂ_{fld} ↑_{𝑠} ℂ} (E \circ (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})))) = \underset{k \in ℕ_{0}}{\sum_{ℂ_{fld} ↑_{𝑠} ℂ}} (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})$
241	157 215 240	3eqtr2d	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to E (a) = \underset{k \in ℕ_{0}}{\sum_{ℂ_{fld} ↑_{𝑠} ℂ}} (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})$
242	10	a1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to ℂ \in V$
243	13 14	mp1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to ℂ_{fld} \in CMnd$
244	181	adantlr	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in ℕ_{0}) \to {coe}_{1} (a) (k) \in ℂ$
245	37	adantll	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in ℕ_{0}) \to z^{k} \in ℂ$
246	244 245	mulcld	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in ℕ_{0}) \to {coe}_{1} (a) (k) z^{k} \in ℂ$
247	246	anasss	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land (z \in ℂ \land k \in ℕ_{0})) \to {coe}_{1} (a) (k) z^{k} \in ℂ$
248	165	mptex	$⊢ (k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})) \in V$
249		funmpt	$⊢ Fun (k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k}))$
250	248 249 43	3pm3.2i	$⊢ ((k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})) \in V \land Fun (k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})) \land 0_{(ℂ_{fld} ↑_{𝑠} ℂ)} \in V)$
251	250	a1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to ((k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})) \in V \land Fun (k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})) \land 0_{(ℂ_{fld} ↑_{𝑠} ℂ)} \in V)$
252		fzfid	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \in Fin$
253		eldifn	$⊢ k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))) \to \neg k \in (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))$
254	253	adantl	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to \neg k \in (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))$
255	152	ad2antrr	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to a \in {Base}_{{Poly}_{1} (ℂ_{fld})}$
256		eldifi	$⊢ k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))) \to k \in ℕ_{0}$
257	256	adantl	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to k \in ℕ_{0}$
258		eqid	$⊢ \deg_{1} (ℂ_{fld}) = \deg_{1} (ℂ_{fld})$
259	258 57 93 21 154	deg1ge	$⊢ (a \in {Base}_{{Poly}_{1} (ℂ_{fld})} \land k \in ℕ_{0} \land {coe}_{1} (a) (k) \neq 0) \to k \leq \deg_{1} (ℂ_{fld}) (a)$
260	259	3expia	$⊢ (a \in {Base}_{{Poly}_{1} (ℂ_{fld})} \land k \in ℕ_{0}) \to ({coe}_{1} (a) (k) \neq 0 \to k \leq \deg_{1} (ℂ_{fld}) (a))$
261	255 257 260	syl2anc	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to ({coe}_{1} (a) (k) \neq 0 \to k \leq \deg_{1} (ℂ_{fld}) (a))$
262		0xr	$⊢ 0 \in ℝ^{*}$
263	258 57 93	deg1xrcl	$⊢ a \in {Base}_{{Poly}_{1} (ℂ_{fld})} \to \deg_{1} (ℂ_{fld}) (a) \in ℝ^{*}$
264	152 263	syl	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to \deg_{1} (ℂ_{fld}) (a) \in ℝ^{*}$
265	264	ad2antrr	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to \deg_{1} (ℂ_{fld}) (a) \in ℝ^{*}$
266		xrmax2	$⊢ (0 \in ℝ^{} \land \deg_{1} (ℂ_{fld}) (a) \in ℝ^{}) \to \deg_{1} (ℂ_{fld}) (a) \leq if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)$
267	262 265 266	sylancr	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to \deg_{1} (ℂ_{fld}) (a) \leq if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)$
268	257	nn0red	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to k \in ℝ$
269	268	rexrd	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to k \in ℝ^{*}$
270		ifcl	$⊢ (\deg_{1} (ℂ_{fld}) (a) \in ℝ^{} \land 0 \in ℝ^{}) \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℝ^{*}$
271	265 262 270	sylancl	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℝ^{*}$
272		xrletr	$⊢ (k \in ℝ^{} \land \deg_{1} (ℂ_{fld}) (a) \in ℝ^{} \land if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℝ^{*}) \to ((k \leq \deg_{1} (ℂ_{fld}) (a) \land \deg_{1} (ℂ_{fld}) (a) \leq if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \to k \leq if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))$
273	269 265 271 272	syl3anc	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to ((k \leq \deg_{1} (ℂ_{fld}) (a) \land \deg_{1} (ℂ_{fld}) (a) \leq if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \to k \leq if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))$
274	267 273	mpan2d	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to (k \leq \deg_{1} (ℂ_{fld}) (a) \to k \leq if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))$
275	261 274	syld	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to ({coe}_{1} (a) (k) \neq 0 \to k \leq if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))$
276	275 257	jctild	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to ({coe}_{1} (a) (k) \neq 0 \to (k \in ℕ_{0} \land k \leq if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))$
277	258 57 93	deg1cl	$⊢ a \in {Base}_{{Poly}_{1} (ℂ_{fld})} \to \deg_{1} (ℂ_{fld}) (a) \in (ℕ_{0} \cup \{−∞\})$
278	152 277	syl	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to \deg_{1} (ℂ_{fld}) (a) \in (ℕ_{0} \cup \{−∞\})$
279		elun	$⊢ \deg_{1} (ℂ_{fld}) (a) \in (ℕ_{0} \cup \{−∞\}) \leftrightarrow (\deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \lor \deg_{1} (ℂ_{fld}) (a) \in \{−∞\})$
280	278 279	sylib	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to (\deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \lor \deg_{1} (ℂ_{fld}) (a) \in \{−∞\})$
281		nn0ge0	$⊢ \deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \to 0 \leq \deg_{1} (ℂ_{fld}) (a)$
282	281	iftrued	$⊢ \deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) = \deg_{1} (ℂ_{fld}) (a)$
283		id	$⊢ \deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \to \deg_{1} (ℂ_{fld}) (a) \in ℕ_{0}$
284	282 283	eqeltrd	$⊢ \deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℕ_{0}$
285		mnflt0	$⊢ −∞ < 0$
286		mnfxr	$⊢ −∞ \in ℝ^{*}$
287		xrltnle	$⊢ (−∞ \in ℝ^{} \land 0 \in ℝ^{}) \to (−∞ < 0 \leftrightarrow \neg 0 \leq −∞)$
288	286 262 287	mp2an	$⊢ −∞ < 0 \leftrightarrow \neg 0 \leq −∞$
289	285 288	mpbi	$⊢ \neg 0 \leq −∞$
290		elsni	$⊢ \deg_{1} (ℂ_{fld}) (a) \in \{−∞\} \to \deg_{1} (ℂ_{fld}) (a) = −∞$
291	290	breq2d	$⊢ \deg_{1} (ℂ_{fld}) (a) \in \{−∞\} \to (0 \leq \deg_{1} (ℂ_{fld}) (a) \leftrightarrow 0 \leq −∞)$
292	289 291	mtbiri	$⊢ \deg_{1} (ℂ_{fld}) (a) \in \{−∞\} \to \neg 0 \leq \deg_{1} (ℂ_{fld}) (a)$
293	292	iffalsed	$⊢ \deg_{1} (ℂ_{fld}) (a) \in \{−∞\} \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) = 0$
294		0nn0	$⊢ 0 \in ℕ_{0}$
295	293 294	eqeltrdi	$⊢ \deg_{1} (ℂ_{fld}) (a) \in \{−∞\} \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℕ_{0}$
296	284 295	jaoi	$⊢ (\deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \lor \deg_{1} (ℂ_{fld}) (a) \in \{−∞\}) \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℕ_{0}$
297	280 296	syl	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℕ_{0}$
298	297	ad2antrr	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℕ_{0}$
299		fznn0	$⊢ if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℕ_{0} \to (k \in (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \leftrightarrow (k \in ℕ_{0} \land k \leq if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))$
300	298 299	syl	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to (k \in (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \leftrightarrow (k \in ℕ_{0} \land k \leq if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))$
301	276 300	sylibrd	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to ({coe}_{1} (a) (k) \neq 0 \to k \in (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))$
302	301	necon1bd	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to (\neg k \in (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \to {coe}_{1} (a) (k) = 0)$
303	254 302	mpd	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to {coe}_{1} (a) (k) = 0$
304	303	oveq1d	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to {coe}_{1} (a) (k) z^{k} = 0 \cdot z^{k}$
305	256 245	sylan2	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to z^{k} \in ℂ$
306	305	mul02d	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to 0 \cdot z^{k} = 0$
307	304 306	eqtrd	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to {coe}_{1} (a) (k) z^{k} = 0$
308	307	an32s	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \land z \in ℂ) \to {coe}_{1} (a) (k) z^{k} = 0$
309	308	mpteq2dva	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k}) = (z \in ℂ ⟼ 0)$
310		fconstmpt	$⊢ ℂ \times \{0\} = (z \in ℂ ⟼ 0)$
311		ringmnd	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Mnd$
312	13 311	ax-mp	$⊢ ℂ_{fld} \in Mnd$
313	7 21	pws0g	$⊢ (ℂ_{fld} \in Mnd \land ℂ \in V) \to ℂ \times \{0\} = 0_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
314	312 10 313	mp2an	$⊢ ℂ \times \{0\} = 0_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
315	310 314	eqtr3i	$⊢ (z \in ℂ ⟼ 0) = 0_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
316	309 315	eqtrdi	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k}) = 0_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
317	316 166	suppss2	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to (k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})) supp 0_{(ℂ_{fld} ↑_{𝑠} ℂ)} \subseteq (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))$
318		suppssfifsupp	$⊢ (((k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})) \in V \land Fun (k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})) \land 0_{(ℂ_{fld} ↑_{𝑠} ℂ)} \in V) \land ((0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \in Fin \land (k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})) supp 0_{(ℂ_{fld} ↑_{𝑠} ℂ)} \subseteq (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to {finSupp}_{0_{(ℂ_{fld} ↑_{𝑠} ℂ)}} ((k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})))$
319	251 252 317 318	syl12anc	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {finSupp}_{0_{(ℂ_{fld} ↑_{𝑠} ℂ)}} ((k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})))$
320	7 8 9 242 166 243 247 319	pwsgsum	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to \underset{k \in ℕ_{0}}{\sum_{ℂ_{fld} ↑_{𝑠} ℂ}} (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k}) = (z \in ℂ ⟼ \underset{k \in ℕ_{0}}{\sum_{ℂ_{fld}}} {coe}_{1} (a) (k) z^{k})$
321		fz0ssnn0	$⊢ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \subseteq ℕ_{0}$
322		resmpt	$⊢ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \subseteq ℕ_{0} \to {(k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) ↾}_{(0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))} = (k \in (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) ⟼ {coe}_{1} (a) (k) z^{k})$
323	321 322	ax-mp	$⊢ {(k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) ↾}_{(0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))} = (k \in (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) ⟼ {coe}_{1} (a) (k) z^{k})$
324	323	oveq2i	$⊢ \sum_{ℂ_{fld}} ({(k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) ↾}_{(0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))}) = {\sum_{ℂ_{fld}}}_{k = 0}^{if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)} {coe}_{1} (a) (k) z^{k}$
325	13 14	mp1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to ℂ_{fld} \in CMnd$
326	165	a1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to ℕ_{0} \in V$
327	246	fmpttd	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) : ℕ_{0} ⟶ ℂ$
328	307 326	suppss2	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) supp 0 \subseteq (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))$
329	165	mptex	$⊢ (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) \in V$
330		funmpt	$⊢ Fun (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k})$
331	329 330 210	3pm3.2i	$⊢ ((k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) \in V \land Fun (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) \land 0 \in V)$
332	331	a1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to ((k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) \in V \land Fun (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) \land 0 \in V)$
333		fzfid	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \in Fin$
334		suppssfifsupp	$⊢ (((k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) \in V \land Fun (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) \land 0 \in V) \land ((0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \in Fin \land (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) supp 0 \subseteq (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)))) \to {finSupp}_{0} ((k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}))$
335	332 333 328 334	syl12anc	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to {finSupp}_{0} ((k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}))$
336	8 21 325 326 327 328 335	gsumres	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to \sum_{ℂ_{fld}} ({(k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) ↾}_{(0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))}) = \underset{k \in ℕ_{0}}{\sum_{ℂ_{fld}}} {coe}_{1} (a) (k) z^{k}$
337		elfznn0	$⊢ k \in (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \to k \in ℕ_{0}$
338	337 246	sylan2	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))) \to {coe}_{1} (a) (k) z^{k} \in ℂ$
339	333 338	gsumfsum	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to {\sum_{ℂ_{fld}}}_{k = 0}^{if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)} {coe}_{1} (a) (k) z^{k} = \sum_{k = 0}^{if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)} {coe}_{1} (a) (k) z^{k}$
340	324 336 339	3eqtr3a	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to \underset{k \in ℕ_{0}}{\sum_{ℂ_{fld}}} {coe}_{1} (a) (k) z^{k} = \sum_{k = 0}^{if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)} {coe}_{1} (a) (k) z^{k}$
341	340	mpteq2dva	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to (z \in ℂ ⟼ \underset{k \in ℕ_{0}}{\sum_{ℂ_{fld}}} {coe}_{1} (a) (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)} {coe}_{1} (a) (k) z^{k})$
342	241 320 341	3eqtrd	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to E (a) = (z \in ℂ ⟼ \sum_{k = 0}^{if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)} {coe}_{1} (a) (k) z^{k})$
343	16	adantr	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to S \subseteq ℂ$
344		elplyr	$⊢ (S \subseteq ℂ \land if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℕ_{0} \land {coe}_{1} (a) : ℕ_{0} ⟶ S) \to (z \in ℂ ⟼ \sum_{k = 0}^{if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)} {coe}_{1} (a) (k) z^{k}) \in Poly (S)$
345	343 297 179 344	syl3anc	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to (z \in ℂ ⟼ \sum_{k = 0}^{if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)} {coe}_{1} (a) (k) z^{k}) \in Poly (S)$
346	342 345	eqeltrd	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to E (a) \in Poly (S)$
347		eleq1	$⊢ E (a) = f \to (E (a) \in Poly (S) \leftrightarrow f \in Poly (S))$
348	346 347	syl5ibcom	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to (E (a) = f \to f \in Poly (S))$
349	348	rexlimdva	$⊢ S \in SubRing (ℂ_{fld}) \to (\exists a \in A E (a) = f \to f \in Poly (S))$
350	151 349	syl5	$⊢ S \in SubRing (ℂ_{fld}) \to (f \in E [A] \to f \in Poly (S))$
351	147 350	impbid	$⊢ S \in SubRing (ℂ_{fld}) \to (f \in Poly (S) \leftrightarrow f \in E [A])$
352	351	eqrdv	$⊢ S \in SubRing (ℂ_{fld}) \to Poly (S) = E [A]$

Metamath Proof Explorer

Theorem plypf1

Proof