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