Metamath Proof Explorer


Theorem mpfaddcl

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

Ref Expression
Hypotheses mpfsubrg.q
|- Q = ran ( ( I evalSub S ) ` R )
mpfaddcl.p
|- .+ = ( +g ` S )
Assertion mpfaddcl
|- ( ( F e. Q /\ G e. Q ) -> ( F oF .+ G ) e. Q )

Proof

Step Hyp Ref Expression
1 mpfsubrg.q
 |-  Q = ran ( ( I evalSub S ) ` R )
2 mpfaddcl.p
 |-  .+ = ( +g ` S )
3 eqid
 |-  ( S ^s ( ( Base ` S ) ^m I ) ) = ( S ^s ( ( Base ` S ) ^m I ) )
4 eqid
 |-  ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) = ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) )
5 1 mpfrcl
 |-  ( F e. Q -> ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) )
6 5 adantr
 |-  ( ( F e. Q /\ G e. Q ) -> ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) )
7 6 simp2d
 |-  ( ( F e. Q /\ G e. Q ) -> S e. CRing )
8 ovexd
 |-  ( ( F e. Q /\ G e. Q ) -> ( ( Base ` S ) ^m I ) e. _V )
9 1 mpfsubrg
 |-  ( ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
10 6 9 syl
 |-  ( ( F e. Q /\ G e. Q ) -> Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
11 4 subrgss
 |-  ( Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) -> Q C_ ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
12 10 11 syl
 |-  ( ( F e. Q /\ G e. Q ) -> Q C_ ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
13 simpl
 |-  ( ( F e. Q /\ G e. Q ) -> F e. Q )
14 12 13 sseldd
 |-  ( ( F e. Q /\ G e. Q ) -> F e. ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
15 simpr
 |-  ( ( F e. Q /\ G e. Q ) -> G e. Q )
16 12 15 sseldd
 |-  ( ( F e. Q /\ G e. Q ) -> G e. ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
17 eqid
 |-  ( +g ` ( S ^s ( ( Base ` S ) ^m I ) ) ) = ( +g ` ( S ^s ( ( Base ` S ) ^m I ) ) )
18 3 4 7 8 14 16 2 17 pwsplusgval
 |-  ( ( F e. Q /\ G e. Q ) -> ( F ( +g ` ( S ^s ( ( Base ` S ) ^m I ) ) ) G ) = ( F oF .+ G ) )
19 17 subrgacl
 |-  ( ( Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) /\ F e. Q /\ G e. Q ) -> ( F ( +g ` ( S ^s ( ( Base ` S ) ^m I ) ) ) G ) e. Q )
20 19 3expib
 |-  ( Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) -> ( ( F e. Q /\ G e. Q ) -> ( F ( +g ` ( S ^s ( ( Base ` S ) ^m I ) ) ) G ) e. Q ) )
21 10 20 mpcom
 |-  ( ( F e. Q /\ G e. Q ) -> ( F ( +g ` ( S ^s ( ( Base ` S ) ^m I ) ) ) G ) e. Q )
22 18 21 eqeltrrd
 |-  ( ( F e. Q /\ G e. Q ) -> ( F oF .+ G ) e. Q )