Metamath Proof Explorer

Theorem pf1addcl

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

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

Proof

Step Hyp Ref Expression
1 pf1rcl.q 
 |-  Q = ran ( eval1 ` R )
2 pf1addcl.a 
 |-  .+ = ( +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 )
6 5 adantr 
 |-  ( ( 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 ) )
10 9 adantr 
 |-  ( ( 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 ) )
16 15 adantl 
 |-  ( ( 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 )