Metamath Proof Explorer

Theorem mpfmulcl

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

Ref Expression
Hypotheses mpfsubrg.q 
|- Q = ran ( ( I evalSub S ) ` R )
mpfmulcl.t 
|- .x. = ( .r ` S )
Assertion mpfmulcl 
|- ( ( F e. Q /\ G e. Q ) -> ( F oF .x. G ) e. Q )

Proof

Step Hyp Ref Expression
1 mpfsubrg.q 
 |-  Q = ran ( ( I evalSub S ) ` R )
2 mpfmulcl.t 
 |-  .x. = ( .r ` 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 
 |-  ( .r ` ( S ^s ( ( Base ` S ) ^m I ) ) ) = ( .r ` ( S ^s ( ( Base ` S ) ^m I ) ) )
18 3 4 7 8 14 16 2 17 pwsmulrval 
 |-  ( ( F e. Q /\ G e. Q ) -> ( F ( .r ` ( S ^s ( ( Base ` S ) ^m I ) ) ) G ) = ( F oF .x. G ) )
19 17 subrgmcl 
 |-  ( ( Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) /\ F e. Q /\ G e. Q ) -> ( F ( .r ` ( 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 ( .r ` ( S ^s ( ( Base ` S ) ^m I ) ) ) G ) e. Q ) )
21 10 20 mpcom 
 |-  ( ( F e. Q /\ G e. Q ) -> ( F ( .r ` ( S ^s ( ( Base ` S ) ^m I ) ) ) G ) e. Q )
22 18 21 eqeltrrd 
 |-  ( ( F e. Q /\ G e. Q ) -> ( F oF .x. G ) e. Q )