Step | Hyp | Ref
| Expression |
1 | | dprdsplit.u |
. . . . . 6
|
2 | 1 | adantr 481 |
. . . . 5
|
3 | 2 | eleq2d 2687 |
. . . 4
|
4 | | elun 3753 |
. . . 4
|
5 | 3, 4 | syl6bb 276 |
. . 3
|
6 | | dmdprdsplit2.1 |
. . . . . . . 8
DProd
|
7 | 6 | ad2antrr 762 |
. . . . . . 7
DProd |
8 | | dprdsplit.2 |
. . . . . . . . . 10
SubGrp |
9 | | ssun1 3776 |
. . . . . . . . . . 11
|
10 | 9, 1 | syl5sseqr 3654 |
. . . . . . . . . 10
|
11 | 8, 10 | fssresd 6071 |
. . . . . . . . 9
SubGrp |
12 | | fdm 6051 |
. . . . . . . . 9
SubGrp |
13 | 11, 12 | syl 17 |
. . . . . . . 8
|
14 | 13 | ad2antrr 762 |
. . . . . . 7
|
15 | | simplr 792 |
. . . . . . 7
|
16 | | simprl 794 |
. . . . . . 7
|
17 | | simprr 796 |
. . . . . . 7
|
18 | | dmdprdsplit.z |
. . . . . . 7
Cntz |
19 | 7, 14, 15, 16, 17, 18 | dprdcntz 18407 |
. . . . . 6
|
20 | | fvres 6207 |
. . . . . . 7
|
21 | 20 | ad2antlr 763 |
. . . . . 6
|
22 | | fvres 6207 |
. . . . . . . 8
|
23 | 22 | ad2antrl 764 |
. . . . . . 7
|
24 | 23 | fveq2d 6195 |
. . . . . 6
|
25 | 19, 21, 24 | 3sstr3d 3647 |
. . . . 5
|
26 | 25 | exp32 631 |
. . . 4
|
27 | 20 | ad2antlr 763 |
. . . . . . 7
|
28 | 6 | ad2antrr 762 |
. . . . . . . 8
DProd |
29 | 13 | ad2antrr 762 |
. . . . . . . 8
|
30 | | simplr 792 |
. . . . . . . 8
|
31 | 28, 29, 30 | dprdub 18424 |
. . . . . . 7
DProd
|
32 | 27, 31 | eqsstr3d 3640 |
. . . . . 6
DProd |
33 | | dmdprdsplit2.3 |
. . . . . . . 8
DProd DProd |
34 | 33 | ad2antrr 762 |
. . . . . . 7
DProd
DProd |
35 | | eqid 2622 |
. . . . . . . . 9
|
36 | 35 | dprdssv 18415 |
. . . . . . . 8
DProd
|
37 | | fvres 6207 |
. . . . . . . . . 10
|
38 | 37 | ad2antrl 764 |
. . . . . . . . 9
|
39 | | dmdprdsplit2.2 |
. . . . . . . . . . 11
DProd
|
40 | 39 | ad2antrr 762 |
. . . . . . . . . 10
DProd |
41 | | ssun2 3777 |
. . . . . . . . . . . . . 14
|
42 | 41, 1 | syl5sseqr 3654 |
. . . . . . . . . . . . 13
|
43 | 8, 42 | fssresd 6071 |
. . . . . . . . . . . 12
SubGrp |
44 | | fdm 6051 |
. . . . . . . . . . . 12
SubGrp |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
|
46 | 45 | ad2antrr 762 |
. . . . . . . . . 10
|
47 | | simprl 794 |
. . . . . . . . . 10
|
48 | 40, 46, 47 | dprdub 18424 |
. . . . . . . . 9
DProd
|
49 | 38, 48 | eqsstr3d 3640 |
. . . . . . . 8
DProd |
50 | 35, 18 | cntz2ss 17765 |
. . . . . . . 8
DProd
DProd
DProd
|
51 | 36, 49, 50 | sylancr 695 |
. . . . . . 7
DProd |
52 | 34, 51 | sstrd 3613 |
. . . . . 6
DProd |
53 | 32, 52 | sstrd 3613 |
. . . . 5
|
54 | 53 | exp32 631 |
. . . 4
|
55 | 26, 54 | jaod 395 |
. . 3
|
56 | 5, 55 | sylbid 230 |
. 2
|
57 | | dprdgrp 18404 |
. . . . . . . 8
DProd |
58 | 6, 57 | syl 17 |
. . . . . . 7
|
59 | 58 | adantr 481 |
. . . . . 6
|
60 | 35 | subgacs 17629 |
. . . . . 6
SubGrp ACS |
61 | | acsmre 16313 |
. . . . . 6
SubGrp ACS SubGrp Moore |
62 | 59, 60, 61 | 3syl 18 |
. . . . 5
SubGrp Moore |
63 | | difundir 3880 |
. . . . . . . . . . 11
|
64 | 2 | difeq1d 3727 |
. . . . . . . . . . 11
|
65 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
66 | 65 | snssd 4340 |
. . . . . . . . . . . . . . 15
|
67 | | sslin 3839 |
. . . . . . . . . . . . . . 15
|
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . 14
|
69 | | incom 3805 |
. . . . . . . . . . . . . . 15
|
70 | | dprdsplit.i |
. . . . . . . . . . . . . . . 16
|
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . 15
|
72 | 69, 71 | syl5eqr 2670 |
. . . . . . . . . . . . . 14
|
73 | | sseq0 3975 |
. . . . . . . . . . . . . 14
|
74 | 68, 72, 73 | syl2anc 693 |
. . . . . . . . . . . . 13
|
75 | | disj3 4021 |
. . . . . . . . . . . . 13
|
76 | 74, 75 | sylib 208 |
. . . . . . . . . . . 12
|
77 | 76 | uneq2d 3767 |
. . . . . . . . . . 11
|
78 | 63, 64, 77 | 3eqtr4a 2682 |
. . . . . . . . . 10
|
79 | 78 | imaeq2d 5466 |
. . . . . . . . 9
|
80 | | imaundi 5545 |
. . . . . . . . 9
|
81 | 79, 80 | syl6eq 2672 |
. . . . . . . 8
|
82 | 81 | unieqd 4446 |
. . . . . . 7
|
83 | | uniun 4456 |
. . . . . . 7
|
84 | 82, 83 | syl6eq 2672 |
. . . . . 6
|
85 | | dmdprdsplit2lem.k |
. . . . . . . . 9
mrClsSubGrp |
86 | | difss 3737 |
. . . . . . . . . . 11
|
87 | | imass2 5501 |
. . . . . . . . . . 11
|
88 | | uniss 4458 |
. . . . . . . . . . 11
|
89 | 86, 87, 88 | mp2b 10 |
. . . . . . . . . 10
|
90 | | imassrn 5477 |
. . . . . . . . . . . 12
|
91 | | frn 6053 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp |
92 | 8, 91 | syl 17 |
. . . . . . . . . . . . . 14
SubGrp |
93 | 92 | adantr 481 |
. . . . . . . . . . . . 13
SubGrp |
94 | | mresspw 16252 |
. . . . . . . . . . . . . 14
SubGrp Moore SubGrp |
95 | 62, 94 | syl 17 |
. . . . . . . . . . . . 13
SubGrp |
96 | 93, 95 | sstrd 3613 |
. . . . . . . . . . . 12
|
97 | 90, 96 | syl5ss 3614 |
. . . . . . . . . . 11
|
98 | | sspwuni 4611 |
. . . . . . . . . . 11
|
99 | 97, 98 | sylib 208 |
. . . . . . . . . 10
|
100 | 89, 99 | syl5ss 3614 |
. . . . . . . . 9
|
101 | 62, 85, 100 | mrcssidd 16285 |
. . . . . . . 8
|
102 | | imassrn 5477 |
. . . . . . . . . . . 12
|
103 | 102, 96 | syl5ss 3614 |
. . . . . . . . . . 11
|
104 | | sspwuni 4611 |
. . . . . . . . . . 11
|
105 | 103, 104 | sylib 208 |
. . . . . . . . . 10
|
106 | 62, 85, 105 | mrcssidd 16285 |
. . . . . . . . 9
|
107 | 85 | dprdspan 18426 |
. . . . . . . . . . . 12
DProd DProd |
108 | 39, 107 | syl 17 |
. . . . . . . . . . 11
DProd |
109 | | df-ima 5127 |
. . . . . . . . . . . . 13
|
110 | 109 | unieqi 4445 |
. . . . . . . . . . . 12
|
111 | 110 | fveq2i 6194 |
. . . . . . . . . . 11
|
112 | 108, 111 | syl6eqr 2674 |
. . . . . . . . . 10
DProd |
113 | 112 | adantr 481 |
. . . . . . . . 9
DProd |
114 | 106, 113 | sseqtr4d 3642 |
. . . . . . . 8
DProd |
115 | | unss12 3785 |
. . . . . . . 8
DProd DProd |
116 | 101, 114,
115 | syl2anc 693 |
. . . . . . 7
DProd |
117 | 85 | mrccl 16271 |
. . . . . . . . 9
SubGrp Moore SubGrp |
118 | 62, 100, 117 | syl2anc 693 |
. . . . . . . 8
SubGrp |
119 | | dprdsubg 18423 |
. . . . . . . . . 10
DProd DProd SubGrp |
120 | 39, 119 | syl 17 |
. . . . . . . . 9
DProd SubGrp |
121 | 120 | adantr 481 |
. . . . . . . 8
DProd SubGrp |
122 | | eqid 2622 |
. . . . . . . . 9
|
123 | 122 | lsmunss 18073 |
. . . . . . . 8
SubGrp DProd SubGrp
DProd DProd |
124 | 118, 121,
123 | syl2anc 693 |
. . . . . . 7
DProd DProd |
125 | 116, 124 | sstrd 3613 |
. . . . . 6
DProd |
126 | 84, 125 | eqsstrd 3639 |
. . . . 5
DProd |
127 | 89 | a1i 11 |
. . . . . . . . 9
|
128 | 62, 85, 127, 99 | mrcssd 16284 |
. . . . . . . 8
|
129 | 85 | dprdspan 18426 |
. . . . . . . . . . 11
DProd DProd |
130 | 6, 129 | syl 17 |
. . . . . . . . . 10
DProd |
131 | | df-ima 5127 |
. . . . . . . . . . . 12
|
132 | 131 | unieqi 4445 |
. . . . . . . . . . 11
|
133 | 132 | fveq2i 6194 |
. . . . . . . . . 10
|
134 | 130, 133 | syl6eqr 2674 |
. . . . . . . . 9
DProd |
135 | 134 | adantr 481 |
. . . . . . . 8
DProd |
136 | 128, 135 | sseqtr4d 3642 |
. . . . . . 7
DProd
|
137 | 33 | adantr 481 |
. . . . . . 7
DProd
DProd |
138 | 136, 137 | sstrd 3613 |
. . . . . 6
DProd |
139 | 122, 18 | lsmsubg 18069 |
. . . . . 6
SubGrp DProd SubGrp DProd DProd SubGrp |
140 | 118, 121,
138, 139 | syl3anc 1326 |
. . . . 5
DProd SubGrp |
141 | 85 | mrcsscl 16280 |
. . . . 5
SubGrp Moore
DProd DProd SubGrp DProd |
142 | 62, 126, 140, 141 | syl3anc 1326 |
. . . 4
DProd |
143 | | sslin 3839 |
. . . 4
DProd
DProd |
144 | 142, 143 | syl 17 |
. . 3
DProd |
145 | 10 | sselda 3603 |
. . . . 5
|
146 | 8 | ffvelrnda 6359 |
. . . . 5
SubGrp |
147 | 145, 146 | syldan 487 |
. . . 4
SubGrp |
148 | | dmdprdsplit.0 |
. . . 4
|
149 | 20 | adantl 482 |
. . . . . . . . 9
|
150 | 6 | adantr 481 |
. . . . . . . . . 10
DProd |
151 | 13 | adantr 481 |
. . . . . . . . . 10
|
152 | 150, 151,
65 | dprdub 18424 |
. . . . . . . . 9
DProd |
153 | 149, 152 | eqsstr3d 3640 |
. . . . . . . 8
DProd |
154 | | dprdsubg 18423 |
. . . . . . . . . . 11
DProd DProd SubGrp |
155 | 6, 154 | syl 17 |
. . . . . . . . . 10
DProd SubGrp |
156 | 155 | adantr 481 |
. . . . . . . . 9
DProd SubGrp |
157 | 122 | lsmlub 18078 |
. . . . . . . . 9
SubGrp SubGrp DProd SubGrp
DProd
DProd
DProd |
158 | 147, 118,
156, 157 | syl3anc 1326 |
. . . . . . . 8
DProd
DProd
DProd |
159 | 153, 136,
158 | mpbi2and 956 |
. . . . . . 7
DProd |
160 | | ssrin 3838 |
. . . . . . 7
DProd DProd
DProd DProd |
161 | 159, 160 | syl 17 |
. . . . . 6
DProd DProd
DProd |
162 | | dmdprdsplit2.4 |
. . . . . . 7
DProd DProd |
163 | 162 | adantr 481 |
. . . . . 6
DProd
DProd |
164 | 161, 163 | sseqtrd 3641 |
. . . . 5
DProd |
165 | 122 | lsmub1 18071 |
. . . . . . . . 9
SubGrp SubGrp
|
166 | 147, 118,
165 | syl2anc 693 |
. . . . . . . 8
|
167 | 148 | subg0cl 17602 |
. . . . . . . . 9
SubGrp
|
168 | 147, 167 | syl 17 |
. . . . . . . 8
|
169 | 166, 168 | sseldd 3604 |
. . . . . . 7
|
170 | 148 | subg0cl 17602 |
. . . . . . . 8
DProd SubGrp DProd |
171 | 121, 170 | syl 17 |
. . . . . . 7
DProd |
172 | 169, 171 | elind 3798 |
. . . . . 6
DProd |
173 | 172 | snssd 4340 |
. . . . 5
DProd |
174 | 164, 173 | eqssd 3620 |
. . . 4
DProd |
175 | | resima2 5432 |
. . . . . . . . 9
|
176 | 86, 175 | mp1i 13 |
. . . . . . . 8
|
177 | 176 | unieqd 4446 |
. . . . . . 7
|
178 | 177 | fveq2d 6195 |
. . . . . 6
|
179 | 149, 178 | ineq12d 3815 |
. . . . 5
|
180 | 150, 151,
65, 148, 85 | dprddisj 18408 |
. . . . 5
|
181 | 179, 180 | eqtr3d 2658 |
. . . 4
|
182 | 8 | adantr 481 |
. . . . . . . 8
SubGrp |
183 | | ffun 6048 |
. . . . . . . 8
SubGrp |
184 | | funiunfv 6506 |
. . . . . . . 8
|
185 | 182, 183,
184 | 3syl 18 |
. . . . . . 7
|
186 | 6 | ad2antrr 762 |
. . . . . . . . . . 11
DProd |
187 | 13 | ad2antrr 762 |
. . . . . . . . . . 11
|
188 | | eldifi 3732 |
. . . . . . . . . . . 12
|
189 | 188 | adantl 482 |
. . . . . . . . . . 11
|
190 | | simplr 792 |
. . . . . . . . . . 11
|
191 | | eldifsni 4320 |
. . . . . . . . . . . 12
|
192 | 191 | adantl 482 |
. . . . . . . . . . 11
|
193 | 186, 187,
189, 190, 192, 18 | dprdcntz 18407 |
. . . . . . . . . 10
|
194 | | fvres 6207 |
. . . . . . . . . . 11
|
195 | 189, 194 | syl 17 |
. . . . . . . . . 10
|
196 | 20 | ad2antlr 763 |
. . . . . . . . . . 11
|
197 | 196 | fveq2d 6195 |
. . . . . . . . . 10
|
198 | 193, 195,
197 | 3sstr3d 3647 |
. . . . . . . . 9
|
199 | 198 | ralrimiva 2966 |
. . . . . . . 8
|
200 | | iunss 4561 |
. . . . . . . 8
|
201 | 199, 200 | sylibr 224 |
. . . . . . 7
|
202 | 185, 201 | eqsstr3d 3640 |
. . . . . 6
|
203 | 35 | subgss 17595 |
. . . . . . . 8
SubGrp
|
204 | 147, 203 | syl 17 |
. . . . . . 7
|
205 | 35, 18 | cntzsubg 17769 |
. . . . . . 7
SubGrp |
206 | 59, 204, 205 | syl2anc 693 |
. . . . . 6
SubGrp |
207 | 85 | mrcsscl 16280 |
. . . . . 6
SubGrp Moore SubGrp
|
208 | 62, 202, 206, 207 | syl3anc 1326 |
. . . . 5
|
209 | 18, 118, 147, 208 | cntzrecd 18091 |
. . . 4
|
210 | 122, 147,
118, 121, 148, 174, 181, 18, 209 | lsmdisj3 18096 |
. . 3
DProd |
211 | 144, 210 | sseqtrd 3641 |
. 2
|
212 | 56, 211 | jca 554 |
1
|