Metamath Proof Explorer

Theorem mzpclall

Description: The set of all functions with the signature of a polynomial is a polynomially closed set. This is a lemma to show that the intersection in df-mzp is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion mzpclall ( ๐‘‰ โˆˆ V โ†’ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘‰ ) ) โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) )

Proof

Step Hyp Ref Expression
1 oveq2 โŠข ( ๐‘ฃ = ๐‘‰ โ†’ ( โ„ค โ†‘m ๐‘ฃ ) = ( โ„ค โ†‘m ๐‘‰ ) )
2 1 oveq2d โŠข ( ๐‘ฃ = ๐‘‰ โ†’ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) = ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘‰ ) ) )
3 fveq2 โŠข ( ๐‘ฃ = ๐‘‰ โ†’ ( mzPolyCld โ€˜ ๐‘ฃ ) = ( mzPolyCld โ€˜ ๐‘‰ ) )
4 2 3 eleq12d โŠข ( ๐‘ฃ = ๐‘‰ โ†’ ( ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆˆ ( mzPolyCld โ€˜ ๐‘ฃ ) โ†” ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘‰ ) ) โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) ) )
5 ssid โŠข ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โŠ† ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) )
6 ovex โŠข ( โ„ค โ†‘m ๐‘ฃ ) โˆˆ V
7 zex โŠข โ„ค โˆˆ V
8 6 7 constmap โŠข ( ๐‘“ โˆˆ โ„ค โ†’ ( ( โ„ค โ†‘m ๐‘ฃ ) ร— { ๐‘“ } ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) )
9 8 rgen โŠข โˆ€ ๐‘“ โˆˆ โ„ค ( ( โ„ค โ†‘m ๐‘ฃ ) ร— { ๐‘“ } ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) )
10 vex โŠข ๐‘ฃ โˆˆ V
11 7 10 elmap โŠข ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘ฃ ) โ†” ๐‘” : ๐‘ฃ โŸถ โ„ค )
12 ffvelcdm โŠข ( ( ๐‘” : ๐‘ฃ โŸถ โ„ค โˆง ๐‘“ โˆˆ ๐‘ฃ ) โ†’ ( ๐‘” โ€˜ ๐‘“ ) โˆˆ โ„ค )
13 11 12 sylanb โŠข ( ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘ฃ ) โˆง ๐‘“ โˆˆ ๐‘ฃ ) โ†’ ( ๐‘” โ€˜ ๐‘“ ) โˆˆ โ„ค )
14 13 ancoms โŠข ( ( ๐‘“ โˆˆ ๐‘ฃ โˆง ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘ฃ ) ) โ†’ ( ๐‘” โ€˜ ๐‘“ ) โˆˆ โ„ค )
15 14 fmpttd โŠข ( ๐‘“ โˆˆ ๐‘ฃ โ†’ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘ฃ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค )
16 7 6 elmap โŠข ( ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘ฃ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โ†” ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘ฃ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค )
17 15 16 sylibr โŠข ( ๐‘“ โˆˆ ๐‘ฃ โ†’ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘ฃ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) )
18 17 rgen โŠข โˆ€ ๐‘“ โˆˆ ๐‘ฃ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘ฃ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) )
19 9 18 pm3.2i โŠข ( โˆ€ ๐‘“ โˆˆ โ„ค ( ( โ„ค โ†‘m ๐‘ฃ ) ร— { ๐‘“ } ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง โˆ€ ๐‘“ โˆˆ ๐‘ฃ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘ฃ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) )
20 zaddcl โŠข ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘Ž + ๐‘ ) โˆˆ โ„ค )
21 20 adantl โŠข ( ( ( ๐‘“ : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค โˆง ๐‘” : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค ) โˆง ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) ) โ†’ ( ๐‘Ž + ๐‘ ) โˆˆ โ„ค )
22 simpl โŠข ( ( ๐‘“ : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค โˆง ๐‘” : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค ) โ†’ ๐‘“ : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค )
23 simpr โŠข ( ( ๐‘“ : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค โˆง ๐‘” : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค ) โ†’ ๐‘” : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค )
24 ovexd โŠข ( ( ๐‘“ : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค โˆง ๐‘” : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค ) โ†’ ( โ„ค โ†‘m ๐‘ฃ ) โˆˆ V )
25 inidm โŠข ( ( โ„ค โ†‘m ๐‘ฃ ) โˆฉ ( โ„ค โ†‘m ๐‘ฃ ) ) = ( โ„ค โ†‘m ๐‘ฃ )
26 21 22 23 24 24 25 off โŠข ( ( ๐‘“ : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค โˆง ๐‘” : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค ) โ†’ ( ๐‘“ โˆ˜f + ๐‘” ) : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค )
27 zmulcl โŠข ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘Ž ยท ๐‘ ) โˆˆ โ„ค )
28 27 adantl โŠข ( ( ( ๐‘“ : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค โˆง ๐‘” : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค ) โˆง ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) ) โ†’ ( ๐‘Ž ยท ๐‘ ) โˆˆ โ„ค )
29 28 22 23 24 24 25 off โŠข ( ( ๐‘“ : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค โˆง ๐‘” : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค ) โ†’ ( ๐‘“ โˆ˜f ยท ๐‘” ) : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค )
30 26 29 jca โŠข ( ( ๐‘“ : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค โˆง ๐‘” : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค ) โ†’ ( ( ๐‘“ โˆ˜f + ๐‘” ) : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค โˆง ( ๐‘“ โˆ˜f ยท ๐‘” ) : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค ) )
31 7 6 elmap โŠข ( ๐‘“ โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โ†” ๐‘“ : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค )
32 7 6 elmap โŠข ( ๐‘” โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โ†” ๐‘” : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค )
33 31 32 anbi12i โŠข ( ( ๐‘“ โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง ๐‘” โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ) โ†” ( ๐‘“ : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค โˆง ๐‘” : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค ) )
34 7 6 elmap โŠข ( ( ๐‘“ โˆ˜f + ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โ†” ( ๐‘“ โˆ˜f + ๐‘” ) : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค )
35 7 6 elmap โŠข ( ( ๐‘“ โˆ˜f ยท ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โ†” ( ๐‘“ โˆ˜f ยท ๐‘” ) : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค )
36 34 35 anbi12i โŠข ( ( ( ๐‘“ โˆ˜f + ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง ( ๐‘“ โˆ˜f ยท ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ) โ†” ( ( ๐‘“ โˆ˜f + ๐‘” ) : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค โˆง ( ๐‘“ โˆ˜f ยท ๐‘” ) : ( โ„ค โ†‘m ๐‘ฃ ) โŸถ โ„ค ) )
37 30 33 36 3imtr4i โŠข ( ( ๐‘“ โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง ๐‘” โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ) โ†’ ( ( ๐‘“ โˆ˜f + ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง ( ๐‘“ โˆ˜f ยท ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ) )
38 37 rgen2 โŠข โˆ€ ๐‘“ โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆ€ ๐‘” โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ( ( ๐‘“ โˆ˜f + ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง ( ๐‘“ โˆ˜f ยท ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) )
39 19 38 pm3.2i โŠข ( ( โˆ€ ๐‘“ โˆˆ โ„ค ( ( โ„ค โ†‘m ๐‘ฃ ) ร— { ๐‘“ } ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง โˆ€ ๐‘“ โˆˆ ๐‘ฃ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘ฃ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ) โˆง โˆ€ ๐‘“ โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆ€ ๐‘” โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ( ( ๐‘“ โˆ˜f + ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง ( ๐‘“ โˆ˜f ยท ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ) )
40 elmzpcl โŠข ( ๐‘ฃ โˆˆ V โ†’ ( ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆˆ ( mzPolyCld โ€˜ ๐‘ฃ ) โ†” ( ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โŠ† ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง ( ( โˆ€ ๐‘“ โˆˆ โ„ค ( ( โ„ค โ†‘m ๐‘ฃ ) ร— { ๐‘“ } ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง โˆ€ ๐‘“ โˆˆ ๐‘ฃ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘ฃ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ) โˆง โˆ€ ๐‘“ โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆ€ ๐‘” โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ( ( ๐‘“ โˆ˜f + ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง ( ๐‘“ โˆ˜f ยท ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ) ) ) ) )
41 10 40 ax-mp โŠข ( ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆˆ ( mzPolyCld โ€˜ ๐‘ฃ ) โ†” ( ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โŠ† ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง ( ( โˆ€ ๐‘“ โˆˆ โ„ค ( ( โ„ค โ†‘m ๐‘ฃ ) ร— { ๐‘“ } ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง โˆ€ ๐‘“ โˆˆ ๐‘ฃ ( ๐‘” โˆˆ ( โ„ค โ†‘m ๐‘ฃ ) โ†ฆ ( ๐‘” โ€˜ ๐‘“ ) ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ) โˆง โˆ€ ๐‘“ โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆ€ ๐‘” โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ( ( ๐‘“ โˆ˜f + ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆง ( ๐‘“ โˆ˜f ยท ๐‘” ) โˆˆ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) ) ) ) )
42 5 39 41 mpbir2an โŠข ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘ฃ ) ) โˆˆ ( mzPolyCld โ€˜ ๐‘ฃ )
43 4 42 vtoclg โŠข ( ๐‘‰ โˆˆ V โ†’ ( โ„ค โ†‘m ( โ„ค โ†‘m ๐‘‰ ) ) โˆˆ ( mzPolyCld โ€˜ ๐‘‰ ) )