Step | Hyp | Ref
| Expression |
1 | | wrd0 13330 |
. . 3
Word |
2 | | pgpfac.g |
. . . . . 6
|
3 | | ablgrp 18198 |
. . . . . 6
|
4 | | eqid 2622 |
. . . . . . 7
|
5 | 4 | dprd0 18430 |
. . . . . 6
DProd DProd |
6 | 2, 3, 5 | 3syl 18 |
. . . . 5
DProd DProd |
7 | 6 | adantr 481 |
. . . 4
gEx ↾s DProd DProd |
8 | | pgpfac.u |
. . . . . . . . 9
SubGrp |
9 | 4 | subg0cl 17602 |
. . . . . . . . 9
SubGrp
|
10 | 8, 9 | syl 17 |
. . . . . . . 8
|
11 | 10 | adantr 481 |
. . . . . . 7
gEx ↾s |
12 | | eqid 2622 |
. . . . . . . . . . 11
↾s ↾s |
13 | 12 | subgbas 17598 |
. . . . . . . . . 10
SubGrp
↾s |
14 | 8, 13 | syl 17 |
. . . . . . . . 9
↾s |
15 | 14 | adantr 481 |
. . . . . . . 8
gEx ↾s ↾s |
16 | 12 | subggrp 17597 |
. . . . . . . . . . 11
SubGrp
↾s |
17 | 8, 16 | syl 17 |
. . . . . . . . . 10
↾s |
18 | | grpmnd 17429 |
. . . . . . . . . 10
↾s
↾s |
19 | | eqid 2622 |
. . . . . . . . . . 11
↾s ↾s |
20 | | eqid 2622 |
. . . . . . . . . . 11
gEx
↾s gEx ↾s |
21 | 19, 20 | gex1 18006 |
. . . . . . . . . 10
↾s gEx ↾s ↾s |
22 | 17, 18, 21 | 3syl 18 |
. . . . . . . . 9
gEx ↾s ↾s |
23 | 22 | biimpa 501 |
. . . . . . . 8
gEx ↾s ↾s |
24 | 15, 23 | eqbrtrd 4675 |
. . . . . . 7
gEx ↾s |
25 | | en1eqsn 8190 |
. . . . . . 7
|
26 | 11, 24, 25 | syl2anc 693 |
. . . . . 6
gEx ↾s |
27 | 26 | eqeq2d 2632 |
. . . . 5
gEx ↾s DProd
DProd |
28 | 27 | anbi2d 740 |
. . . 4
gEx ↾s DProd DProd DProd DProd |
29 | 7, 28 | mpbird 247 |
. . 3
gEx ↾s DProd DProd |
30 | | breq2 4657 |
. . . . 5
DProd
DProd |
31 | | oveq2 6658 |
. . . . . 6
DProd DProd |
32 | 31 | eqeq1d 2624 |
. . . . 5
DProd DProd |
33 | 30, 32 | anbi12d 747 |
. . . 4
DProd
DProd
DProd DProd |
34 | 33 | rspcev 3309 |
. . 3
Word DProd DProd
Word DProd DProd |
35 | 1, 29, 34 | sylancr 695 |
. 2
gEx ↾s Word DProd DProd |
36 | 12 | subgabl 18241 |
. . . . . 6
SubGrp
↾s |
37 | 2, 8, 36 | syl2anc 693 |
. . . . 5
↾s |
38 | | pgpfac.f |
. . . . . . . 8
|
39 | | pgpfac.b |
. . . . . . . . . 10
|
40 | 39 | subgss 17595 |
. . . . . . . . 9
SubGrp
|
41 | 8, 40 | syl 17 |
. . . . . . . 8
|
42 | | ssfi 8180 |
. . . . . . . 8
|
43 | 38, 41, 42 | syl2anc 693 |
. . . . . . 7
|
44 | 14, 43 | eqeltrrd 2702 |
. . . . . 6
↾s |
45 | 19, 20 | gexcl2 18004 |
. . . . . 6
↾s ↾s gEx
↾s |
46 | 17, 44, 45 | syl2anc 693 |
. . . . 5
gEx ↾s |
47 | | eqid 2622 |
. . . . . 6
↾s ↾s |
48 | 19, 20, 47 | gexex 18256 |
. . . . 5
↾s gEx ↾s ↾s ↾s gEx
↾s |
49 | 37, 46, 48 | syl2anc 693 |
. . . 4
↾s ↾s gEx
↾s |
50 | 49 | adantr 481 |
. . 3
gEx ↾s ↾s ↾s gEx ↾s |
51 | | eqid 2622 |
. . . . 5
mrClsSubGrp ↾s mrClsSubGrp ↾s |
52 | | eqid 2622 |
. . . . 5
mrClsSubGrp ↾s mrClsSubGrp ↾s |
53 | | eqid 2622 |
. . . . 5
↾s ↾s |
54 | | eqid 2622 |
. . . . 5
↾s ↾s |
55 | | pgpfac.p |
. . . . . . 7
pGrp |
56 | | subgpgp 18012 |
. . . . . . 7
pGrp SubGrp
pGrp ↾s |
57 | 55, 8, 56 | syl2anc 693 |
. . . . . 6
pGrp ↾s |
58 | 57 | ad2antrr 762 |
. . . . 5
gEx
↾s
↾s
↾s gEx ↾s pGrp
↾s |
59 | 37 | ad2antrr 762 |
. . . . 5
gEx
↾s
↾s
↾s gEx ↾s
↾s |
60 | 44 | ad2antrr 762 |
. . . . 5
gEx
↾s
↾s
↾s gEx ↾s ↾s |
61 | | simprr 796 |
. . . . 5
gEx
↾s
↾s
↾s gEx ↾s
↾s gEx ↾s |
62 | | simprl 794 |
. . . . 5
gEx
↾s
↾s
↾s gEx ↾s
↾s |
63 | 51, 52, 19, 47, 20, 53, 54, 58, 59, 60, 61, 62 | pgpfac1 18479 |
. . . 4
gEx
↾s
↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s ↾s mrClsSubGrp ↾s ↾s ↾s |
64 | | pgpfac.c |
. . . . 5
SubGrp ↾s CycGrp pGrp |
65 | 2 | ad3antrrr 766 |
. . . . 5
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s |
66 | 55 | ad3antrrr 766 |
. . . . 5
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s pGrp |
67 | 38 | ad3antrrr 766 |
. . . . 5
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s |
68 | 8 | ad3antrrr 766 |
. . . . 5
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s SubGrp |
69 | | pgpfac.a |
. . . . . 6
SubGrp Word DProd DProd |
70 | 69 | ad3antrrr 766 |
. . . . 5
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s SubGrp Word DProd
DProd |
71 | | simpllr 799 |
. . . . 5
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s gEx
↾s |
72 | | simplrl 800 |
. . . . . 6
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s ↾s |
73 | 68, 13 | syl 17 |
. . . . . 6
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s ↾s |
74 | 72, 73 | eleqtrrd 2704 |
. . . . 5
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s |
75 | | simplrr 801 |
. . . . 5
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s ↾s gEx ↾s |
76 | | simprl 794 |
. . . . 5
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s SubGrp ↾s |
77 | | simprrl 804 |
. . . . 5
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s mrClsSubGrp
↾s
↾s |
78 | | simprrr 805 |
. . . . . 6
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s mrClsSubGrp
↾s ↾s
↾s |
79 | 78, 73 | eqtr4d 2659 |
. . . . 5
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s mrClsSubGrp
↾s ↾s |
80 | 39, 64, 65, 66, 67, 68, 70, 12, 51, 47, 20, 53, 54, 71, 74, 75, 76, 77, 79 | pgpfaclem2 18481 |
. . . 4
gEx ↾s ↾s
↾s gEx ↾s
SubGrp
↾s mrClsSubGrp ↾s
↾s mrClsSubGrp ↾s ↾s ↾s Word DProd DProd |
81 | 63, 80 | rexlimddv 3035 |
. . 3
gEx
↾s
↾s
↾s gEx ↾s
Word DProd
DProd |
82 | 50, 81 | rexlimddv 3035 |
. 2
gEx ↾s Word DProd DProd |
83 | 35, 82 | pm2.61dane 2881 |
1
Word DProd
DProd |