# Metamath Proof Explorer

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

Ref Expression
Hypotheses pf1rcl.q ${⊢}{Q}=\mathrm{ran}{\mathrm{eval}}_{1}\left({R}\right)$

### Proof

Step Hyp Ref Expression
1 pf1rcl.q ${⊢}{Q}=\mathrm{ran}{\mathrm{eval}}_{1}\left({R}\right)$
3 eqid ${⊢}{R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}={R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}$
4 eqid ${⊢}{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}={\mathrm{Base}}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}$
5 1 pf1rcl ${⊢}{F}\in {Q}\to {R}\in \mathrm{CRing}$
6 5 adantr ${⊢}\left({F}\in {Q}\wedge {G}\in {Q}\right)\to {R}\in \mathrm{CRing}$
7 fvexd ${⊢}\left({F}\in {Q}\wedge {G}\in {Q}\right)\to {\mathrm{Base}}_{{R}}\in \mathrm{V}$
8 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
9 1 8 pf1f ${⊢}{F}\in {Q}\to {F}:{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}$
10 9 adantr ${⊢}\left({F}\in {Q}\wedge {G}\in {Q}\right)\to {F}:{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}$
11 fvex ${⊢}{\mathrm{Base}}_{{R}}\in \mathrm{V}$
12 3 8 4 pwselbasb ${⊢}\left({R}\in \mathrm{CRing}\wedge {\mathrm{Base}}_{{R}}\in \mathrm{V}\right)\to \left({F}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}↔{F}:{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}\right)$
13 6 11 12 sylancl ${⊢}\left({F}\in {Q}\wedge {G}\in {Q}\right)\to \left({F}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}↔{F}:{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}\right)$
14 10 13 mpbird ${⊢}\left({F}\in {Q}\wedge {G}\in {Q}\right)\to {F}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}$
15 1 8 pf1f ${⊢}{G}\in {Q}\to {G}:{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}$
16 15 adantl ${⊢}\left({F}\in {Q}\wedge {G}\in {Q}\right)\to {G}:{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}$
17 3 8 4 pwselbasb ${⊢}\left({R}\in \mathrm{CRing}\wedge {\mathrm{Base}}_{{R}}\in \mathrm{V}\right)\to \left({G}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}↔{G}:{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}\right)$
18 6 11 17 sylancl ${⊢}\left({F}\in {Q}\wedge {G}\in {Q}\right)\to \left({G}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}↔{G}:{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}\right)$
19 16 18 mpbird ${⊢}\left({F}\in {Q}\wedge {G}\in {Q}\right)\to {G}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}$
20 eqid ${⊢}{+}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}={+}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}$
21 3 4 6 7 14 19 2 20 pwsplusgval
22 8 1 pf1subrg ${⊢}{R}\in \mathrm{CRing}\to {Q}\in \mathrm{SubRing}\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)$
23 6 22 syl ${⊢}\left({F}\in {Q}\wedge {G}\in {Q}\right)\to {Q}\in \mathrm{SubRing}\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)$
24 20 subrgacl ${⊢}\left({Q}\in \mathrm{SubRing}\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)\wedge {F}\in {Q}\wedge {G}\in {Q}\right)\to {F}{+}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}{G}\in {Q}$
25 24 3expib ${⊢}{Q}\in \mathrm{SubRing}\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)\to \left(\left({F}\in {Q}\wedge {G}\in {Q}\right)\to {F}{+}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}{G}\in {Q}\right)$
26 23 25 mpcom ${⊢}\left({F}\in {Q}\wedge {G}\in {Q}\right)\to {F}{+}_{\left({R}{↑}_{𝑠}{\mathrm{Base}}_{{R}}\right)}{G}\in {Q}$
27 21 26 eqeltrrd