Metamath Proof Explorer

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

Ref Expression
Hypotheses pf1rcl.q
`|- Q = ran ( eval1 ` R )`
`|- .+ = ( +g ` R )`
`|- ( ( F e. Q /\ G e. Q ) -> ( F oF .+ G ) e. Q )`

Proof

Step Hyp Ref Expression
1 pf1rcl.q
` |-  Q = ran ( eval1 ` R )`
` |-  .+ = ( +g ` R )`
3 eqid
` |-  ( R ^s ( Base ` R ) ) = ( R ^s ( Base ` R ) )`
4 eqid
` |-  ( Base ` ( R ^s ( Base ` R ) ) ) = ( Base ` ( R ^s ( Base ` R ) ) )`
5 1 pf1rcl
` |-  ( F e. Q -> R e. CRing )`
` |-  ( ( F e. Q /\ G e. Q ) -> R e. CRing )`
7 fvexd
` |-  ( ( F e. Q /\ G e. Q ) -> ( Base ` R ) e. _V )`
8 eqid
` |-  ( Base ` R ) = ( Base ` R )`
9 1 8 pf1f
` |-  ( F e. Q -> F : ( Base ` R ) --> ( Base ` R ) )`
` |-  ( ( F e. Q /\ G e. Q ) -> F : ( Base ` R ) --> ( Base ` R ) )`
11 fvex
` |-  ( Base ` R ) e. _V`
12 3 8 4 pwselbasb
` |-  ( ( R e. CRing /\ ( Base ` R ) e. _V ) -> ( F e. ( Base ` ( R ^s ( Base ` R ) ) ) <-> F : ( Base ` R ) --> ( Base ` R ) ) )`
13 6 11 12 sylancl
` |-  ( ( F e. Q /\ G e. Q ) -> ( F e. ( Base ` ( R ^s ( Base ` R ) ) ) <-> F : ( Base ` R ) --> ( Base ` R ) ) )`
14 10 13 mpbird
` |-  ( ( F e. Q /\ G e. Q ) -> F e. ( Base ` ( R ^s ( Base ` R ) ) ) )`
15 1 8 pf1f
` |-  ( G e. Q -> G : ( Base ` R ) --> ( Base ` R ) )`
` |-  ( ( F e. Q /\ G e. Q ) -> G : ( Base ` R ) --> ( Base ` R ) )`
17 3 8 4 pwselbasb
` |-  ( ( R e. CRing /\ ( Base ` R ) e. _V ) -> ( G e. ( Base ` ( R ^s ( Base ` R ) ) ) <-> G : ( Base ` R ) --> ( Base ` R ) ) )`
18 6 11 17 sylancl
` |-  ( ( F e. Q /\ G e. Q ) -> ( G e. ( Base ` ( R ^s ( Base ` R ) ) ) <-> G : ( Base ` R ) --> ( Base ` R ) ) )`
19 16 18 mpbird
` |-  ( ( F e. Q /\ G e. Q ) -> G e. ( Base ` ( R ^s ( Base ` R ) ) ) )`
20 eqid
` |-  ( +g ` ( R ^s ( Base ` R ) ) ) = ( +g ` ( R ^s ( Base ` R ) ) )`
21 3 4 6 7 14 19 2 20 pwsplusgval
` |-  ( ( F e. Q /\ G e. Q ) -> ( F ( +g ` ( R ^s ( Base ` R ) ) ) G ) = ( F oF .+ G ) )`
22 8 1 pf1subrg
` |-  ( R e. CRing -> Q e. ( SubRing ` ( R ^s ( Base ` R ) ) ) )`
23 6 22 syl
` |-  ( ( F e. Q /\ G e. Q ) -> Q e. ( SubRing ` ( R ^s ( Base ` R ) ) ) )`
24 20 subrgacl
` |-  ( ( Q e. ( SubRing ` ( R ^s ( Base ` R ) ) ) /\ F e. Q /\ G e. Q ) -> ( F ( +g ` ( R ^s ( Base ` R ) ) ) G ) e. Q )`
25 24 3expib
` |-  ( Q e. ( SubRing ` ( R ^s ( Base ` R ) ) ) -> ( ( F e. Q /\ G e. Q ) -> ( F ( +g ` ( R ^s ( Base ` R ) ) ) G ) e. Q ) )`
26 23 25 mpcom
` |-  ( ( F e. Q /\ G e. Q ) -> ( F ( +g ` ( R ^s ( Base ` R ) ) ) G ) e. Q )`
27 21 26 eqeltrrd
` |-  ( ( F e. Q /\ G e. Q ) -> ( F oF .+ G ) e. Q )`