Step | Hyp | Ref
| Expression |
1 | | wrdf 13310 |
. . . . . . . 8
Word ..^ |
2 | 1 | ad2antlr 763 |
. . . . . . 7
Word DProd DProd ..^ |
3 | | fdm 6051 |
. . . . . . 7
..^
..^ |
4 | 2, 3 | syl 17 |
. . . . . 6
Word DProd DProd
..^ |
5 | | fzofi 12773 |
. . . . . 6
..^ |
6 | 4, 5 | syl6eqel 2709 |
. . . . 5
Word DProd DProd
|
7 | 4 | feq2d 6031 |
. . . . . . . . . . 11
Word DProd DProd ..^ |
8 | 2, 7 | mpbird 247 |
. . . . . . . . . 10
Word DProd DProd |
9 | 8 | ffvelrnda 6359 |
. . . . . . . . 9
Word DProd
DProd
|
10 | | oveq2 6658 |
. . . . . . . . . . . 12
↾s ↾s |
11 | 10 | eleq1d 2686 |
. . . . . . . . . . 11
↾s CycGrp
pGrp
↾s CycGrp pGrp |
12 | | ablfac.c |
. . . . . . . . . . 11
SubGrp ↾s CycGrp pGrp |
13 | 11, 12 | elrab2 3366 |
. . . . . . . . . 10
SubGrp
↾s CycGrp
pGrp |
14 | 13 | simplbi 476 |
. . . . . . . . 9
SubGrp |
15 | 9, 14 | syl 17 |
. . . . . . . 8
Word DProd
DProd
SubGrp |
16 | | ablfac.b |
. . . . . . . . 9
|
17 | 16 | subgss 17595 |
. . . . . . . 8
SubGrp
|
18 | 15, 17 | syl 17 |
. . . . . . 7
Word DProd
DProd
|
19 | | inss1 3833 |
. . . . . . . . . . 11
CycGrp pGrp CycGrp |
20 | 13 | simprbi 480 |
. . . . . . . . . . . 12
↾s CycGrp pGrp |
21 | 9, 20 | syl 17 |
. . . . . . . . . . 11
Word DProd
DProd
↾s CycGrp pGrp |
22 | 19, 21 | sseldi 3601 |
. . . . . . . . . 10
Word DProd
DProd
↾s CycGrp |
23 | | eqid 2622 |
. . . . . . . . . . . 12
↾s ↾s |
24 | | eqid 2622 |
. . . . . . . . . . . 12
.g ↾s .g ↾s |
25 | 23, 24 | iscyg 18281 |
. . . . . . . . . . 11
↾s CycGrp
↾s ↾s .g ↾s ↾s |
26 | 25 | simprbi 480 |
. . . . . . . . . 10
↾s CycGrp
↾s .g
↾s ↾s |
27 | 22, 26 | syl 17 |
. . . . . . . . 9
Word DProd
DProd
↾s .g ↾s ↾s |
28 | | eqid 2622 |
. . . . . . . . . . . 12
↾s ↾s |
29 | 28 | subgbas 17598 |
. . . . . . . . . . 11
SubGrp
↾s |
30 | 15, 29 | syl 17 |
. . . . . . . . . 10
Word DProd
DProd
↾s |
31 | 30 | rexeqdv 3145 |
. . . . . . . . 9
Word DProd
DProd
.g
↾s ↾s
↾s .g ↾s ↾s |
32 | 27, 31 | mpbird 247 |
. . . . . . . 8
Word DProd
DProd
.g
↾s ↾s |
33 | 15 | ad2antrr 762 |
. . . . . . . . . . . . 13
Word DProd DProd
SubGrp |
34 | | simpr 477 |
. . . . . . . . . . . . 13
Word DProd DProd
|
35 | | simplr 792 |
. . . . . . . . . . . . 13
Word DProd DProd
|
36 | | ablfac2.m |
. . . . . . . . . . . . . 14
.g |
37 | 36, 28, 24 | subgmulg 17608 |
. . . . . . . . . . . . 13
SubGrp
.g
↾s |
38 | 33, 34, 35, 37 | syl3anc 1326 |
. . . . . . . . . . . 12
Word DProd DProd
.g ↾s |
39 | 38 | mpteq2dva 4744 |
. . . . . . . . . . 11
Word DProd DProd
.g ↾s |
40 | 39 | rneqd 5353 |
. . . . . . . . . 10
Word DProd DProd
.g ↾s |
41 | 30 | adantr 481 |
. . . . . . . . . 10
Word DProd DProd
↾s |
42 | 40, 41 | eqeq12d 2637 |
. . . . . . . . 9
Word DProd DProd
.g
↾s ↾s |
43 | 42 | rexbidva 3049 |
. . . . . . . 8
Word DProd
DProd
.g
↾s ↾s |
44 | 32, 43 | mpbird 247 |
. . . . . . 7
Word DProd
DProd
|
45 | | ssrexv 3667 |
. . . . . . 7
|
46 | 18, 44, 45 | sylc 65 |
. . . . . 6
Word DProd
DProd
|
47 | 46 | ralrimiva 2966 |
. . . . 5
Word DProd DProd
|
48 | | oveq2 6658 |
. . . . . . . . 9
|
49 | 48 | mpteq2dv 4745 |
. . . . . . . 8
|
50 | 49 | rneqd 5353 |
. . . . . . 7
|
51 | 50 | eqeq1d 2624 |
. . . . . 6
|
52 | 51 | ac6sfi 8204 |
. . . . 5
|
53 | 6, 47, 52 | syl2anc 693 |
. . . 4
Word DProd DProd |
54 | | simprl 794 |
. . . . . . . . 9
Word DProd
DProd
|
55 | 4 | adantr 481 |
. . . . . . . . . 10
Word DProd
DProd
..^ |
56 | 55 | feq2d 6031 |
. . . . . . . . 9
Word DProd
DProd
..^ |
57 | 54, 56 | mpbid 222 |
. . . . . . . 8
Word DProd
DProd
..^ |
58 | | iswrdi 13309 |
. . . . . . . 8
..^ Word |
59 | 57, 58 | syl 17 |
. . . . . . 7
Word DProd
DProd
Word |
60 | | fdm 6051 |
. . . . . . . . . . . . . 14
..^
..^ |
61 | 57, 60 | syl 17 |
. . . . . . . . . . . . 13
Word DProd
DProd
..^ |
62 | 61, 55 | eqtr4d 2659 |
. . . . . . . . . . . 12
Word DProd
DProd
|
63 | 62 | eleq2d 2687 |
. . . . . . . . . . 11
Word DProd
DProd
|
64 | 63 | biimpa 501 |
. . . . . . . . . 10
Word DProd DProd |
65 | | simprr 796 |
. . . . . . . . . . . 12
Word DProd
DProd
|
66 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
|
67 | 66 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
68 | 67 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
69 | 68 | mpteq2dva 4744 |
. . . . . . . . . . . . . . 15
|
70 | 69 | rneqd 5353 |
. . . . . . . . . . . . . 14
|
71 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
72 | 70, 71 | eqeq12d 2637 |
. . . . . . . . . . . . 13
|
73 | 72 | rspccva 3308 |
. . . . . . . . . . . 12
|
74 | 65, 73 | sylan 488 |
. . . . . . . . . . 11
Word DProd DProd
|
75 | 8 | adantr 481 |
. . . . . . . . . . . 12
Word DProd
DProd
|
76 | 75 | ffvelrnda 6359 |
. . . . . . . . . . 11
Word DProd DProd |
77 | 74, 76 | eqeltrd 2701 |
. . . . . . . . . 10
Word DProd DProd
|
78 | 64, 77 | syldan 487 |
. . . . . . . . 9
Word DProd DProd
|
79 | | ablfac2.s |
. . . . . . . . . 10
|
80 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
81 | 80 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
82 | 81 | mpteq2dv 4745 |
. . . . . . . . . . . 12
|
83 | 82 | rneqd 5353 |
. . . . . . . . . . 11
|
84 | 83 | cbvmptv 4750 |
. . . . . . . . . 10
|
85 | 79, 84 | eqtri 2644 |
. . . . . . . . 9
|
86 | 78, 85 | fmptd 6385 |
. . . . . . . 8
Word DProd
DProd
|
87 | | simprl 794 |
. . . . . . . . . 10
Word DProd DProd DProd |
88 | 87 | adantr 481 |
. . . . . . . . 9
Word DProd
DProd
DProd |
89 | 62 | raleqdv 3144 |
. . . . . . . . . . . . 13
Word DProd
DProd
|
90 | 65, 89 | mpbird 247 |
. . . . . . . . . . . 12
Word DProd
DProd
|
91 | | mpteq12 4736 |
. . . . . . . . . . . 12
|
92 | 62, 90, 91 | syl2anc 693 |
. . . . . . . . . . 11
Word DProd
DProd
|
93 | 79, 92 | syl5eq 2668 |
. . . . . . . . . 10
Word DProd
DProd
|
94 | | dprdf 18405 |
. . . . . . . . . . . 12
DProd SubGrp |
95 | 88, 94 | syl 17 |
. . . . . . . . . . 11
Word DProd
DProd
SubGrp |
96 | 95 | feqmptd 6249 |
. . . . . . . . . 10
Word DProd
DProd
|
97 | 93, 96 | eqtr4d 2659 |
. . . . . . . . 9
Word DProd
DProd
|
98 | 88, 97 | breqtrrd 4681 |
. . . . . . . 8
Word DProd
DProd
DProd |
99 | 97 | oveq2d 6666 |
. . . . . . . . 9
Word DProd
DProd
DProd DProd |
100 | | simplrr 801 |
. . . . . . . . 9
Word DProd
DProd
DProd |
101 | 99, 100 | eqtrd 2656 |
. . . . . . . 8
Word DProd
DProd
DProd |
102 | 86, 98, 101 | 3jca 1242 |
. . . . . . 7
Word DProd
DProd
DProd
DProd |
103 | 59, 102 | jca 554 |
. . . . . 6
Word DProd
DProd
Word DProd
DProd |
104 | 103 | ex 450 |
. . . . 5
Word DProd DProd Word DProd DProd |
105 | 104 | eximdv 1846 |
. . . 4
Word DProd DProd
Word DProd
DProd |
106 | 53, 105 | mpd 15 |
. . 3
Word DProd DProd Word DProd DProd |
107 | | df-rex 2918 |
. . 3
Word DProd
DProd
Word DProd DProd |
108 | 106, 107 | sylibr 224 |
. 2
Word DProd DProd Word DProd DProd |
109 | | ablfac.1 |
. . 3
|
110 | | ablfac.2 |
. . 3
|
111 | 16, 12, 109, 110 | ablfac 18487 |
. 2
Word DProd
DProd |
112 | 108, 111 | r19.29a 3078 |
1
Word DProd DProd |