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		ffvelcdm	$⊢ (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	imbitrrid	$⊢ 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	ffvelcdmda	$⊢ ((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 93	mgpbas	$⊢ {Base}_{{Poly}_{1} (ℂ_{fld})} = {Base}_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}}$
183	110	ringmgp	$⊢ {Poly}_{1} (ℂ_{fld}) \in Ring \to {mulGrp}_{{Poly}_{1} (ℂ_{fld})} \in Mnd$
184	160 183	mp1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to {mulGrp}_{{Poly}_{1} (ℂ_{fld})} \in Mnd$
185		simpr	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
186	114 57 93	vr1cl	$⊢ ℂ_{fld} \in Ring \to {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})}$
187	13 186	mp1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to {var}_{1} (ℂ_{fld}) \in {Base}_{{Poly}_{1} (ℂ_{fld})}$
188	182 116 184 185 187	mulgnn0cld	$⊢ ((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})}$
189	57	ply1sca	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} = Scalar ({Poly}_{1} (ℂ_{fld}))$
190	13 189	ax-mp	$⊢ ℂ_{fld} = Scalar ({Poly}_{1} (ℂ_{fld}))$
191	93 190 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})}$
192	172 181 188 191	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})}$
193	192	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})}$
194	165	mptex	$⊢ (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld}))) \in V$
195		funmpt	$⊢ Fun (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) \cdot_{{Poly}_{1} (ℂ_{fld})} (k \cdot_{{mulGrp}_{{Poly}_{1} (ℂ_{fld})}} {var}_{1} (ℂ_{fld})))$
196		fvex	$⊢ 0_{{Poly}_{1} (ℂ_{fld})} \in V$
197	194 195 196	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)$
198	197	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)$
199	154 93 57 21	coe1sfi	$⊢ a \in {Base}_{{Poly}_{1} (ℂ_{fld})} \to {finSupp}_{0} ({coe}_{1} (a))$
200	152 199	syl	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {finSupp}_{0} ({coe}_{1} (a))$
201	200	fsuppimpd	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {coe}_{1} (a) supp 0 \in Fin$
202	179	feqmptd	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {coe}_{1} (a) = (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k))$
203	202	oveq1d	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {coe}_{1} (a) supp 0 = (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k)) supp 0$
204		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$
205	203 204	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$
206	13 171	mp1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {Poly}_{1} (ℂ_{fld}) \in LMod$
207	93 190 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})}$
208	206 207	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})}$
209		c0ex	$⊢ 0 \in V$
210	209	a1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to 0 \in V$
211	205 208 180 188 210	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$
212		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}))))$
213	198 201 211 212	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}))))$
214	93 158 162 164 166 170 193 213	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}))))$
215	95	a1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to E : {Base}_{{Poly}_{1} (ℂ_{fld})} ⟶ {Base}_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
216	215 192	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}))))$
217	13	a1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to ℂ_{fld} \in Ring$
218	10	a1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \to ℂ \in V$
219	95	ffvelcdmi	$⊢ {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} ↑_{𝑠} ℂ)}$
220	192 219	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} ↑_{𝑠} ℂ)}$
221	7 8 67 217 218 220	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}))) : ℂ ⟶ ℂ$
222	221	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))$
223	56	a1i	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to ℂ_{fld} \in CRing$
224		simpr	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to z \in ℂ$
225	4 114 8 57 93 223 224	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)$
226	185	adantr	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to k \in ℕ_{0}$
227	4 57 8 93 223 224 225 116 127 226	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)$
228	224 226 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}$
229	228	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})$
230	229	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}))$
231	227 230	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})$
232	181	adantr	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land k \in ℕ_{0}) \land z \in ℂ) \to {coe}_{1} (a) (k) \in ℂ$
233	4 57 8 93 223 224 231 232 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})$
234	233	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}$
235	234	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})$
236	222 235	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})$
237	236	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}))$
238	216 237	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}))$
239	238	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})$
240	157 214 239	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})$
241	10	a1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to ℂ \in V$
242	13 14	mp1i	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to ℂ_{fld} \in CMnd$
243	181	adantlr	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in ℕ_{0}) \to {coe}_{1} (a) (k) \in ℂ$
244	37	adantll	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in ℕ_{0}) \to z^{k} \in ℂ$
245	243 244	mulcld	$⊢ (((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \land k \in ℕ_{0}) \to {coe}_{1} (a) (k) z^{k} \in ℂ$
246	245	anasss	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land (z \in ℂ \land k \in ℕ_{0})) \to {coe}_{1} (a) (k) z^{k} \in ℂ$
247	165	mptex	$⊢ (k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})) \in V$
248		funmpt	$⊢ Fun (k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k}))$
249	247 248 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)$
250	249	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)$
251		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$
252		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))$
253	252	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))$
254	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})}$
255		eldifi	$⊢ k \in (ℕ_{0} ∖ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0))) \to k \in ℕ_{0}$
256	255	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}$
257		eqid	$⊢ \deg_{1} (ℂ_{fld}) = \deg_{1} (ℂ_{fld})$
258	257 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)$
259	258	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))$
260	254 256 259	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))$
261		0xr	$⊢ 0 \in ℝ^{*}$
262	257 57 93	deg1xrcl	$⊢ a \in {Base}_{{Poly}_{1} (ℂ_{fld})} \to \deg_{1} (ℂ_{fld}) (a) \in ℝ^{*}$
263	152 262	syl	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to \deg_{1} (ℂ_{fld}) (a) \in ℝ^{*}$
264	263	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 ℝ^{*}$
265		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)$
266	261 264 265	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)$
267	256	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 ℝ$
268	267	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 ℝ^{*}$
269		ifcl	$⊢ (\deg_{1} (ℂ_{fld}) (a) \in ℝ^{} \land 0 \in ℝ^{}) \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℝ^{*}$
270	264 261 269	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 ℝ^{*}$
271		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))$
272	268 264 270 271	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))$
273	266 272	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))$
274	260 273	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))$
275	274 256	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)))$
276	257 57 93	deg1cl	$⊢ a \in {Base}_{{Poly}_{1} (ℂ_{fld})} \to \deg_{1} (ℂ_{fld}) (a) \in (ℕ_{0} \cup \{−∞\})$
277	152 276	syl	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to \deg_{1} (ℂ_{fld}) (a) \in (ℕ_{0} \cup \{−∞\})$
278		elun	$⊢ \deg_{1} (ℂ_{fld}) (a) \in (ℕ_{0} \cup \{−∞\}) \leftrightarrow (\deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \lor \deg_{1} (ℂ_{fld}) (a) \in \{−∞\})$
279	277 278	sylib	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to (\deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \lor \deg_{1} (ℂ_{fld}) (a) \in \{−∞\})$
280		nn0ge0	$⊢ \deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \to 0 \leq \deg_{1} (ℂ_{fld}) (a)$
281	280	iftrued	$⊢ \deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) = \deg_{1} (ℂ_{fld}) (a)$
282		id	$⊢ \deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \to \deg_{1} (ℂ_{fld}) (a) \in ℕ_{0}$
283	281 282	eqeltrd	$⊢ \deg_{1} (ℂ_{fld}) (a) \in ℕ_{0} \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℕ_{0}$
284		mnflt0	$⊢ −∞ < 0$
285		mnfxr	$⊢ −∞ \in ℝ^{*}$
286		xrltnle	$⊢ (−∞ \in ℝ^{} \land 0 \in ℝ^{}) \to (−∞ < 0 \leftrightarrow \neg 0 \leq −∞)$
287	285 261 286	mp2an	$⊢ −∞ < 0 \leftrightarrow \neg 0 \leq −∞$
288	284 287	mpbi	$⊢ \neg 0 \leq −∞$
289		elsni	$⊢ \deg_{1} (ℂ_{fld}) (a) \in \{−∞\} \to \deg_{1} (ℂ_{fld}) (a) = −∞$
290	289	breq2d	$⊢ \deg_{1} (ℂ_{fld}) (a) \in \{−∞\} \to (0 \leq \deg_{1} (ℂ_{fld}) (a) \leftrightarrow 0 \leq −∞)$
291	288 290	mtbiri	$⊢ \deg_{1} (ℂ_{fld}) (a) \in \{−∞\} \to \neg 0 \leq \deg_{1} (ℂ_{fld}) (a)$
292	291	iffalsed	$⊢ \deg_{1} (ℂ_{fld}) (a) \in \{−∞\} \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) = 0$
293		0nn0	$⊢ 0 \in ℕ_{0}$
294	292 293	eqeltrdi	$⊢ \deg_{1} (ℂ_{fld}) (a) \in \{−∞\} \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℕ_{0}$
295	283 294	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}$
296	279 295	syl	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0) \in ℕ_{0}$
297	296	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}$
298		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)))$
299	297 298	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)))$
300	275 299	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)))$
301	300	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)$
302	253 301	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$
303	302	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}$
304	255 244	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 ℂ$
305	304	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$
306	303 305	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$
307	306	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$
308	307	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)$
309		fconstmpt	$⊢ ℂ \times \{0\} = (z \in ℂ ⟼ 0)$
310		ringmnd	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Mnd$
311	13 310	ax-mp	$⊢ ℂ_{fld} \in Mnd$
312	7 21	pws0g	$⊢ (ℂ_{fld} \in Mnd \land ℂ \in V) \to ℂ \times \{0\} = 0_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
313	311 10 312	mp2an	$⊢ ℂ \times \{0\} = 0_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
314	309 313	eqtr3i	$⊢ (z \in ℂ ⟼ 0) = 0_{(ℂ_{fld} ↑_{𝑠} ℂ)}$
315	308 314	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} ↑_{𝑠} ℂ)}$
316	315 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))$
317		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})))$
318	250 251 316 317	syl12anc	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to {finSupp}_{0_{(ℂ_{fld} ↑_{𝑠} ℂ)}} ((k \in ℕ_{0} ⟼ (z \in ℂ ⟼ {coe}_{1} (a) (k) z^{k})))$
319	7 8 9 241 166 242 246 318	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})$
320		fz0ssnn0	$⊢ (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \subseteq ℕ_{0}$
321		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})$
322	320 321	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})$
323	322	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}$
324	13 14	mp1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to ℂ_{fld} \in CMnd$
325	165	a1i	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to ℕ_{0} \in V$
326	245	fmpttd	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) : ℕ_{0} ⟶ ℂ$
327	306 325	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))$
328	165	mptex	$⊢ (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}) \in V$
329		funmpt	$⊢ Fun (k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k})$
330	328 329 209	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)$
331	330	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)$
332		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$
333		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}))$
334	331 332 327 333	syl12anc	$⊢ ((S \in SubRing (ℂ_{fld}) \land a \in A) \land z \in ℂ) \to {finSupp}_{0} ((k \in ℕ_{0} ⟼ {coe}_{1} (a) (k) z^{k}))$
335	8 21 324 325 326 327 334	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}$
336		elfznn0	$⊢ k \in (0 \dots if (0 \leq \deg_{1} (ℂ_{fld}) (a), \deg_{1} (ℂ_{fld}) (a), 0)) \to k \in ℕ_{0}$
337	336 245	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 ℂ$
338	332 337	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}$
339	323 335 338	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}$
340	339	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})$
341	240 319 340	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})$
342	16	adantr	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to S \subseteq ℂ$
343		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)$
344	342 296 179 343	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)$
345	341 344	eqeltrd	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to E (a) \in Poly (S)$
346		eleq1	$⊢ E (a) = f \to (E (a) \in Poly (S) \leftrightarrow f \in Poly (S))$
347	345 346	syl5ibcom	$⊢ (S \in SubRing (ℂ_{fld}) \land a \in A) \to (E (a) = f \to f \in Poly (S))$
348	347	rexlimdva	$⊢ S \in SubRing (ℂ_{fld}) \to (\exists a \in A E (a) = f \to f \in Poly (S))$
349	151 348	syl5	$⊢ S \in SubRing (ℂ_{fld}) \to (f \in E [A] \to f \in Poly (S))$
350	147 349	impbid	$⊢ S \in SubRing (ℂ_{fld}) \to (f \in Poly (S) \leftrightarrow f \in E [A])$
351	350	eqrdv	$⊢ S \in SubRing (ℂ_{fld}) \to Poly (S) = E [A]$

Metamath Proof Explorer

Theorem plypf1

Proof