Metamath Proof Explorer

Theorem mzpincl

Description: Polynomial closedness is a universal first-order property and passes to intersections. This is where the closure properties of the polynomial ring itself are proved. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion mzpincl 
|- ( V e. _V -> ( mzPoly ` V ) e. ( mzPolyCld ` V ) )

Proof

Step Hyp Ref Expression
1 mzpval 
 |-  ( V e. _V -> ( mzPoly ` V ) = |^| ( mzPolyCld ` V ) )
2 mzpclall 
 |-  ( V e. _V -> ( ZZ ^m ( ZZ ^m V ) ) e. ( mzPolyCld ` V ) )
3 intss1 
 |-  ( ( ZZ ^m ( ZZ ^m V ) ) e. ( mzPolyCld ` V ) -> |^| ( mzPolyCld ` V ) C_ ( ZZ ^m ( ZZ ^m V ) ) )
4 2 3 syl 
 |-  ( V e. _V -> |^| ( mzPolyCld ` V ) C_ ( ZZ ^m ( ZZ ^m V ) ) )
5 simpr 
 |-  ( ( ( V e. _V /\ f e. ZZ ) /\ a e. ( mzPolyCld ` V ) ) -> a e. ( mzPolyCld ` V ) )
6 simplr 
 |-  ( ( ( V e. _V /\ f e. ZZ ) /\ a e. ( mzPolyCld ` V ) ) -> f e. ZZ )
7 mzpcl1 
 |-  ( ( a e. ( mzPolyCld ` V ) /\ f e. ZZ ) -> ( ( ZZ ^m V ) X. { f } ) e. a )
8 5 6 7 syl2anc 
 |-  ( ( ( V e. _V /\ f e. ZZ ) /\ a e. ( mzPolyCld ` V ) ) -> ( ( ZZ ^m V ) X. { f } ) e. a )
9 8 ralrimiva 
 |-  ( ( V e. _V /\ f e. ZZ ) -> A. a e. ( mzPolyCld ` V ) ( ( ZZ ^m V ) X. { f } ) e. a )
10 ovex 
 |-  ( ZZ ^m V ) e. _V
11 snex 
 |-  { f } e. _V
12 10 11 xpex 
 |-  ( ( ZZ ^m V ) X. { f } ) e. _V
13 12 elint2 
 |-  ( ( ( ZZ ^m V ) X. { f } ) e. |^| ( mzPolyCld ` V ) <-> A. a e. ( mzPolyCld ` V ) ( ( ZZ ^m V ) X. { f } ) e. a )
14 9 13 sylibr 
 |-  ( ( V e. _V /\ f e. ZZ ) -> ( ( ZZ ^m V ) X. { f } ) e. |^| ( mzPolyCld ` V ) )
15 14 ralrimiva 
 |-  ( V e. _V -> A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. |^| ( mzPolyCld ` V ) )
16 simpr 
 |-  ( ( ( V e. _V /\ f e. V ) /\ a e. ( mzPolyCld ` V ) ) -> a e. ( mzPolyCld ` V ) )
17 simplr 
 |-  ( ( ( V e. _V /\ f e. V ) /\ a e. ( mzPolyCld ` V ) ) -> f e. V )
18 mzpcl2 
 |-  ( ( a e. ( mzPolyCld ` V ) /\ f e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. a )
19 16 17 18 syl2anc 
 |-  ( ( ( V e. _V /\ f e. V ) /\ a e. ( mzPolyCld ` V ) ) -> ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. a )
20 19 ralrimiva 
 |-  ( ( V e. _V /\ f e. V ) -> A. a e. ( mzPolyCld ` V ) ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. a )
21 10 mptex 
 |-  ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. _V
22 21 elint2 
 |-  ( ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. |^| ( mzPolyCld ` V ) <-> A. a e. ( mzPolyCld ` V ) ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. a )
23 20 22 sylibr 
 |-  ( ( V e. _V /\ f e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. |^| ( mzPolyCld ` V ) )
24 23 ralrimiva 
 |-  ( V e. _V -> A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. |^| ( mzPolyCld ` V ) )
25 15 24 jca 
 |-  ( V e. _V -> ( A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. |^| ( mzPolyCld ` V ) /\ A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. |^| ( mzPolyCld ` V ) ) )
26 vex 
 |-  f e. _V
27 26 elint2 
 |-  ( f e. |^| ( mzPolyCld ` V ) <-> A. a e. ( mzPolyCld ` V ) f e. a )
28 vex 
 |-  g e. _V
29 28 elint2 
 |-  ( g e. |^| ( mzPolyCld ` V ) <-> A. a e. ( mzPolyCld ` V ) g e. a )
30 mzpcl34 
 |-  ( ( a e. ( mzPolyCld ` V ) /\ f e. a /\ g e. a ) -> ( ( f oF + g ) e. a /\ ( f oF x. g ) e. a ) )
31 30 3expib 
 |-  ( a e. ( mzPolyCld ` V ) -> ( ( f e. a /\ g e. a ) -> ( ( f oF + g ) e. a /\ ( f oF x. g ) e. a ) ) )
32 31 ralimia 
 |-  ( A. a e. ( mzPolyCld ` V ) ( f e. a /\ g e. a ) -> A. a e. ( mzPolyCld ` V ) ( ( f oF + g ) e. a /\ ( f oF x. g ) e. a ) )
33 r19.26 
 |-  ( A. a e. ( mzPolyCld ` V ) ( f e. a /\ g e. a ) <-> ( A. a e. ( mzPolyCld ` V ) f e. a /\ A. a e. ( mzPolyCld ` V ) g e. a ) )
34 r19.26 
 |-  ( A. a e. ( mzPolyCld ` V ) ( ( f oF + g ) e. a /\ ( f oF x. g ) e. a ) <-> ( A. a e. ( mzPolyCld ` V ) ( f oF + g ) e. a /\ A. a e. ( mzPolyCld ` V ) ( f oF x. g ) e. a ) )
35 32 33 34 3imtr3i 
 |-  ( ( A. a e. ( mzPolyCld ` V ) f e. a /\ A. a e. ( mzPolyCld ` V ) g e. a ) -> ( A. a e. ( mzPolyCld ` V ) ( f oF + g ) e. a /\ A. a e. ( mzPolyCld ` V ) ( f oF x. g ) e. a ) )
36 27 29 35 syl2anb 
 |-  ( ( f e. |^| ( mzPolyCld ` V ) /\ g e. |^| ( mzPolyCld ` V ) ) -> ( A. a e. ( mzPolyCld ` V ) ( f oF + g ) e. a /\ A. a e. ( mzPolyCld ` V ) ( f oF x. g ) e. a ) )
37 ovex 
 |-  ( f oF + g ) e. _V
38 37 elint2 
 |-  ( ( f oF + g ) e. |^| ( mzPolyCld ` V ) <-> A. a e. ( mzPolyCld ` V ) ( f oF + g ) e. a )
39 ovex 
 |-  ( f oF x. g ) e. _V
40 39 elint2 
 |-  ( ( f oF x. g ) e. |^| ( mzPolyCld ` V ) <-> A. a e. ( mzPolyCld ` V ) ( f oF x. g ) e. a )
41 38 40 anbi12i 
 |-  ( ( ( f oF + g ) e. |^| ( mzPolyCld ` V ) /\ ( f oF x. g ) e. |^| ( mzPolyCld ` V ) ) <-> ( A. a e. ( mzPolyCld ` V ) ( f oF + g ) e. a /\ A. a e. ( mzPolyCld ` V ) ( f oF x. g ) e. a ) )
42 36 41 sylibr 
 |-  ( ( f e. |^| ( mzPolyCld ` V ) /\ g e. |^| ( mzPolyCld ` V ) ) -> ( ( f oF + g ) e. |^| ( mzPolyCld ` V ) /\ ( f oF x. g ) e. |^| ( mzPolyCld ` V ) ) )
43 42 a1i 
 |-  ( V e. _V -> ( ( f e. |^| ( mzPolyCld ` V ) /\ g e. |^| ( mzPolyCld ` V ) ) -> ( ( f oF + g ) e. |^| ( mzPolyCld ` V ) /\ ( f oF x. g ) e. |^| ( mzPolyCld ` V ) ) ) )
44 43 ralrimivv 
 |-  ( V e. _V -> A. f e. |^| ( mzPolyCld ` V ) A. g e. |^| ( mzPolyCld ` V ) ( ( f oF + g ) e. |^| ( mzPolyCld ` V ) /\ ( f oF x. g ) e. |^| ( mzPolyCld ` V ) ) )
45 4 25 44 jca32 
 |-  ( V e. _V -> ( |^| ( mzPolyCld ` V ) C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. |^| ( mzPolyCld ` V ) /\ A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. |^| ( mzPolyCld ` V ) ) /\ A. f e. |^| ( mzPolyCld ` V ) A. g e. |^| ( mzPolyCld ` V ) ( ( f oF + g ) e. |^| ( mzPolyCld ` V ) /\ ( f oF x. g ) e. |^| ( mzPolyCld ` V ) ) ) ) )
46 elmzpcl 
 |-  ( V e. _V -> ( |^| ( mzPolyCld ` V ) e. ( mzPolyCld ` V ) <-> ( |^| ( mzPolyCld ` V ) C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. |^| ( mzPolyCld ` V ) /\ A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. |^| ( mzPolyCld ` V ) ) /\ A. f e. |^| ( mzPolyCld ` V ) A. g e. |^| ( mzPolyCld ` V ) ( ( f oF + g ) e. |^| ( mzPolyCld ` V ) /\ ( f oF x. g ) e. |^| ( mzPolyCld ` V ) ) ) ) ) )
47 45 46 mpbird 
 |-  ( V e. _V -> |^| ( mzPolyCld ` V ) e. ( mzPolyCld ` V ) )
48 1 47 eqeltrd 
 |-  ( V e. _V -> ( mzPoly ` V ) e. ( mzPolyCld ` V ) )