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 ( ( ๐‘ƒ โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) โˆง ๐น โˆˆ ๐‘‰ ) โ†’ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐น ) ) โˆˆ ๐‘ƒ )

Proof

Step Hyp Ref Expression
1 simpr โŠข ( ( ๐‘ƒ โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) โˆง ๐น โˆˆ ๐‘‰ ) โ†’ ๐น โˆˆ ๐‘‰ )
2 simpl โŠข ( ( ๐‘ƒ โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) โˆง ๐น โˆˆ ๐‘‰ ) โ†’ ๐‘ƒ โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) )
3 elfvex โŠข ( ๐‘ƒ โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) โ†’ ๐‘‰ โˆˆ V )
4 3 adantr โŠข ( ( ๐‘ƒ โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) โˆง ๐น โˆˆ ๐‘‰ ) โ†’ ๐‘‰ โˆˆ V )
5 elmzpcl โŠข ( ๐‘‰ โˆˆ V โ†’ ( ๐‘ƒ โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) โ†” ( ๐‘ƒ โŠ† ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘‰ ) ) โˆง ( ( โˆ€ ๐‘“ โˆˆ โ„ค ( ( โ„ค โ†‘m ๐‘‰ ) ร— { ๐‘“ } ) โˆˆ ๐‘ƒ โˆง โˆ€ ๐‘“ โˆˆ ๐‘‰ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ๐‘ƒ ) โˆง โˆ€ ๐‘“ โˆˆ ๐‘ƒ โˆ€ ๐‘” โˆˆ ๐‘ƒ ( ( ๐‘“ โˆ˜f + ๐‘” ) โˆˆ ๐‘ƒ โˆง ( ๐‘“ โˆ˜f ยท ๐‘” ) โˆˆ ๐‘ƒ ) ) ) ) )
6 4 5 syl โŠข ( ( ๐‘ƒ โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) โˆง ๐น โˆˆ ๐‘‰ ) โ†’ ( ๐‘ƒ โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) โ†” ( ๐‘ƒ โŠ† ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘‰ ) ) โˆง ( ( โˆ€ ๐‘“ โˆˆ โ„ค ( ( โ„ค โ†‘m ๐‘‰ ) ร— { ๐‘“ } ) โˆˆ ๐‘ƒ โˆง โˆ€ ๐‘“ โˆˆ ๐‘‰ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ๐‘ƒ ) โˆง โˆ€ ๐‘“ โˆˆ ๐‘ƒ โˆ€ ๐‘” โˆˆ ๐‘ƒ ( ( ๐‘“ โˆ˜f + ๐‘” ) โˆˆ ๐‘ƒ โˆง ( ๐‘“ โˆ˜f ยท ๐‘” ) โˆˆ ๐‘ƒ ) ) ) ) )
7 2 6 mpbid โŠข ( ( ๐‘ƒ โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) โˆง ๐น โˆˆ ๐‘‰ ) โ†’ ( ๐‘ƒ โŠ† ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘‰ ) ) โˆง ( ( โˆ€ ๐‘“ โˆˆ โ„ค ( ( โ„ค โ†‘m ๐‘‰ ) ร— { ๐‘“ } ) โˆˆ ๐‘ƒ โˆง โˆ€ ๐‘“ โˆˆ ๐‘‰ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ๐‘ƒ ) โˆง โˆ€ ๐‘“ โˆˆ ๐‘ƒ โˆ€ ๐‘” โˆˆ ๐‘ƒ ( ( ๐‘“ โˆ˜f + ๐‘” ) โˆˆ ๐‘ƒ โˆง ( ๐‘“ โˆ˜f ยท ๐‘” ) โˆˆ ๐‘ƒ ) ) ) )
8 simprlr โŠข ( ( ๐‘ƒ โŠ† ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘‰ ) ) โˆง ( ( โˆ€ ๐‘“ โˆˆ โ„ค ( ( โ„ค โ†‘m ๐‘‰ ) ร— { ๐‘“ } ) โˆˆ ๐‘ƒ โˆง โˆ€ ๐‘“ โˆˆ ๐‘‰ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ๐‘ƒ ) โˆง โˆ€ ๐‘“ โˆˆ ๐‘ƒ โˆ€ ๐‘” โˆˆ ๐‘ƒ ( ( ๐‘“ โˆ˜f + ๐‘” ) โˆˆ ๐‘ƒ โˆง ( ๐‘“ โˆ˜f ยท ๐‘” ) โˆˆ ๐‘ƒ ) ) ) โ†’ โˆ€ ๐‘“ โˆˆ ๐‘‰ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ๐‘ƒ )
9 7 8 syl โŠข ( ( ๐‘ƒ โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) โˆง ๐น โˆˆ ๐‘‰ ) โ†’ โˆ€ ๐‘“ โˆˆ ๐‘‰ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ๐‘ƒ )
10 fveq2 โŠข ( ๐‘“ = ๐น โ†’ ( ๐‘” โ€˜ ๐‘“ ) = ( ๐‘” โ€˜ ๐น ) )
11 10 mpteq2dv โŠข ( ๐‘“ = ๐น โ†’ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) = ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐น ) ) )
12 11 eleq1d โŠข ( ๐‘“ = ๐น โ†’ ( ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ๐‘ƒ โ†” ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐น ) ) โˆˆ ๐‘ƒ ) )
13 12 rspcva โŠข ( ( ๐น โˆˆ ๐‘‰ โˆง โˆ€ ๐‘“ โˆˆ ๐‘‰ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ๐‘ƒ ) โ†’ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐น ) ) โˆˆ ๐‘ƒ )
14 1 9 13 syl2anc โŠข ( ( ๐‘ƒ โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) โˆง ๐น โˆˆ ๐‘‰ ) โ†’ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘‰ ) โ†ฆ ( ๐‘” โ€˜ ๐น ) ) โˆˆ ๐‘ƒ )