Step | Hyp | Ref
| Expression |
1 | | dprdres.1 |
. . . 4
DProd
|
2 | | dprdgrp 18404 |
. . . 4
DProd
|
3 | 1, 2 | syl 17 |
. . 3
|
4 | | dprdres.2 |
. . . . 5
|
5 | 1, 4 | dprdf2 18406 |
. . . 4
SubGrp |
6 | | dprdres.3 |
. . . 4
|
7 | 5, 6 | fssresd 6071 |
. . 3
SubGrp |
8 | 1 | ad2antrr 762 |
. . . . . . . 8
DProd |
9 | 4 | ad2antrr 762 |
. . . . . . . 8
|
10 | 6 | ad2antrr 762 |
. . . . . . . . 9
|
11 | | simplr 792 |
. . . . . . . . 9
|
12 | 10, 11 | sseldd 3604 |
. . . . . . . 8
|
13 | | eldifi 3732 |
. . . . . . . . . 10
|
14 | 13 | adantl 482 |
. . . . . . . . 9
|
15 | 10, 14 | sseldd 3604 |
. . . . . . . 8
|
16 | | eldifsni 4320 |
. . . . . . . . . 10
|
17 | 16 | adantl 482 |
. . . . . . . . 9
|
18 | 17 | necomd 2849 |
. . . . . . . 8
|
19 | | eqid 2622 |
. . . . . . . 8
Cntz Cntz |
20 | 8, 9, 12, 15, 18, 19 | dprdcntz 18407 |
. . . . . . 7
Cntz |
21 | | fvres 6207 |
. . . . . . . 8
|
22 | 11, 21 | syl 17 |
. . . . . . 7
|
23 | | fvres 6207 |
. . . . . . . . 9
|
24 | 14, 23 | syl 17 |
. . . . . . . 8
|
25 | 24 | fveq2d 6195 |
. . . . . . 7
Cntz Cntz |
26 | 20, 22, 25 | 3sstr4d 3648 |
. . . . . 6
Cntz |
27 | 26 | ralrimiva 2966 |
. . . . 5
Cntz |
28 | 21 | adantl 482 |
. . . . . . 7
|
29 | 28 | ineq1d 3813 |
. . . . . 6
mrClsSubGrp
mrClsSubGrp |
30 | | eqid 2622 |
. . . . . . . . . . . . 13
|
31 | 30 | subgacs 17629 |
. . . . . . . . . . . 12
SubGrp ACS |
32 | | acsmre 16313 |
. . . . . . . . . . . 12
SubGrp ACS SubGrp Moore |
33 | 3, 31, 32 | 3syl 18 |
. . . . . . . . . . 11
SubGrp Moore |
34 | 33 | adantr 481 |
. . . . . . . . . 10
SubGrp Moore |
35 | | eqid 2622 |
. . . . . . . . . 10
mrClsSubGrp mrClsSubGrp |
36 | | resss 5422 |
. . . . . . . . . . . . 13
|
37 | | imass1 5500 |
. . . . . . . . . . . . 13
|
38 | 36, 37 | ax-mp 5 |
. . . . . . . . . . . 12
|
39 | 6 | adantr 481 |
. . . . . . . . . . . . 13
|
40 | | ssdif 3745 |
. . . . . . . . . . . . 13
|
41 | | imass2 5501 |
. . . . . . . . . . . . 13
|
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . . . . . 12
|
43 | 38, 42 | syl5ss 3614 |
. . . . . . . . . . 11
|
44 | 43 | unissd 4462 |
. . . . . . . . . 10
|
45 | | imassrn 5477 |
. . . . . . . . . . . 12
|
46 | | frn 6053 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp |
47 | 5, 46 | syl 17 |
. . . . . . . . . . . . . 14
SubGrp |
48 | 30 | subgss 17595 |
. . . . . . . . . . . . . . . 16
SubGrp
|
49 | | selpw 4165 |
. . . . . . . . . . . . . . . 16
|
50 | 48, 49 | sylibr 224 |
. . . . . . . . . . . . . . 15
SubGrp
|
51 | 50 | ssriv 3607 |
. . . . . . . . . . . . . 14
SubGrp |
52 | 47, 51 | syl6ss 3615 |
. . . . . . . . . . . . 13
|
53 | 52 | adantr 481 |
. . . . . . . . . . . 12
|
54 | 45, 53 | syl5ss 3614 |
. . . . . . . . . . 11
|
55 | | sspwuni 4611 |
. . . . . . . . . . 11
|
56 | 54, 55 | sylib 208 |
. . . . . . . . . 10
|
57 | 34, 35, 44, 56 | mrcssd 16284 |
. . . . . . . . 9
mrClsSubGrp mrClsSubGrp |
58 | | sslin 3839 |
. . . . . . . . 9
mrClsSubGrp mrClsSubGrp mrClsSubGrp mrClsSubGrp
|
59 | 57, 58 | syl 17 |
. . . . . . . 8
mrClsSubGrp
mrClsSubGrp |
60 | 1 | adantr 481 |
. . . . . . . . 9
DProd |
61 | 4 | adantr 481 |
. . . . . . . . 9
|
62 | 6 | sselda 3603 |
. . . . . . . . 9
|
63 | | eqid 2622 |
. . . . . . . . 9
|
64 | 60, 61, 62, 63, 35 | dprddisj 18408 |
. . . . . . . 8
mrClsSubGrp |
65 | 59, 64 | sseqtrd 3641 |
. . . . . . 7
mrClsSubGrp
|
66 | 5 | ffvelrnda 6359 |
. . . . . . . . . . 11
SubGrp |
67 | 62, 66 | syldan 487 |
. . . . . . . . . 10
SubGrp |
68 | 63 | subg0cl 17602 |
. . . . . . . . . 10
SubGrp
|
69 | 67, 68 | syl 17 |
. . . . . . . . 9
|
70 | 44, 56 | sstrd 3613 |
. . . . . . . . . . 11
|
71 | 35 | mrccl 16271 |
. . . . . . . . . . 11
SubGrp Moore mrClsSubGrp
SubGrp |
72 | 34, 70, 71 | syl2anc 693 |
. . . . . . . . . 10
mrClsSubGrp SubGrp |
73 | 63 | subg0cl 17602 |
. . . . . . . . . 10
mrClsSubGrp SubGrp mrClsSubGrp
|
74 | 72, 73 | syl 17 |
. . . . . . . . 9
mrClsSubGrp |
75 | 69, 74 | elind 3798 |
. . . . . . . 8
mrClsSubGrp |
76 | 75 | snssd 4340 |
. . . . . . 7
mrClsSubGrp |
77 | 65, 76 | eqssd 3620 |
. . . . . 6
mrClsSubGrp
|
78 | 29, 77 | eqtrd 2656 |
. . . . 5
mrClsSubGrp
|
79 | 27, 78 | jca 554 |
. . . 4
Cntz
mrClsSubGrp |
80 | 79 | ralrimiva 2966 |
. . 3
Cntz
mrClsSubGrp
|
81 | 1, 4 | dprddomcld 18400 |
. . . . 5
|
82 | 81, 6 | ssexd 4805 |
. . . 4
|
83 | | fdm 6051 |
. . . . 5
SubGrp |
84 | 7, 83 | syl 17 |
. . . 4
|
85 | 19, 63, 35 | dmdprd 18397 |
. . . 4
DProd
SubGrp
Cntz
mrClsSubGrp
|
86 | 82, 84, 85 | syl2anc 693 |
. . 3
DProd
SubGrp
Cntz
mrClsSubGrp
|
87 | 3, 7, 80, 86 | mpbir3and 1245 |
. 2
DProd
|
88 | | rnss 5354 |
. . . . . 6
|
89 | | uniss 4458 |
. . . . . 6
|
90 | 36, 88, 89 | mp2b 10 |
. . . . 5
|
91 | 90 | a1i 11 |
. . . 4
|
92 | | sspwuni 4611 |
. . . . 5
|
93 | 52, 92 | sylib 208 |
. . . 4
|
94 | 33, 35, 91, 93 | mrcssd 16284 |
. . 3
mrClsSubGrp mrClsSubGrp |
95 | 35 | dprdspan 18426 |
. . . 4
DProd DProd mrClsSubGrp |
96 | 87, 95 | syl 17 |
. . 3
DProd mrClsSubGrp |
97 | 35 | dprdspan 18426 |
. . . 4
DProd
DProd mrClsSubGrp |
98 | 1, 97 | syl 17 |
. . 3
DProd mrClsSubGrp |
99 | 94, 96, 98 | 3sstr4d 3648 |
. 2
DProd
DProd |
100 | 87, 99 | jca 554 |
1
DProd DProd
DProd |