Theorem plyaddlem

Description: Lemma for plyadd . (Contributed by Mario Carneiro, 21-Jul-2014)

	Ref	Expression
Hypotheses	plyadd.1	$$⊢\phi \to F\in \mathrm{Poly}\left(S\right)$$
	plyadd.2	$$⊢\phi \to G\in \mathrm{Poly}\left(S\right)$$
	plyadd.3	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to x+y\in S$$
	plyadd.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	plyadd.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	plyadd.a	$$⊢\phi \to A\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)$$
	plyadd.b	$$⊢\phi \to B\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)$$
	plyadd.a2	$$⊢\phi \to A\left[{\mathbb{Z}}_{\ge \left(M+1\right)}\right]=\left\{0\right\}$$
	plyadd.b2	$$⊢\phi \to B\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
	plyadd.f	$$⊢\phi \to F=\left(z\in ℂ⟼\sum _{k=0}^{M}A\left(k\right)z^k\right)$$
	plyadd.g	$$⊢\phi \to G=\left(z\in ℂ⟼\sum _{k=0}^{N}B\left(k\right)z^k\right)$$
Assertion	plyaddlem	$$⊢\phi \to F{+}_{f}G\in \mathrm{Poly}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		plyadd.1	$$⊢\phi \to F\in \mathrm{Poly}\left(S\right)$$
2		plyadd.2	$$⊢\phi \to G\in \mathrm{Poly}\left(S\right)$$
3		plyadd.3	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to x+y\in S$$
4		plyadd.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
5		plyadd.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
6		plyadd.a	$$⊢\phi \to A\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)$$
7		plyadd.b	$$⊢\phi \to B\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)$$
8		plyadd.a2	$$⊢\phi \to A\left[{\mathbb{Z}}_{\ge \left(M+1\right)}\right]=\left\{0\right\}$$
9		plyadd.b2	$$⊢\phi \to B\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
10		plyadd.f	$$⊢\phi \to F=\left(z\in ℂ⟼\sum _{k=0}^{M}A\left(k\right)z^k\right)$$
11		plyadd.g	$$⊢\phi \to G=\left(z\in ℂ⟼\sum _{k=0}^{N}B\left(k\right)z^k\right)$$
12		plybss	$$⊢F\in \mathrm{Poly}\left(S\right)\to S\subseteq ℂ$$
13	1 12	syl	$$⊢\phi \to S\subseteq ℂ$$
14		0cnd	$$⊢\phi \to 0\in ℂ$$
15	14	snssd	$$⊢\phi \to \left\{0\right\}\subseteq ℂ$$
16	13 15	unssd	$$⊢\phi \to S\cup \left\{0\right\}\subseteq ℂ$$
17		cnex	$$⊢ℂ\in \mathrm{V}$$
18		ssexg	$$⊢\left(S\cup \left\{0\right\}\subseteq ℂ\wedge ℂ\in \mathrm{V}\right)\to S\cup \left\{0\right\}\in \mathrm{V}$$
19	16 17 18	sylancl	$$⊢\phi \to S\cup \left\{0\right\}\in \mathrm{V}$$
20		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
21		elmapg	$$⊢\left(S\cup \left\{0\right\}\in \mathrm{V}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)\to \left(A\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\leftrightarrow A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}\right)$$
22	19 20 21	sylancl	$$⊢\phi \to \left(A\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\leftrightarrow A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}\right)$$
23	6 22	mpbid	$$⊢\phi \to A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}$$
24	23 16	fssd	$$⊢\phi \to A:{\mathbb{N}}_0⟶ℂ$$
25		elmapg	$$⊢\left(S\cup \left\{0\right\}\in \mathrm{V}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)\to \left(B\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\leftrightarrow B:{\mathbb{N}}_0⟶S\cup \left\{0\right\}\right)$$
26	19 20 25	sylancl	$$⊢\phi \to \left(B\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\leftrightarrow B:{\mathbb{N}}_0⟶S\cup \left\{0\right\}\right)$$
27	7 26	mpbid	$$⊢\phi \to B:{\mathbb{N}}_0⟶S\cup \left\{0\right\}$$
28	27 16	fssd	$$⊢\phi \to B:{\mathbb{N}}_0⟶ℂ$$
29	1 2 4 5 24 28 8 9 10 11	plyaddlem1	$$⊢\phi \to F{+}_{f}G=\left(z\in ℂ⟼\sum _{k=0}^{if\left(M\le N,N,M\right)}\left(A{+}_{f}B\right)\left(k\right)z^k\right)$$
30	5 4	ifcld	$$⊢\phi \to if\left(M\le N,N,M\right)\in {\mathbb{N}}_0$$
31		eqid	$$⊢S\cup \left\{0\right\}=S\cup \left\{0\right\}$$
32	13 31 3	un0addcl	$$⊢\left(\phi \wedge \left(x\in \left(S\cup \left\{0\right\}\right)\wedge y\in \left(S\cup \left\{0\right\}\right)\right)\right)\to x+y\in \left(S\cup \left\{0\right\}\right)$$
33	20	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
34		inidm	$$⊢{\mathbb{N}}_0\cap {\mathbb{N}}_0={\mathbb{N}}_0$$
35	32 23 27 33 33 34	off	$$⊢\phi \to \left(A{+}_{f}B\right):{\mathbb{N}}_0⟶S\cup \left\{0\right\}$$
36		elfznn0	$$⊢k\in \left(0\dots if\left(M\le N,N,M\right)\right)\to k\in {\mathbb{N}}_0$$
37		ffvelrn	$$⊢\left(\left(A{+}_{f}B\right):{\mathbb{N}}_0⟶S\cup \left\{0\right\}\wedge k\in {\mathbb{N}}_0\right)\to \left(A{+}_{f}B\right)\left(k\right)\in \left(S\cup \left\{0\right\}\right)$$
38	35 36 37	syl2an	$$⊢\left(\phi \wedge k\in \left(0\dots if\left(M\le N,N,M\right)\right)\right)\to \left(A{+}_{f}B\right)\left(k\right)\in \left(S\cup \left\{0\right\}\right)$$
39	16 30 38	elplyd	$$⊢\phi \to \left(z\in ℂ⟼\sum _{k=0}^{if\left(M\le N,N,M\right)}\left(A{+}_{f}B\right)\left(k\right)z^k\right)\in \mathrm{Poly}\left(S\cup \left\{0\right\}\right)$$
40	29 39	eqeltrd	$$⊢\phi \to F{+}_{f}G\in \mathrm{Poly}\left(S\cup \left\{0\right\}\right)$$
41		plyun0	$$⊢\mathrm{Poly}\left(S\cup \left\{0\right\}\right)=\mathrm{Poly}\left(S\right)$$
42	40 41	eleqtrdi	$$⊢\phi \to F{+}_{f}G\in \mathrm{Poly}\left(S\right)$$