Step |
Hyp |
Ref |
Expression |
1 |
|
dmdprdsplitlem.0 |
|
2 |
|
dmdprdsplitlem.w |
|
3 |
|
dmdprdsplitlem.1 |
|
4 |
|
dmdprdsplitlem.2 |
|
5 |
|
dmdprdsplitlem.3 |
|
6 |
|
dmdprdsplitlem.4 |
|
7 |
|
dmdprdsplitlem.5 |
|
8 |
3 4
|
dprdf2 |
|
9 |
8 5
|
fssresd |
|
10 |
|
fdm |
|
11 |
|
eqid |
|
12 |
1 11
|
eldprd |
|
13 |
9 10 12
|
3syl |
|
14 |
7 13
|
mpbid |
|
15 |
14
|
simprd |
|
16 |
15
|
adantr |
|
17 |
|
simprr |
|
18 |
14
|
simpld |
|
19 |
18
|
ad2antrr |
|
20 |
9 10
|
syl |
|
21 |
20
|
ad2antrr |
|
22 |
|
simprl |
|
23 |
|
eqid |
|
24 |
11 19 21 22 23
|
dprdff |
|
25 |
24
|
feqmptd |
|
26 |
5
|
ad2antrr |
|
27 |
26
|
resmptd |
|
28 |
|
iftrue |
|
29 |
28
|
mpteq2ia |
|
30 |
27 29
|
eqtrdi |
|
31 |
25 30
|
eqtr4d |
|
32 |
31
|
oveq2d |
|
33 |
|
eqid |
|
34 |
3
|
ad2antrr |
|
35 |
|
dprdgrp |
|
36 |
|
grpmnd |
|
37 |
34 35 36
|
3syl |
|
38 |
3 4
|
dprddomcld |
|
39 |
38
|
ad2antrr |
|
40 |
4
|
ad2antrr |
|
41 |
19
|
adantr |
|
42 |
21
|
adantr |
|
43 |
|
simplrl |
|
44 |
11 41 42 43
|
dprdfcl |
|
45 |
|
fvres |
|
46 |
45
|
adantl |
|
47 |
44 46
|
eleqtrd |
|
48 |
8
|
ad2antrr |
|
49 |
48
|
ffvelrnda |
|
50 |
1
|
subg0cl |
|
51 |
49 50
|
syl |
|
52 |
51
|
adantr |
|
53 |
47 52
|
ifclda |
|
54 |
38
|
mptexd |
|
55 |
54
|
ad2antrr |
|
56 |
|
funmpt |
|
57 |
56
|
a1i |
|
58 |
11 19 21 22
|
dprdffsupp |
|
59 |
|
simpr |
|
60 |
|
eldifn |
|
61 |
60
|
ad2antlr |
|
62 |
59 61
|
eldifd |
|
63 |
|
ssidd |
|
64 |
38 5
|
ssexd |
|
65 |
64
|
ad2antrr |
|
66 |
1
|
fvexi |
|
67 |
66
|
a1i |
|
68 |
24 63 65 67
|
suppssr |
|
69 |
68
|
adantlr |
|
70 |
62 69
|
syldan |
|
71 |
70
|
ifeq1da |
|
72 |
|
ifid |
|
73 |
71 72
|
eqtrdi |
|
74 |
73 39
|
suppss2 |
|
75 |
|
fsuppsssupp |
|
76 |
55 57 58 74 75
|
syl22anc |
|
77 |
2 34 40 53 76
|
dprdwd |
|
78 |
2 34 40 77 23
|
dprdff |
|
79 |
2 34 40 77 33
|
dprdfcntz |
|
80 |
|
eldifn |
|
81 |
80
|
adantl |
|
82 |
81
|
iffalsed |
|
83 |
82 39
|
suppss2 |
|
84 |
23 1 33 37 39 78 79 83 76
|
gsumzres |
|
85 |
17 32 84
|
3eqtrd |
|
86 |
6
|
ad2antrr |
|
87 |
1 2 34 40 86 77
|
dprdf11 |
|
88 |
85 87
|
mpbid |
|
89 |
88
|
fveq1d |
|
90 |
|
eldifi |
|
91 |
90
|
ad2antlr |
|
92 |
|
eleq1 |
|
93 |
|
fveq2 |
|
94 |
92 93
|
ifbieq1d |
|
95 |
|
eqid |
|
96 |
|
fvex |
|
97 |
96 66
|
ifex |
|
98 |
94 95 97
|
fvmpt3i |
|
99 |
91 98
|
syl |
|
100 |
|
eldifn |
|
101 |
100
|
ad2antlr |
|
102 |
101
|
iffalsed |
|
103 |
89 99 102
|
3eqtrd |
|
104 |
16 103
|
rexlimddv |
|