Metamath Proof Explorer


Theorem mzpcl34

Description: Defining properties 3 and 4 of a polynomially closed function set P : it is closed under pointwise addition and multiplication. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion mzpcl34 P mzPolyCld V F P G P F + f G P F × f G P

Proof

Step Hyp Ref Expression
1 simp2 P mzPolyCld V F P G P F P
2 simp3 P mzPolyCld V F P G P G P
3 simp1 P mzPolyCld V F P G P P mzPolyCld V
4 3 elfvexd P mzPolyCld V F P G P V V
5 elmzpcl V V P mzPolyCld V P V f V × f P f V g V g f P f P g P f + f g P f × f g P
6 4 5 syl P mzPolyCld V F P G P P mzPolyCld V P V f V × f P f V g V g f P f P g P f + f g P f × f g P
7 3 6 mpbid P mzPolyCld V F P G P P V f V × f P f V g V g f P f P g P f + f g P f × f g P
8 7 simprrd P mzPolyCld V F P G P f P g P f + f g P f × f g P
9 oveq1 f = F f + f g = F + f g
10 9 eleq1d f = F f + f g P F + f g P
11 oveq1 f = F f × f g = F × f g
12 11 eleq1d f = F f × f g P F × f g P
13 10 12 anbi12d f = F f + f g P f × f g P F + f g P F × f g P
14 oveq2 g = G F + f g = F + f G
15 14 eleq1d g = G F + f g P F + f G P
16 oveq2 g = G F × f g = F × f G
17 16 eleq1d g = G F × f g P F × f G P
18 15 17 anbi12d g = G F + f g P F × f g P F + f G P F × f G P
19 13 18 rspc2va F P G P f P g P f + f g P f × f g P F + f G P F × f G P
20 1 2 8 19 syl21anc P mzPolyCld V F P G P F + f G P F × f G P