Metamath Proof Explorer

Theorem mzpcl1

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

Ref Expression
Assertion mzpcl1 
|- ( ( P e. ( mzPolyCld ` V ) /\ F e. ZZ ) -> ( ( ZZ ^m V ) X. { F } ) e. P )

Proof

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