Metamath Proof Explorer


Theorem mzpclall

Description: The set of all functions with the signature of a polynomial is a polynomially closed set. This is a lemma to show that the intersection in df-mzp is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion mzpclall V V V mzPolyCld V

Proof

Step Hyp Ref Expression
1 oveq2 v = V v = V
2 1 oveq2d v = V v = V
3 fveq2 v = V mzPolyCld v = mzPolyCld V
4 2 3 eleq12d v = V v mzPolyCld v V mzPolyCld V
5 ssid v v
6 ovex v V
7 zex V
8 6 7 constmap f v × f v
9 8 rgen f v × f v
10 vex v V
11 7 10 elmap g v g : v
12 ffvelrn g : v f v g f
13 11 12 sylanb g v f v g f
14 13 ancoms f v g v g f
15 14 fmpttd f v g v g f : v
16 7 6 elmap g v g f v g v g f : v
17 15 16 sylibr f v g v g f v
18 17 rgen f v g v g f v
19 9 18 pm3.2i f v × f v f v g v g f v
20 zaddcl a b a + b
21 20 adantl f : v g : v a b a + b
22 simpl f : v g : v f : v
23 simpr f : v g : v g : v
24 ovexd f : v g : v v V
25 inidm v v = v
26 21 22 23 24 24 25 off f : v g : v f + f g : v
27 zmulcl a b a b
28 27 adantl f : v g : v a b a b
29 28 22 23 24 24 25 off f : v g : v f × f g : v
30 26 29 jca f : v g : v f + f g : v f × f g : v
31 7 6 elmap f v f : v
32 7 6 elmap g v g : v
33 31 32 anbi12i f v g v f : v g : v
34 7 6 elmap f + f g v f + f g : v
35 7 6 elmap f × f g v f × f g : v
36 34 35 anbi12i f + f g v f × f g v f + f g : v f × f g : v
37 30 33 36 3imtr4i f v g v f + f g v f × f g v
38 37 rgen2 f v g v f + f g v f × f g v
39 19 38 pm3.2i f v × f v f v g v g f v f v g v f + f g v f × f g v
40 elmzpcl v V v mzPolyCld v v v f v × f v f v g v g f v f v g v f + f g v f × f g v
41 10 40 ax-mp v mzPolyCld v v v f v × f v f v g v g f v f v g v f + f g v f × f g v
42 5 39 41 mpbir2an v mzPolyCld v
43 4 42 vtoclg V V V mzPolyCld V