Theorem mpfaddcl

Description: The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015)

	Ref	Expression
Hypotheses	mpfsubrg.q	$$⊢Q=\mathrm{ran}\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	mpfaddcl.p	$$⊢\underset{\dot{}}{+}={+}_S$$
Assertion	mpfaddcl	$$⊢\left(F\in Q\wedge G\in Q\right)\to F{\underset{\dot{}}{+}}_{f}G\in Q$$

Proof

Step	Hyp	Ref	Expression
1		mpfsubrg.q	$$⊢Q=\mathrm{ran}\left(I\mathrm{evalSub}S\right)\left(R\right)$$
2		mpfaddcl.p	$$⊢\underset{\dot{}}{+}={+}_S$$
3		eqid	$$⊢S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)=S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)$$
4		eqid	$$⊢{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}={\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}$$
5	1	mpfrcl	$$⊢F\in Q\to \left(I\in \mathrm{V}\wedge S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\right)$$
6	5	adantr	$$⊢\left(F\in Q\wedge G\in Q\right)\to \left(I\in \mathrm{V}\wedge S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\right)$$
7	6	simp2d	$$⊢\left(F\in Q\wedge G\in Q\right)\to S\in \mathrm{CRing}$$
8		ovexd	$$⊢\left(F\in Q\wedge G\in Q\right)\to {{\mathrm{Base}}_S}^I\in \mathrm{V}$$
9	1	mpfsubrg	$$⊢\left(I\in \mathrm{V}\wedge S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\right)\to Q\in \mathrm{SubRing}\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)$$
10	6 9	syl	$$⊢\left(F\in Q\wedge G\in Q\right)\to Q\in \mathrm{SubRing}\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)$$
11	4	subrgss	$$⊢Q\in \mathrm{SubRing}\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)\to Q\subseteq {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}$$
12	10 11	syl	$$⊢\left(F\in Q\wedge G\in Q\right)\to Q\subseteq {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}$$
13		simpl	$$⊢\left(F\in Q\wedge G\in Q\right)\to F\in Q$$
14	12 13	sseldd	$$⊢\left(F\in Q\wedge G\in Q\right)\to F\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}$$
15		simpr	$$⊢\left(F\in Q\wedge G\in Q\right)\to G\in Q$$
16	12 15	sseldd	$$⊢\left(F\in Q\wedge G\in Q\right)\to G\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}$$
17		eqid	$$⊢{+}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}={+}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}$$
18	3 4 7 8 14 16 2 17	pwsplusgval	$$⊢\left(F\in Q\wedge G\in Q\right)\to F{+}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}G=F{\underset{\dot{}}{+}}_{f}G$$
19	17	subrgacl	$$⊢\left(Q\in \mathrm{SubRing}\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)\wedge F\in Q\wedge G\in Q\right)\to F{+}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}G\in Q$$
20	19	3expib	$$⊢Q\in \mathrm{SubRing}\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)\to \left(\left(F\in Q\wedge G\in Q\right)\to F{+}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}G\in Q\right)$$
21	10 20	mpcom	$$⊢\left(F\in Q\wedge G\in Q\right)\to F{+}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}G\in Q$$
22	18 21	eqeltrrd	$$⊢\left(F\in Q\wedge G\in Q\right)\to F{\underset{\dot{}}{+}}_{f}G\in Q$$