Description: The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mpfsubrg.q | |
|
mpfmulcl.t | |
||
Assertion | mpfmulcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpfsubrg.q | |
|
2 | mpfmulcl.t | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | 1 | mpfrcl | |
6 | 5 | adantr | |
7 | 6 | simp2d | |
8 | ovexd | |
|
9 | 1 | mpfsubrg | |
10 | 6 9 | syl | |
11 | 4 | subrgss | |
12 | 10 11 | syl | |
13 | simpl | |
|
14 | 12 13 | sseldd | |
15 | simpr | |
|
16 | 12 15 | sseldd | |
17 | eqid | |
|
18 | 3 4 7 8 14 16 2 17 | pwsmulrval | |
19 | 17 | subrgmcl | |
20 | 19 | 3expib | |
21 | 10 20 | mpcom | |
22 | 18 21 | eqeltrrd | |