Metamath Proof Explorer

Theorem mzpcl2

Description: Defining property 2 of a polynomially closed function set P : it contains all projections. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion mzpcl2 
|- ( ( P e. ( mzPolyCld ` V ) /\ F e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` F ) ) e. P )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. V ) -> F e. V )
2 simpl 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. V ) -> P e. ( mzPolyCld ` V ) )
3 elfvex 
 |-  ( P e. ( mzPolyCld ` V ) -> V e. _V )
4 3 adantr 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. V ) -> 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. 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 ) ) ) ) )
7 2 6 mpbid 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. 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 ) ) ) )
8 simprlr 
 |-  ( ( 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 ) ) ) -> A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. P )
9 7 8 syl 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. V ) -> A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. P )
10 fveq2 
 |-  ( f = F -> ( g ` f ) = ( g ` F ) )
11 10 mpteq2dv 
 |-  ( f = F -> ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) = ( g e. ( ZZ ^m V ) |-> ( g ` F ) ) )
12 11 eleq1d 
 |-  ( f = F -> ( ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. P <-> ( g e. ( ZZ ^m V ) |-> ( g ` F ) ) e. P ) )
13 12 rspcva 
 |-  ( ( F e. V /\ A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. P ) -> ( g e. ( ZZ ^m V ) |-> ( g ` F ) ) e. P )
14 1 9 13 syl2anc 
 |-  ( ( P e. ( mzPolyCld ` V ) /\ F e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` F ) ) e. P )