Metamath Proof Explorer

Theorem mzpindd

Description: "Structural" induction to prove properties of all polynomial functions. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Hypotheses mzpindd.co 
|- ( ( ph /\ f e. ZZ ) -> ch )
mzpindd.pr 
|- ( ( ph /\ f e. V ) -> th )
mzpindd.ad 
|- ( ( ph /\ ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> ze )
mzpindd.mu 
|- ( ( ph /\ ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> si )
mzpindd.1 
|- ( x = ( ( ZZ ^m V ) X. { f } ) -> ( ps <-> ch ) )
mzpindd.2 
|- ( x = ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) -> ( ps <-> th ) )
mzpindd.3 
|- ( x = f -> ( ps <-> ta ) )
mzpindd.4 
|- ( x = g -> ( ps <-> et ) )
mzpindd.5 
|- ( x = ( f oF + g ) -> ( ps <-> ze ) )
mzpindd.6 
|- ( x = ( f oF x. g ) -> ( ps <-> si ) )
mzpindd.7 
|- ( x = A -> ( ps <-> rh ) )
Assertion mzpindd 
|- ( ( ph /\ A e. ( mzPoly ` V ) ) -> rh )

Proof

Step Hyp Ref Expression
1 mzpindd.co 
 |-  ( ( ph /\ f e. ZZ ) -> ch )
2 mzpindd.pr 
 |-  ( ( ph /\ f e. V ) -> th )
3 mzpindd.ad 
 |-  ( ( ph /\ ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> ze )
4 mzpindd.mu 
 |-  ( ( ph /\ ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> si )
5 mzpindd.1 
 |-  ( x = ( ( ZZ ^m V ) X. { f } ) -> ( ps <-> ch ) )
6 mzpindd.2 
 |-  ( x = ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) -> ( ps <-> th ) )
7 mzpindd.3 
 |-  ( x = f -> ( ps <-> ta ) )
8 mzpindd.4 
 |-  ( x = g -> ( ps <-> et ) )
9 mzpindd.5 
 |-  ( x = ( f oF + g ) -> ( ps <-> ze ) )
10 mzpindd.6 
 |-  ( x = ( f oF x. g ) -> ( ps <-> si ) )
11 mzpindd.7 
 |-  ( x = A -> ( ps <-> rh ) )
12 elfvex 
 |-  ( A e. ( mzPoly ` V ) -> V e. _V )
13 12 adantl 
 |-  ( ( ph /\ A e. ( mzPoly ` V ) ) -> V e. _V )
14 mzpval 
 |-  ( V e. _V -> ( mzPoly ` V ) = |^| ( mzPolyCld ` V ) )
15 14 adantl 
 |-  ( ( ph /\ V e. _V ) -> ( mzPoly ` V ) = |^| ( mzPolyCld ` V ) )
16 ssrab2 
 |-  { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } C_ ( ZZ ^m ( ZZ ^m V ) )
17 16 a1i 
 |-  ( ( ph /\ V e. _V ) -> { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } C_ ( ZZ ^m ( ZZ ^m V ) ) )
18 ovex 
 |-  ( ZZ ^m V ) e. _V
19 zex 
 |-  ZZ e. _V
20 18 19 constmap 
 |-  ( f e. ZZ -> ( ( ZZ ^m V ) X. { f } ) e. ( ZZ ^m ( ZZ ^m V ) ) )
21 20 adantl 
 |-  ( ( ph /\ f e. ZZ ) -> ( ( ZZ ^m V ) X. { f } ) e. ( ZZ ^m ( ZZ ^m V ) ) )
22 5 elrab 
 |-  ( ( ( ZZ ^m V ) X. { f } ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } <-> ( ( ( ZZ ^m V ) X. { f } ) e. ( ZZ ^m ( ZZ ^m V ) ) /\ ch ) )
23 21 1 22 sylanbrc 
 |-  ( ( ph /\ f e. ZZ ) -> ( ( ZZ ^m V ) X. { f } ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } )
24 23 ralrimiva 
 |-  ( ph -> A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } )
25 24 adantr 
 |-  ( ( ph /\ V e. _V ) -> A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } )
26 19 a1i 
 |-  ( ( ( ( ph /\ V e. _V ) /\ f e. V ) /\ g e. ( ZZ ^m V ) ) -> ZZ e. _V )
27 simpllr 
 |-  ( ( ( ( ph /\ V e. _V ) /\ f e. V ) /\ g e. ( ZZ ^m V ) ) -> V e. _V )
28 simpr 
 |-  ( ( ( ( ph /\ V e. _V ) /\ f e. V ) /\ g e. ( ZZ ^m V ) ) -> g e. ( ZZ ^m V ) )
29 elmapg 
 |-  ( ( ZZ e. _V /\ V e. _V ) -> ( g e. ( ZZ ^m V ) <-> g : V --> ZZ ) )
30 29 biimpa 
 |-  ( ( ( ZZ e. _V /\ V e. _V ) /\ g e. ( ZZ ^m V ) ) -> g : V --> ZZ )
31 26 27 28 30 syl21anc 
 |-  ( ( ( ( ph /\ V e. _V ) /\ f e. V ) /\ g e. ( ZZ ^m V ) ) -> g : V --> ZZ )
32 simplr 
 |-  ( ( ( ( ph /\ V e. _V ) /\ f e. V ) /\ g e. ( ZZ ^m V ) ) -> f e. V )
33 31 32 ffvelcdmd 
 |-  ( ( ( ( ph /\ V e. _V ) /\ f e. V ) /\ g e. ( ZZ ^m V ) ) -> ( g ` f ) e. ZZ )
34 33 fmpttd 
 |-  ( ( ( ph /\ V e. _V ) /\ f e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) : ( ZZ ^m V ) --> ZZ )
35 19 18 elmap 
 |-  ( ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. ( ZZ ^m ( ZZ ^m V ) ) <-> ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) : ( ZZ ^m V ) --> ZZ )
36 34 35 sylibr 
 |-  ( ( ( ph /\ V e. _V ) /\ f e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. ( ZZ ^m ( ZZ ^m V ) ) )
37 2 adantlr 
 |-  ( ( ( ph /\ V e. _V ) /\ f e. V ) -> th )
38 6 elrab 
 |-  ( ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } <-> ( ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. ( ZZ ^m ( ZZ ^m V ) ) /\ th ) )
39 36 37 38 sylanbrc 
 |-  ( ( ( ph /\ V e. _V ) /\ f e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } )
40 39 ralrimiva 
 |-  ( ( ph /\ V e. _V ) -> A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } )
41 25 40 jca 
 |-  ( ( ph /\ V e. _V ) -> ( A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) )
42 zaddcl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a + b ) e. ZZ )
43 42 adantl 
 |-  ( ( ( f : ( ZZ ^m V ) --> ZZ /\ g : ( ZZ ^m V ) --> ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a + b ) e. ZZ )
44 simpl 
 |-  ( ( f : ( ZZ ^m V ) --> ZZ /\ g : ( ZZ ^m V ) --> ZZ ) -> f : ( ZZ ^m V ) --> ZZ )
45 simpr 
 |-  ( ( f : ( ZZ ^m V ) --> ZZ /\ g : ( ZZ ^m V ) --> ZZ ) -> g : ( ZZ ^m V ) --> ZZ )
46 18 a1i 
 |-  ( ( f : ( ZZ ^m V ) --> ZZ /\ g : ( ZZ ^m V ) --> ZZ ) -> ( ZZ ^m V ) e. _V )
47 inidm 
 |-  ( ( ZZ ^m V ) i^i ( ZZ ^m V ) ) = ( ZZ ^m V )
48 43 44 45 46 46 47 off 
 |-  ( ( f : ( ZZ ^m V ) --> ZZ /\ g : ( ZZ ^m V ) --> ZZ ) -> ( f oF + g ) : ( ZZ ^m V ) --> ZZ )
49 48 ad2ant2r 
 |-  ( ( ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> ( f oF + g ) : ( ZZ ^m V ) --> ZZ )
50 49 adantl 
 |-  ( ( ph /\ ( ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) ) -> ( f oF + g ) : ( ZZ ^m V ) --> ZZ )
51 3 3expb 
 |-  ( ( ph /\ ( ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) ) -> ze )
52 50 51 jca 
 |-  ( ( ph /\ ( ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) ) -> ( ( f oF + g ) : ( ZZ ^m V ) --> ZZ /\ ze ) )
53 zmulcl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a x. b ) e. ZZ )
54 53 adantl 
 |-  ( ( ( f : ( ZZ ^m V ) --> ZZ /\ g : ( ZZ ^m V ) --> ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a x. b ) e. ZZ )
55 54 44 45 46 46 47 off 
 |-  ( ( f : ( ZZ ^m V ) --> ZZ /\ g : ( ZZ ^m V ) --> ZZ ) -> ( f oF x. g ) : ( ZZ ^m V ) --> ZZ )
56 55 ad2ant2r 
 |-  ( ( ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> ( f oF x. g ) : ( ZZ ^m V ) --> ZZ )
57 56 adantl 
 |-  ( ( ph /\ ( ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) ) -> ( f oF x. g ) : ( ZZ ^m V ) --> ZZ )
58 4 3expb 
 |-  ( ( ph /\ ( ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) ) -> si )
59 52 57 58 jca32 
 |-  ( ( ph /\ ( ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) ) -> ( ( ( f oF + g ) : ( ZZ ^m V ) --> ZZ /\ ze ) /\ ( ( f oF x. g ) : ( ZZ ^m V ) --> ZZ /\ si ) ) )
60 59 ex 
 |-  ( ph -> ( ( ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> ( ( ( f oF + g ) : ( ZZ ^m V ) --> ZZ /\ ze ) /\ ( ( f oF x. g ) : ( ZZ ^m V ) --> ZZ /\ si ) ) ) )
61 19 18 elmap 
 |-  ( f e. ( ZZ ^m ( ZZ ^m V ) ) <-> f : ( ZZ ^m V ) --> ZZ )
62 61 anbi1i 
 |-  ( ( f e. ( ZZ ^m ( ZZ ^m V ) ) /\ ta ) <-> ( f : ( ZZ ^m V ) --> ZZ /\ ta ) )
63 19 18 elmap 
 |-  ( g e. ( ZZ ^m ( ZZ ^m V ) ) <-> g : ( ZZ ^m V ) --> ZZ )
64 63 anbi1i 
 |-  ( ( g e. ( ZZ ^m ( ZZ ^m V ) ) /\ et ) <-> ( g : ( ZZ ^m V ) --> ZZ /\ et ) )
65 62 64 anbi12i 
 |-  ( ( ( f e. ( ZZ ^m ( ZZ ^m V ) ) /\ ta ) /\ ( g e. ( ZZ ^m ( ZZ ^m V ) ) /\ et ) ) <-> ( ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) )
66 19 18 elmap 
 |-  ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m V ) ) <-> ( f oF + g ) : ( ZZ ^m V ) --> ZZ )
67 66 anbi1i 
 |-  ( ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m V ) ) /\ ze ) <-> ( ( f oF + g ) : ( ZZ ^m V ) --> ZZ /\ ze ) )
68 19 18 elmap 
 |-  ( ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m V ) ) <-> ( f oF x. g ) : ( ZZ ^m V ) --> ZZ )
69 68 anbi1i 
 |-  ( ( ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m V ) ) /\ si ) <-> ( ( f oF x. g ) : ( ZZ ^m V ) --> ZZ /\ si ) )
70 67 69 anbi12i 
 |-  ( ( ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m V ) ) /\ ze ) /\ ( ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m V ) ) /\ si ) ) <-> ( ( ( f oF + g ) : ( ZZ ^m V ) --> ZZ /\ ze ) /\ ( ( f oF x. g ) : ( ZZ ^m V ) --> ZZ /\ si ) ) )
71 60 65 70 3imtr4g 
 |-  ( ph -> ( ( ( f e. ( ZZ ^m ( ZZ ^m V ) ) /\ ta ) /\ ( g e. ( ZZ ^m ( ZZ ^m V ) ) /\ et ) ) -> ( ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m V ) ) /\ ze ) /\ ( ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m V ) ) /\ si ) ) ) )
72 7 elrab 
 |-  ( f e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } <-> ( f e. ( ZZ ^m ( ZZ ^m V ) ) /\ ta ) )
73 8 elrab 
 |-  ( g e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } <-> ( g e. ( ZZ ^m ( ZZ ^m V ) ) /\ et ) )
74 72 73 anbi12i 
 |-  ( ( f e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ g e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) <-> ( ( f e. ( ZZ ^m ( ZZ ^m V ) ) /\ ta ) /\ ( g e. ( ZZ ^m ( ZZ ^m V ) ) /\ et ) ) )
75 9 elrab 
 |-  ( ( f oF + g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } <-> ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m V ) ) /\ ze ) )
76 10 elrab 
 |-  ( ( f oF x. g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } <-> ( ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m V ) ) /\ si ) )
77 75 76 anbi12i 
 |-  ( ( ( f oF + g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ ( f oF x. g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) <-> ( ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m V ) ) /\ ze ) /\ ( ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m V ) ) /\ si ) ) )
78 71 74 77 3imtr4g 
 |-  ( ph -> ( ( f e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ g e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) -> ( ( f oF + g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ ( f oF x. g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) ) )
79 78 ralrimivv 
 |-  ( ph -> A. f e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } A. g e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ( ( f oF + g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ ( f oF x. g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) )
80 79 adantr 
 |-  ( ( ph /\ V e. _V ) -> A. f e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } A. g e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ( ( f oF + g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ ( f oF x. g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) )
81 17 41 80 jca32 
 |-  ( ( ph /\ V e. _V ) -> ( { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) /\ A. f e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } A. g e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ( ( f oF + g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ ( f oF x. g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) ) ) )
82 elmzpcl 
 |-  ( V e. _V -> ( { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } e. ( mzPolyCld ` V ) <-> ( { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) /\ A. f e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } A. g e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ( ( f oF + g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ ( f oF x. g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) ) ) ) )
83 82 adantl 
 |-  ( ( ph /\ V e. _V ) -> ( { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } e. ( mzPolyCld ` V ) <-> ( { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. f e. ZZ ( ( ZZ ^m V ) X. { f } ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ A. f e. V ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) /\ A. f e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } A. g e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ( ( f oF + g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } /\ ( f oF x. g ) e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } ) ) ) ) )
84 81 83 mpbird 
 |-  ( ( ph /\ V e. _V ) -> { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } e. ( mzPolyCld ` V ) )
85 intss1 
 |-  ( { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } e. ( mzPolyCld ` V ) -> |^| ( mzPolyCld ` V ) C_ { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } )
86 84 85 syl 
 |-  ( ( ph /\ V e. _V ) -> |^| ( mzPolyCld ` V ) C_ { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } )
87 15 86 eqsstrd 
 |-  ( ( ph /\ V e. _V ) -> ( mzPoly ` V ) C_ { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } )
88 87 sselda 
 |-  ( ( ( ph /\ V e. _V ) /\ A e. ( mzPoly ` V ) ) -> A e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } )
89 88 an32s 
 |-  ( ( ( ph /\ A e. ( mzPoly ` V ) ) /\ V e. _V ) -> A e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } )
90 13 89 mpdan 
 |-  ( ( ph /\ A e. ( mzPoly ` V ) ) -> A e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } )
91 11 elrab 
 |-  ( A e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } <-> ( A e. ( ZZ ^m ( ZZ ^m V ) ) /\ rh ) )
92 91 simprbi 
 |-  ( A e. { x e. ( ZZ ^m ( ZZ ^m V ) ) | ps } -> rh )
93 90 92 syl 
 |-  ( ( ph /\ A e. ( mzPoly ` V ) ) -> rh )