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=ranIevalSubSR
mpfmulcl.t ·˙=S
Assertion mpfmulcl FQGQF·˙fGQ

Proof

Step Hyp Ref Expression
1 mpfsubrg.q Q=ranIevalSubSR
2 mpfmulcl.t ·˙=S
3 eqid S𝑠BaseSI=S𝑠BaseSI
4 eqid BaseS𝑠BaseSI=BaseS𝑠BaseSI
5 1 mpfrcl FQIVSCRingRSubRingS
6 5 adantr FQGQIVSCRingRSubRingS
7 6 simp2d FQGQSCRing
8 ovexd FQGQBaseSIV
9 1 mpfsubrg IVSCRingRSubRingSQSubRingS𝑠BaseSI
10 6 9 syl FQGQQSubRingS𝑠BaseSI
11 4 subrgss QSubRingS𝑠BaseSIQBaseS𝑠BaseSI
12 10 11 syl FQGQQBaseS𝑠BaseSI
13 simpl FQGQFQ
14 12 13 sseldd FQGQFBaseS𝑠BaseSI
15 simpr FQGQGQ
16 12 15 sseldd FQGQGBaseS𝑠BaseSI
17 eqid S𝑠BaseSI=S𝑠BaseSI
18 3 4 7 8 14 16 2 17 pwsmulrval FQGQFS𝑠BaseSIG=F·˙fG
19 17 subrgmcl QSubRingS𝑠BaseSIFQGQFS𝑠BaseSIGQ
20 19 3expib QSubRingS𝑠BaseSIFQGQFS𝑠BaseSIGQ
21 10 20 mpcom FQGQFS𝑠BaseSIGQ
22 18 21 eqeltrrd FQGQF·˙fGQ