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 e. ( mzPolyCld ` V ) /\ F e. P /\ G e. P ) -> ( ( F oF + G ) e. P /\ ( F oF x. G ) e. P ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. P /\ G e. P ) -> F e. P )
2 simp3 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. P /\ G e. P ) -> G e. P )
3 simp1 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. P /\ G e. P ) -> P e. ( mzPolyCld ` V ) )
4 3 elfvexd 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. P /\ G e. P ) -> V e. _V )
5 elmzpcl 
 |-  ( V e. _V -> ( P e. ( mzPolyCld ` V ) <-> ( P C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. P /\ A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) ) ) )
6 4 5 syl 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. P /\ G e. P ) -> ( P e. ( mzPolyCld ` V ) <-> ( P C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. P /\ A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) ) ) )
7 3 6 mpbid 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. P /\ G e. P ) -> ( P C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. P /\ A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) ) )
8 7 simprrd 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. P /\ G e. P ) -> A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) )
9 oveq1 
 |-  ( f = F -> ( f oF + g ) = ( F oF + g ) )
10 9 eleq1d 
 |-  ( f = F -> ( ( f oF + g ) e. P <-> ( F oF + g ) e. P ) )
11 oveq1 
 |-  ( f = F -> ( f oF x. g ) = ( F oF x. g ) )
12 11 eleq1d 
 |-  ( f = F -> ( ( f oF x. g ) e. P <-> ( F oF x. g ) e. P ) )
13 10 12 anbi12d 
 |-  ( f = F -> ( ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) <-> ( ( F oF + g ) e. P /\ ( F oF x. g ) e. P ) ) )
14 oveq2 
 |-  ( g = G -> ( F oF + g ) = ( F oF + G ) )
15 14 eleq1d 
 |-  ( g = G -> ( ( F oF + g ) e. P <-> ( F oF + G ) e. P ) )
16 oveq2 
 |-  ( g = G -> ( F oF x. g ) = ( F oF x. G ) )
17 16 eleq1d 
 |-  ( g = G -> ( ( F oF x. g ) e. P <-> ( F oF x. G ) e. P ) )
18 15 17 anbi12d 
 |-  ( g = G -> ( ( ( F oF + g ) e. P /\ ( F oF x. g ) e. P ) <-> ( ( F oF + G ) e. P /\ ( F oF x. G ) e. P ) ) )
19 13 18 rspc2va 
 |-  ( ( ( F e. P /\ G e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) -> ( ( F oF + G ) e. P /\ ( F oF x. G ) e. P ) )
20 1 2 8 19 syl21anc 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. P /\ G e. P ) -> ( ( F oF + G ) e. P /\ ( F oF x. G ) e. P ) )