Step | Hyp | Ref
| Expression |
1 | | elfvex 6221 |
. . . 4
mzPoly
|
2 | 1 | adantl 482 |
. . 3
mzPoly |
3 | | mzpval 37295 |
. . . . . . 7
mzPoly mzPolyCld |
4 | 3 | adantl 482 |
. . . . . 6
mzPoly mzPolyCld |
5 | | ssrab2 3687 |
. . . . . . . . . 10
|
6 | 5 | a1i 11 |
. . . . . . . . 9
|
7 | | ovex 6678 |
. . . . . . . . . . . . . . 15
|
8 | | zex 11386 |
. . . . . . . . . . . . . . 15
|
9 | 7, 8 | constmap 37276 |
. . . . . . . . . . . . . 14
|
10 | 9 | adantl 482 |
. . . . . . . . . . . . 13
|
11 | | mzpindd.co |
. . . . . . . . . . . . 13
|
12 | | mzpindd.1 |
. . . . . . . . . . . . . 14
|
13 | 12 | elrab 3363 |
. . . . . . . . . . . . 13
|
14 | 10, 11, 13 | sylanbrc 698 |
. . . . . . . . . . . 12
|
15 | 14 | ralrimiva 2966 |
. . . . . . . . . . 11
|
16 | 15 | adantr 481 |
. . . . . . . . . 10
|
17 | 8 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
18 | | simpllr 799 |
. . . . . . . . . . . . . . . 16
|
19 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
20 | | elmapg 7870 |
. . . . . . . . . . . . . . . . 17
|
21 | 20 | biimpa 501 |
. . . . . . . . . . . . . . . 16
|
22 | 17, 18, 19, 21 | syl21anc 1325 |
. . . . . . . . . . . . . . 15
|
23 | | simplr 792 |
. . . . . . . . . . . . . . 15
|
24 | 22, 23 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
25 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
26 | 24, 25 | fmptd 6385 |
. . . . . . . . . . . . 13
|
27 | 8, 7 | elmap 7886 |
. . . . . . . . . . . . 13
|
28 | 26, 27 | sylibr 224 |
. . . . . . . . . . . 12
|
29 | | mzpindd.pr |
. . . . . . . . . . . . 13
|
30 | 29 | adantlr 751 |
. . . . . . . . . . . 12
|
31 | | mzpindd.2 |
. . . . . . . . . . . . 13
|
32 | 31 | elrab 3363 |
. . . . . . . . . . . 12
|
33 | 28, 30, 32 | sylanbrc 698 |
. . . . . . . . . . 11
|
34 | 33 | ralrimiva 2966 |
. . . . . . . . . 10
|
35 | 16, 34 | jca 554 |
. . . . . . . . 9
|
36 | | zaddcl 11417 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | 36 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
38 | | simpl 473 |
. . . . . . . . . . . . . . . . . . 19
|
39 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
41 | | inidm 3822 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 37, 38, 39, 40, 40, 41 | off 6912 |
. . . . . . . . . . . . . . . . . 18
|
43 | 42 | ad2ant2r 783 |
. . . . . . . . . . . . . . . . 17
|
44 | 43 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
45 | | mzpindd.ad |
. . . . . . . . . . . . . . . . 17
|
46 | 45 | 3expb 1266 |
. . . . . . . . . . . . . . . 16
|
47 | 44, 46 | jca 554 |
. . . . . . . . . . . . . . 15
|
48 | | zmulcl 11426 |
. . . . . . . . . . . . . . . . . . 19
|
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
50 | 49, 38, 39, 40, 40, 41 | off 6912 |
. . . . . . . . . . . . . . . . 17
|
51 | 50 | ad2ant2r 783 |
. . . . . . . . . . . . . . . 16
|
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . 15
|
53 | | mzpindd.mu |
. . . . . . . . . . . . . . . 16
|
54 | 53 | 3expb 1266 |
. . . . . . . . . . . . . . 15
|
55 | 47, 52, 54 | jca32 558 |
. . . . . . . . . . . . . 14
|
56 | 55 | ex 450 |
. . . . . . . . . . . . 13
|
57 | 8, 7 | elmap 7886 |
. . . . . . . . . . . . . . 15
|
58 | 57 | anbi1i 731 |
. . . . . . . . . . . . . 14
|
59 | 8, 7 | elmap 7886 |
. . . . . . . . . . . . . . 15
|
60 | 59 | anbi1i 731 |
. . . . . . . . . . . . . 14
|
61 | 58, 60 | anbi12i 733 |
. . . . . . . . . . . . 13
|
62 | 8, 7 | elmap 7886 |
. . . . . . . . . . . . . . 15
|
63 | 62 | anbi1i 731 |
. . . . . . . . . . . . . 14
|
64 | 8, 7 | elmap 7886 |
. . . . . . . . . . . . . . 15
|
65 | 64 | anbi1i 731 |
. . . . . . . . . . . . . 14
|
66 | 63, 65 | anbi12i 733 |
. . . . . . . . . . . . 13
|
67 | 56, 61, 66 | 3imtr4g 285 |
. . . . . . . . . . . 12
|
68 | | mzpindd.3 |
. . . . . . . . . . . . . 14
|
69 | 68 | elrab 3363 |
. . . . . . . . . . . . 13
|
70 | | mzpindd.4 |
. . . . . . . . . . . . . 14
|
71 | 70 | elrab 3363 |
. . . . . . . . . . . . 13
|
72 | 69, 71 | anbi12i 733 |
. . . . . . . . . . . 12
|
73 | | mzpindd.5 |
. . . . . . . . . . . . . 14
|
74 | 73 | elrab 3363 |
. . . . . . . . . . . . 13
|
75 | | mzpindd.6 |
. . . . . . . . . . . . . 14
|
76 | 75 | elrab 3363 |
. . . . . . . . . . . . 13
|
77 | 74, 76 | anbi12i 733 |
. . . . . . . . . . . 12
|
78 | 67, 72, 77 | 3imtr4g 285 |
. . . . . . . . . . 11
|
79 | 78 | ralrimivv 2970 |
. . . . . . . . . 10
|
80 | 79 | adantr 481 |
. . . . . . . . 9
|
81 | 6, 35, 80 | jca32 558 |
. . . . . . . 8
|
82 | | elmzpcl 37289 |
. . . . . . . . 9
mzPolyCld
|
83 | 82 | adantl 482 |
. . . . . . . 8
mzPolyCld
|
84 | 81, 83 | mpbird 247 |
. . . . . . 7
mzPolyCld |
85 | | intss1 4492 |
. . . . . . 7
mzPolyCld mzPolyCld |
86 | 84, 85 | syl 17 |
. . . . . 6
mzPolyCld |
87 | 4, 86 | eqsstrd 3639 |
. . . . 5
mzPoly |
88 | 87 | sselda 3603 |
. . . 4
mzPoly
|
89 | 88 | an32s 846 |
. . 3
mzPoly
|
90 | 2, 89 | mpdan 702 |
. 2
mzPoly |
91 | | mzpindd.7 |
. . . 4
|
92 | 91 | elrab 3363 |
. . 3
|
93 | 92 | simprbi 480 |
. 2
|
94 | 90, 93 | syl 17 |
1
mzPoly |