Step | Hyp | Ref
| Expression |
1 | | reldmdprd 18396 |
. . . 4
DProd |
2 | 1 | brrelex2i 5159 |
. . 3
DProd
|
3 | 2 | a1i 11 |
. 2
SubGrp
DProd
|
4 | 1 | brrelex2i 5159 |
. . . 4
DProd
|
5 | 4 | adantr 481 |
. . 3
DProd
|
6 | 5 | a1i 11 |
. 2
SubGrp
DProd
|
7 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . 16
SubGrp
SubGrp |
8 | 7 | ad2ant2lr 784 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
SubGrp |
9 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
10 | 9 | subgss 17595 |
. . . . . . . . . . . . . . 15
SubGrp
|
11 | 8, 10 | syl 17 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
|
12 | | subgdprd.1 |
. . . . . . . . . . . . . . . 16
↾s |
13 | 12 | subgbas 17598 |
. . . . . . . . . . . . . . 15
SubGrp
|
14 | 13 | ad2antrr 762 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
|
15 | 11, 14 | sseqtr4d 3642 |
. . . . . . . . . . . . 13
SubGrp SubGrp
|
16 | 15 | biantrud 528 |
. . . . . . . . . . . 12
SubGrp SubGrp
Cntz
Cntz |
17 | | simpll 790 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
SubGrp |
18 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
SubGrp SubGrp
SubGrp |
19 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 19 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
SubGrp SubGrp
|
21 | 18, 20 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
SubGrp SubGrp
SubGrp |
22 | 9 | subgss 17595 |
. . . . . . . . . . . . . . . . 17
SubGrp
|
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
SubGrp SubGrp
|
24 | 23, 14 | sseqtr4d 3642 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
|
25 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
Cntz Cntz |
26 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
Cntz Cntz |
27 | 12, 25, 26 | resscntz 17764 |
. . . . . . . . . . . . . . 15
SubGrp Cntz Cntz |
28 | 17, 24, 27 | syl2anc 693 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
Cntz Cntz |
29 | 28 | sseq2d 3633 |
. . . . . . . . . . . . 13
SubGrp SubGrp
Cntz
Cntz |
30 | | ssin 3835 |
. . . . . . . . . . . . 13
Cntz
Cntz |
31 | 29, 30 | syl6bbr 278 |
. . . . . . . . . . . 12
SubGrp SubGrp
Cntz
Cntz |
32 | 16, 31 | bitr4d 271 |
. . . . . . . . . . 11
SubGrp SubGrp
Cntz
Cntz |
33 | 32 | anassrs 680 |
. . . . . . . . . 10
SubGrp SubGrp
Cntz
Cntz |
34 | 33 | ralbidva 2985 |
. . . . . . . . 9
SubGrp SubGrp
Cntz Cntz |
35 | | subgrcl 17599 |
. . . . . . . . . . . . . . 15
SubGrp
|
36 | 35 | ad2antrr 762 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
|
37 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
38 | 37 | subgacs 17629 |
. . . . . . . . . . . . . 14
SubGrp ACS |
39 | | acsmre 16313 |
. . . . . . . . . . . . . 14
SubGrp ACS SubGrp Moore |
40 | 36, 38, 39 | 3syl 18 |
. . . . . . . . . . . . 13
SubGrp SubGrp
SubGrp Moore |
41 | 12 | subggrp 17597 |
. . . . . . . . . . . . . . . 16
SubGrp
|
42 | 41 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
|
43 | 9 | subgacs 17629 |
. . . . . . . . . . . . . . 15
SubGrp ACS |
44 | | acsmre 16313 |
. . . . . . . . . . . . . . 15
SubGrp ACS SubGrp Moore |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
SubGrp Moore |
46 | | eqid 2622 |
. . . . . . . . . . . . . 14
mrClsSubGrp mrClsSubGrp |
47 | | imassrn 5477 |
. . . . . . . . . . . . . . . . 17
|
48 | | frn 6053 |
. . . . . . . . . . . . . . . . . 18
SubGrp SubGrp |
49 | 48 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
SubGrp SubGrp
SubGrp |
50 | 47, 49 | syl5ss 3614 |
. . . . . . . . . . . . . . . 16
SubGrp SubGrp
SubGrp |
51 | | mresspw 16252 |
. . . . . . . . . . . . . . . . 17
SubGrp Moore SubGrp |
52 | 45, 51 | syl 17 |
. . . . . . . . . . . . . . . 16
SubGrp SubGrp
SubGrp |
53 | 50, 52 | sstrd 3613 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
|
54 | | sspwuni 4611 |
. . . . . . . . . . . . . . 15
|
55 | 53, 54 | sylib 208 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
|
56 | 45, 46, 55 | mrcssidd 16285 |
. . . . . . . . . . . . 13
SubGrp SubGrp
mrClsSubGrp |
57 | 46 | mrccl 16271 |
. . . . . . . . . . . . . . . 16
SubGrp Moore
mrClsSubGrp SubGrp |
58 | 45, 55, 57 | syl2anc 693 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
mrClsSubGrp SubGrp |
59 | 12 | subsubg 17617 |
. . . . . . . . . . . . . . . 16
SubGrp
mrClsSubGrp
SubGrp mrClsSubGrp SubGrp mrClsSubGrp
|
60 | 59 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
mrClsSubGrp SubGrp
mrClsSubGrp
SubGrp
mrClsSubGrp |
61 | 58, 60 | mpbid 222 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
mrClsSubGrp SubGrp mrClsSubGrp
|
62 | 61 | simpld 475 |
. . . . . . . . . . . . 13
SubGrp SubGrp
mrClsSubGrp SubGrp |
63 | | eqid 2622 |
. . . . . . . . . . . . . 14
mrClsSubGrp mrClsSubGrp |
64 | 63 | mrcsscl 16280 |
. . . . . . . . . . . . 13
SubGrp Moore mrClsSubGrp
mrClsSubGrp SubGrp mrClsSubGrp mrClsSubGrp |
65 | 40, 56, 62, 64 | syl3anc 1326 |
. . . . . . . . . . . 12
SubGrp SubGrp
mrClsSubGrp mrClsSubGrp
|
66 | 13 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
SubGrp SubGrp
|
67 | 55, 66 | sseqtr4d 3642 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
|
68 | 37 | subgss 17595 |
. . . . . . . . . . . . . . . 16
SubGrp
|
69 | 68 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
|
70 | 67, 69 | sstrd 3613 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
|
71 | 40, 63, 70 | mrcssidd 16285 |
. . . . . . . . . . . . 13
SubGrp SubGrp
mrClsSubGrp |
72 | 63 | mrccl 16271 |
. . . . . . . . . . . . . . 15
SubGrp Moore
mrClsSubGrp SubGrp |
73 | 40, 70, 72 | syl2anc 693 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
mrClsSubGrp SubGrp |
74 | | simpll 790 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
SubGrp |
75 | 63 | mrcsscl 16280 |
. . . . . . . . . . . . . . 15
SubGrp Moore SubGrp mrClsSubGrp |
76 | 40, 67, 74, 75 | syl3anc 1326 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
mrClsSubGrp |
77 | 12 | subsubg 17617 |
. . . . . . . . . . . . . . 15
SubGrp
mrClsSubGrp
SubGrp mrClsSubGrp SubGrp mrClsSubGrp
|
78 | 77 | ad2antrr 762 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
mrClsSubGrp SubGrp
mrClsSubGrp
SubGrp
mrClsSubGrp |
79 | 73, 76, 78 | mpbir2and 957 |
. . . . . . . . . . . . 13
SubGrp SubGrp
mrClsSubGrp SubGrp |
80 | 46 | mrcsscl 16280 |
. . . . . . . . . . . . 13
SubGrp Moore mrClsSubGrp
mrClsSubGrp SubGrp mrClsSubGrp mrClsSubGrp |
81 | 45, 71, 79, 80 | syl3anc 1326 |
. . . . . . . . . . . 12
SubGrp SubGrp
mrClsSubGrp mrClsSubGrp
|
82 | 65, 81 | eqssd 3620 |
. . . . . . . . . . 11
SubGrp SubGrp
mrClsSubGrp mrClsSubGrp
|
83 | 82 | ineq2d 3814 |
. . . . . . . . . 10
SubGrp SubGrp
mrClsSubGrp mrClsSubGrp |
84 | | eqid 2622 |
. . . . . . . . . . . . 13
|
85 | 12, 84 | subg0 17600 |
. . . . . . . . . . . 12
SubGrp
|
86 | 85 | ad2antrr 762 |
. . . . . . . . . . 11
SubGrp SubGrp
|
87 | 86 | sneqd 4189 |
. . . . . . . . . 10
SubGrp SubGrp
|
88 | 83, 87 | eqeq12d 2637 |
. . . . . . . . 9
SubGrp SubGrp
mrClsSubGrp
mrClsSubGrp |
89 | 34, 88 | anbi12d 747 |
. . . . . . . 8
SubGrp SubGrp
Cntz
mrClsSubGrp
Cntz
mrClsSubGrp |
90 | 89 | ralbidva 2985 |
. . . . . . 7
SubGrp SubGrp
Cntz
mrClsSubGrp
Cntz
mrClsSubGrp |
91 | 90 | pm5.32da 673 |
. . . . . 6
SubGrp
SubGrp
Cntz
mrClsSubGrp
SubGrp
Cntz
mrClsSubGrp |
92 | 12 | subsubg 17617 |
. . . . . . . . . . . . 13
SubGrp
SubGrp SubGrp |
93 | | elin 3796 |
. . . . . . . . . . . . . 14
SubGrp
SubGrp
|
94 | | selpw 4165 |
. . . . . . . . . . . . . . 15
|
95 | 94 | anbi2i 730 |
. . . . . . . . . . . . . 14
SubGrp
SubGrp
|
96 | 93, 95 | bitri 264 |
. . . . . . . . . . . . 13
SubGrp
SubGrp
|
97 | 92, 96 | syl6bbr 278 |
. . . . . . . . . . . 12
SubGrp
SubGrp SubGrp |
98 | 97 | eqrdv 2620 |
. . . . . . . . . . 11
SubGrp
SubGrp SubGrp |
99 | 98 | sseq2d 3633 |
. . . . . . . . . 10
SubGrp
SubGrp
SubGrp |
100 | | ssin 3835 |
. . . . . . . . . 10
SubGrp
SubGrp |
101 | 99, 100 | syl6bbr 278 |
. . . . . . . . 9
SubGrp
SubGrp SubGrp |
102 | 101 | anbi2d 740 |
. . . . . . . 8
SubGrp
SubGrp
SubGrp
|
103 | | df-f 5892 |
. . . . . . . 8
SubGrp
SubGrp |
104 | | df-f 5892 |
. . . . . . . . . 10
SubGrp
SubGrp |
105 | 104 | anbi1i 731 |
. . . . . . . . 9
SubGrp
SubGrp |
106 | | anass 681 |
. . . . . . . . 9
SubGrp
SubGrp
|
107 | 105, 106 | bitri 264 |
. . . . . . . 8
SubGrp
SubGrp
|
108 | 102, 103,
107 | 3bitr4g 303 |
. . . . . . 7
SubGrp
SubGrp
SubGrp |
109 | 108 | anbi1d 741 |
. . . . . 6
SubGrp
SubGrp
Cntz
mrClsSubGrp
SubGrp
Cntz
mrClsSubGrp |
110 | 91, 109 | bitr3d 270 |
. . . . 5
SubGrp
SubGrp
Cntz
mrClsSubGrp
SubGrp
Cntz
mrClsSubGrp |
111 | 110 | adantr 481 |
. . . 4
SubGrp SubGrp
Cntz
mrClsSubGrp
SubGrp
Cntz
mrClsSubGrp |
112 | | dmexg 7097 |
. . . . . 6
|
113 | 112 | adantl 482 |
. . . . 5
SubGrp |
114 | | eqidd 2623 |
. . . . 5
SubGrp |
115 | 41 | adantr 481 |
. . . . 5
SubGrp |
116 | | eqid 2622 |
. . . . . . . 8
|
117 | 26, 116, 46 | dmdprd 18397 |
. . . . . . 7
DProd
SubGrp
Cntz
mrClsSubGrp |
118 | | 3anass 1042 |
. . . . . . 7
SubGrp
Cntz
mrClsSubGrp
SubGrp
Cntz
mrClsSubGrp |
119 | 117, 118 | syl6bb 276 |
. . . . . 6
DProd
SubGrp
Cntz
mrClsSubGrp |
120 | 119 | baibd 948 |
. . . . 5
DProd
SubGrp
Cntz
mrClsSubGrp |
121 | 113, 114,
115, 120 | syl21anc 1325 |
. . . 4
SubGrp DProd
SubGrp
Cntz
mrClsSubGrp |
122 | 35 | adantr 481 |
. . . . . . 7
SubGrp |
123 | 25, 84, 63 | dmdprd 18397 |
. . . . . . . . 9
DProd
SubGrp
Cntz
mrClsSubGrp |
124 | | 3anass 1042 |
. . . . . . . . 9
SubGrp
Cntz
mrClsSubGrp
SubGrp
Cntz
mrClsSubGrp |
125 | 123, 124 | syl6bb 276 |
. . . . . . . 8
DProd
SubGrp
Cntz
mrClsSubGrp |
126 | 125 | baibd 948 |
. . . . . . 7
DProd
SubGrp
Cntz
mrClsSubGrp |
127 | 113, 114,
122, 126 | syl21anc 1325 |
. . . . . 6
SubGrp DProd
SubGrp
Cntz
mrClsSubGrp |
128 | 127 | anbi1d 741 |
. . . . 5
SubGrp DProd
SubGrp
Cntz
mrClsSubGrp
|
129 | | an32 839 |
. . . . 5
SubGrp
Cntz
mrClsSubGrp
SubGrp
Cntz
mrClsSubGrp |
130 | 128, 129 | syl6bb 276 |
. . . 4
SubGrp DProd
SubGrp
Cntz
mrClsSubGrp |
131 | 111, 121,
130 | 3bitr4d 300 |
. . 3
SubGrp DProd
DProd |
132 | 131 | ex 450 |
. 2
SubGrp
DProd DProd |
133 | 3, 6, 132 | pm5.21ndd 369 |
1
SubGrp
DProd DProd |