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 ffvelrnd
 |-  ( ( ( ( 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 )