Step | Hyp | Ref
| Expression |
1 | | mzpcompact2 37315 |
. . 3
mzPoly
mzPoly
|
2 | 1 | 3ad2ant3 1084 |
. 2
mzPoly
mzPoly |
3 | | fveq1 6190 |
. . . . . . . . . 10
|
4 | 3 | eqeq1d 2624 |
. . . . . . . . 9
|
5 | 4 | anbi2d 740 |
. . . . . . . 8
|
6 | 5 | rexbidv 3052 |
. . . . . . 7
|
7 | 6 | abbidv 2741 |
. . . . . 6
|
8 | 7 | ad2antll 765 |
. . . . 5
mzPoly
mzPoly
|
9 | | simplll 798 |
. . . . . . . . . . 11
mzPoly
|
10 | | simplrl 800 |
. . . . . . . . . . . 12
mzPoly
|
11 | | fzfi 12771 |
. . . . . . . . . . . 12
|
12 | | unfi 8227 |
. . . . . . . . . . . 12
|
13 | 10, 11, 12 | sylancl 694 |
. . . . . . . . . . 11
mzPoly
|
14 | | ssun2 3777 |
. . . . . . . . . . . 12
|
15 | 14 | a1i 11 |
. . . . . . . . . . 11
mzPoly
|
16 | | eldioph2lem1 37323 |
. . . . . . . . . . 11
|
17 | 9, 13, 15, 16 | syl3anc 1326 |
. . . . . . . . . 10
mzPoly
|
18 | | f1ococnv2 6163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
19 | 18 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
mzPoly
|
20 | 19 | reseq1d 5395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
mzPoly
|
21 | | ssun1 3776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
22 | | resabs1 5427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
24 | 20, 23 | syl6req 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
mzPoly
|
25 | | resco 5639 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
26 | 24, 25 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
mzPoly
|
27 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
mzPoly
|
28 | 27 | coeq2d 5284 |
. . . . . . . . . . . . . . . . . . . . . . 23
mzPoly
|
29 | | coires1 5653 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
30 | | coass 5654 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
31 | 30 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
32 | 28, 29, 31 | 3eqtr3g 2679 |
. . . . . . . . . . . . . . . . . . . . . 22
mzPoly
|
33 | 32 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
mzPoly
|
34 | | ovexd 6680 |
. . . . . . . . . . . . . . . . . . . . . . 23
mzPoly
|
35 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
mzPoly
|
36 | | f1of1 6136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
37 | 36 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
mzPoly
|
38 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
mzPoly
|
39 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
40 | 39 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
mzPoly
|
41 | 38, 40 | unssd 3789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
mzPoly
|
42 | 41 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
mzPoly
|
43 | | f1ss 6106 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
44 | 37, 42, 43 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
mzPoly
|
45 | | f1f 6101 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
mzPoly
|
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
mzPoly
|
48 | | mapco2g 37277 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
49 | 34, 35, 47, 48 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
mzPoly
|
50 | | coeq1 5279 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
51 | 50 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
52 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
53 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
54 | 51, 52, 53 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . 22
|
55 | 49, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
mzPoly
|
56 | 33, 55 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
|
57 | 56 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . . 19
mzPoly
|
58 | 57 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . 18
mzPoly
|
59 | 58 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . 17
mzPoly
|
60 | 59 | anbi2d 740 |
. . . . . . . . . . . . . . . 16
mzPoly
|
61 | 60 | rexbidv 3052 |
. . . . . . . . . . . . . . 15
mzPoly
|
62 | 61 | abbidv 2741 |
. . . . . . . . . . . . . 14
mzPoly
|
63 | | simplrl 800 |
. . . . . . . . . . . . . . . 16
mzPoly |
64 | 63 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
mzPoly
|
65 | | simprr 796 |
. . . . . . . . . . . . . . 15
mzPoly
|
66 | | diophrw 37322 |
. . . . . . . . . . . . . . 15
|
67 | 64, 44, 65, 66 | syl3anc 1326 |
. . . . . . . . . . . . . 14
mzPoly
|
68 | 62, 67 | eqtrd 2656 |
. . . . . . . . . . . . 13
mzPoly
|
69 | | simp-5l 808 |
. . . . . . . . . . . . . 14
mzPoly
|
70 | | simplrl 800 |
. . . . . . . . . . . . . 14
mzPoly
|
71 | | ovexd 6680 |
. . . . . . . . . . . . . . 15
mzPoly
|
72 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
mzPoly
mzPoly |
73 | 72 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
mzPoly
mzPoly |
74 | | f1ocnv 6149 |
. . . . . . . . . . . . . . . . . 18
|
75 | | f1of 6137 |
. . . . . . . . . . . . . . . . . 18
|
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
77 | | fssres 6070 |
. . . . . . . . . . . . . . . . 17
|
78 | 76, 21, 77 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
79 | 78 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
mzPoly
|
80 | | mzprename 37312 |
. . . . . . . . . . . . . . 15
mzPoly
mzPoly |
81 | 71, 73, 79, 80 | syl3anc 1326 |
. . . . . . . . . . . . . 14
mzPoly
mzPoly |
82 | | eldioph 37321 |
. . . . . . . . . . . . . 14
mzPoly
Dioph |
83 | 69, 70, 81, 82 | syl3anc 1326 |
. . . . . . . . . . . . 13
mzPoly
Dioph |
84 | 68, 83 | eqeltrd 2701 |
. . . . . . . . . . . 12
mzPoly
Dioph |
85 | 84 | ex 450 |
. . . . . . . . . . 11
mzPoly
Dioph |
86 | 85 | rexlimdvva 3038 |
. . . . . . . . . 10
mzPoly
Dioph |
87 | 17, 86 | mpd 15 |
. . . . . . . . 9
mzPoly
Dioph |
88 | 87 | exp31 630 |
. . . . . . . 8
mzPoly
Dioph |
89 | 88 | 3adant3 1081 |
. . . . . . 7
mzPoly
mzPoly
Dioph |
90 | 89 | imp31 448 |
. . . . . 6
mzPoly
mzPoly Dioph |
91 | 90 | adantrr 753 |
. . . . 5
mzPoly
mzPoly
Dioph |
92 | 8, 91 | eqeltrd 2701 |
. . . 4
mzPoly
mzPoly
Dioph |
93 | 92 | ex 450 |
. . 3
mzPoly mzPoly
Dioph |
94 | 93 | rexlimdvva 3038 |
. 2
mzPoly mzPoly
Dioph |
95 | 2, 94 | mpd 15 |
1
mzPoly
Dioph |