Step | Hyp | Ref
| Expression |
1 | | dprd2d.5 |
. . . . . 6
DProd
DProd |
2 | | dprdgrp 18404 |
. . . . . 6
DProd DProd
|
3 | 1, 2 | syl 17 |
. . . . 5
|
4 | | eqid 2622 |
. . . . . 6
|
5 | 4 | subgacs 17629 |
. . . . 5
SubGrp ACS |
6 | | acsmre 16313 |
. . . . 5
SubGrp ACS SubGrp Moore |
7 | 3, 5, 6 | 3syl 18 |
. . . 4
SubGrp Moore |
8 | | dprd2d.k |
. . . 4
mrClsSubGrp |
9 | | dprd2d.2 |
. . . . . 6
SubGrp |
10 | | ffun 6048 |
. . . . . 6
SubGrp |
11 | | funiunfv 6506 |
. . . . . 6
|
12 | 9, 10, 11 | 3syl 18 |
. . . . 5
|
13 | | resss 5422 |
. . . . . . . . . 10
|
14 | 13 | sseli 3599 |
. . . . . . . . 9
|
15 | | dprd2d.1 |
. . . . . . . . . 10
|
16 | | dprd2d.3 |
. . . . . . . . . 10
|
17 | | dprd2d.4 |
. . . . . . . . . 10
DProd |
18 | 15, 9, 16, 17, 1, 8 | dprd2dlem2 18439 |
. . . . . . . . 9
DProd |
19 | 14, 18 | sylan2 491 |
. . . . . . . 8
DProd |
20 | | 1st2nd 7214 |
. . . . . . . . . . . . 13
|
21 | 15, 14, 20 | syl2an 494 |
. . . . . . . . . . . 12
|
22 | | simpr 477 |
. . . . . . . . . . . 12
|
23 | 21, 22 | eqeltrrd 2702 |
. . . . . . . . . . 11
|
24 | | fvex 6201 |
. . . . . . . . . . . . 13
|
25 | 24 | opelres 5401 |
. . . . . . . . . . . 12
|
26 | 25 | simprbi 480 |
. . . . . . . . . . 11
|
27 | 23, 26 | syl 17 |
. . . . . . . . . 10
|
28 | | ovex 6678 |
. . . . . . . . . 10
DProd |
29 | | eqid 2622 |
. . . . . . . . . . 11
DProd DProd |
30 | | sneq 4187 |
. . . . . . . . . . . . . 14
|
31 | 30 | imaeq2d 5466 |
. . . . . . . . . . . . 13
|
32 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
33 | 31, 32 | mpteq12dv 4733 |
. . . . . . . . . . . 12
|
34 | 33 | oveq2d 6666 |
. . . . . . . . . . 11
DProd DProd |
35 | 29, 34 | elrnmpt1s 5373 |
. . . . . . . . . 10
DProd DProd DProd |
36 | 27, 28, 35 | sylancl 694 |
. . . . . . . . 9
DProd DProd |
37 | | elssuni 4467 |
. . . . . . . . 9
DProd DProd DProd DProd |
38 | 36, 37 | syl 17 |
. . . . . . . 8
DProd DProd |
39 | 19, 38 | sstrd 3613 |
. . . . . . 7
DProd |
40 | 39 | ralrimiva 2966 |
. . . . . 6
DProd |
41 | | iunss 4561 |
. . . . . 6
DProd
DProd |
42 | 40, 41 | sylibr 224 |
. . . . 5
DProd |
43 | 12, 42 | eqsstr3d 3640 |
. . . 4
DProd |
44 | | dprd2d.6 |
. . . . . . . . . . . 12
|
45 | 44 | sselda 3603 |
. . . . . . . . . . 11
|
46 | 45, 17 | syldan 487 |
. . . . . . . . . 10
DProd |
47 | | ovex 6678 |
. . . . . . . . . . . 12
|
48 | | eqid 2622 |
. . . . . . . . . . . 12
|
49 | 47, 48 | dmmpti 6023 |
. . . . . . . . . . 11
|
50 | 49 | a1i 11 |
. . . . . . . . . 10
|
51 | | imassrn 5477 |
. . . . . . . . . . . . . 14
|
52 | | frn 6053 |
. . . . . . . . . . . . . . . 16
SubGrp SubGrp |
53 | 9, 52 | syl 17 |
. . . . . . . . . . . . . . 15
SubGrp |
54 | | mresspw 16252 |
. . . . . . . . . . . . . . . 16
SubGrp Moore SubGrp |
55 | 7, 54 | syl 17 |
. . . . . . . . . . . . . . 15
SubGrp |
56 | 53, 55 | sstrd 3613 |
. . . . . . . . . . . . . 14
|
57 | 51, 56 | syl5ss 3614 |
. . . . . . . . . . . . 13
|
58 | | sspwuni 4611 |
. . . . . . . . . . . . 13
|
59 | 57, 58 | sylib 208 |
. . . . . . . . . . . 12
|
60 | 8 | mrccl 16271 |
. . . . . . . . . . . 12
SubGrp Moore SubGrp |
61 | 7, 59, 60 | syl2anc 693 |
. . . . . . . . . . 11
SubGrp |
62 | 61 | adantr 481 |
. . . . . . . . . 10
SubGrp |
63 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
64 | 63, 48, 47 | fvmpt3i 6287 |
. . . . . . . . . . . 12
|
65 | 64 | adantl 482 |
. . . . . . . . . . 11
|
66 | | df-ov 6653 |
. . . . . . . . . . . . . 14
|
67 | | ffn 6045 |
. . . . . . . . . . . . . . . . 17
SubGrp |
68 | 9, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
|
69 | 68 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
70 | 13 | a1i 11 |
. . . . . . . . . . . . . . 15
|
71 | | elrelimasn 5489 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 15, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 72 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
74 | 73 | biimpa 501 |
. . . . . . . . . . . . . . . . 17
|
75 | | df-br 4654 |
. . . . . . . . . . . . . . . . 17
|
76 | 74, 75 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
77 | | simplr 792 |
. . . . . . . . . . . . . . . 16
|
78 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
79 | 78 | opelres 5401 |
. . . . . . . . . . . . . . . 16
|
80 | 76, 77, 79 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
|
81 | | fnfvima 6496 |
. . . . . . . . . . . . . . 15
|
82 | 69, 70, 80, 81 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
83 | 66, 82 | syl5eqel 2705 |
. . . . . . . . . . . . 13
|
84 | | elssuni 4467 |
. . . . . . . . . . . . 13
|
85 | 83, 84 | syl 17 |
. . . . . . . . . . . 12
|
86 | 7, 8, 59 | mrcssidd 16285 |
. . . . . . . . . . . . 13
|
87 | 86 | ad2antrr 762 |
. . . . . . . . . . . 12
|
88 | 85, 87 | sstrd 3613 |
. . . . . . . . . . 11
|
89 | 65, 88 | eqsstrd 3639 |
. . . . . . . . . 10
|
90 | 46, 50, 62, 89 | dprdlub 18425 |
. . . . . . . . 9
DProd
|
91 | | ovex 6678 |
. . . . . . . . . 10
DProd |
92 | 91 | elpw 4164 |
. . . . . . . . 9
DProd DProd
|
93 | 90, 92 | sylibr 224 |
. . . . . . . 8
DProd |
94 | 93, 29 | fmptd 6385 |
. . . . . . 7
DProd |
95 | | frn 6053 |
. . . . . . 7
DProd
DProd |
96 | 94, 95 | syl 17 |
. . . . . 6
DProd
|
97 | | sspwuni 4611 |
. . . . . 6
DProd DProd |
98 | 96, 97 | sylib 208 |
. . . . 5
DProd |
99 | 7, 8 | mrcssvd 16283 |
. . . . 5
|
100 | 98, 99 | sstrd 3613 |
. . . 4
DProd |
101 | 7, 8, 43, 100 | mrcssd 16284 |
. . 3
DProd |
102 | 8 | mrcsscl 16280 |
. . . 4
SubGrp Moore DProd
SubGrp DProd |
103 | 7, 98, 61, 102 | syl3anc 1326 |
. . 3
DProd
|
104 | 101, 103 | eqssd 3620 |
. 2
DProd |
105 | | eqid 2622 |
. . . . . . . 8
DProd DProd |
106 | 91, 105 | dmmpti 6023 |
. . . . . . 7
DProd |
107 | 106 | a1i 11 |
. . . . . 6
DProd |
108 | 1, 107, 44 | dprdres 18427 |
. . . . 5
DProd DProd DProd DProd
DProd DProd |
109 | 108 | simpld 475 |
. . . 4
DProd
DProd |
110 | 44 | resmptd 5452 |
. . . 4
DProd
DProd |
111 | 109, 110 | breqtrd 4679 |
. . 3
DProd
DProd |
112 | 8 | dprdspan 18426 |
. . 3
DProd DProd
DProd DProd DProd |
113 | 111, 112 | syl 17 |
. 2
DProd DProd DProd |
114 | 104, 113 | eqtr4d 2659 |
1
DProd DProd |