Metamath Proof Explorer


Theorem pf1mulcl

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

Ref Expression
Hypotheses pf1rcl.q Q = ran eval 1 R
pf1mulcl.t · ˙ = R
Assertion pf1mulcl F Q G Q F · ˙ f G Q

Proof

Step Hyp Ref Expression
1 pf1rcl.q Q = ran eval 1 R
2 pf1mulcl.t · ˙ = R
3 eqid R 𝑠 Base R = R 𝑠 Base R
4 eqid Base R 𝑠 Base R = Base R 𝑠 Base R
5 1 pf1rcl F Q R CRing
6 5 adantr F Q G Q R CRing
7 fvexd F Q G Q Base R V
8 eqid Base R = Base R
9 1 8 pf1f F Q F : Base R Base R
10 9 adantr F Q G Q F : Base R Base R
11 fvex Base R V
12 3 8 4 pwselbasb R CRing Base R V F Base R 𝑠 Base R F : Base R Base R
13 6 11 12 sylancl F Q G Q F Base R 𝑠 Base R F : Base R Base R
14 10 13 mpbird F Q G Q F Base R 𝑠 Base R
15 1 8 pf1f G Q G : Base R Base R
16 15 adantl F Q G Q G : Base R Base R
17 3 8 4 pwselbasb R CRing Base R V G Base R 𝑠 Base R G : Base R Base R
18 6 11 17 sylancl F Q G Q G Base R 𝑠 Base R G : Base R Base R
19 16 18 mpbird F Q G Q G Base R 𝑠 Base R
20 eqid R 𝑠 Base R = R 𝑠 Base R
21 3 4 6 7 14 19 2 20 pwsmulrval F Q G Q F R 𝑠 Base R G = F · ˙ f G
22 8 1 pf1subrg R CRing Q SubRing R 𝑠 Base R
23 6 22 syl F Q G Q Q SubRing R 𝑠 Base R
24 20 subrgmcl Q SubRing R 𝑠 Base R F Q G Q F R 𝑠 Base R G Q
25 24 3expib Q SubRing R 𝑠 Base R F Q G Q F R 𝑠 Base R G Q
26 23 25 mpcom F Q G Q F R 𝑠 Base R G Q
27 21 26 eqeltrrd F Q G Q F · ˙ f G Q