Step | Hyp | Ref
| Expression |
1 | | cnvimass 5485 |
. . 3
|
2 | | eqid 2622 |
. . . . . 6
|
3 | | eqid 2622 |
. . . . . 6
|
4 | 2, 3 | ghmf 17664 |
. . . . 5
|
5 | 4 | adantr 481 |
. . . 4
SubGrp
|
6 | | fdm 6051 |
. . . 4
|
7 | 5, 6 | syl 17 |
. . 3
SubGrp
|
8 | 1, 7 | syl5sseq 3653 |
. 2
SubGrp
|
9 | | ghmgrp1 17662 |
. . . . . 6
|
10 | 9 | adantr 481 |
. . . . 5
SubGrp
|
11 | | eqid 2622 |
. . . . . 6
|
12 | 2, 11 | grpidcl 17450 |
. . . . 5
|
13 | 10, 12 | syl 17 |
. . . 4
SubGrp
|
14 | | eqid 2622 |
. . . . . . 7
|
15 | 11, 14 | ghmid 17666 |
. . . . . 6
|
16 | 15 | adantr 481 |
. . . . 5
SubGrp
|
17 | 14 | subg0cl 17602 |
. . . . . 6
SubGrp
|
18 | 17 | adantl 482 |
. . . . 5
SubGrp
|
19 | 16, 18 | eqeltrd 2701 |
. . . 4
SubGrp
|
20 | | ffn 6045 |
. . . . . 6
|
21 | 5, 20 | syl 17 |
. . . . 5
SubGrp
|
22 | | elpreima 6337 |
. . . . 5
|
23 | 21, 22 | syl 17 |
. . . 4
SubGrp
|
24 | 13, 19, 23 | mpbir2and 957 |
. . 3
SubGrp
|
25 | | ne0i 3921 |
. . 3
|
26 | 24, 25 | syl 17 |
. 2
SubGrp
|
27 | | elpreima 6337 |
. . . . 5
|
28 | 21, 27 | syl 17 |
. . . 4
SubGrp
|
29 | | elpreima 6337 |
. . . . . . . . . 10
|
30 | 21, 29 | syl 17 |
. . . . . . . . 9
SubGrp
|
31 | 30 | adantr 481 |
. . . . . . . 8
SubGrp |
32 | 9 | ad2antrr 762 |
. . . . . . . . . . 11
SubGrp
|
33 | | simprll 802 |
. . . . . . . . . . 11
SubGrp
|
34 | | simprrl 804 |
. . . . . . . . . . 11
SubGrp
|
35 | | eqid 2622 |
. . . . . . . . . . . 12
|
36 | 2, 35 | grpcl 17430 |
. . . . . . . . . . 11
|
37 | 32, 33, 34, 36 | syl3anc 1326 |
. . . . . . . . . 10
SubGrp
|
38 | | simpll 790 |
. . . . . . . . . . . 12
SubGrp
|
39 | | eqid 2622 |
. . . . . . . . . . . . 13
|
40 | 2, 35, 39 | ghmlin 17665 |
. . . . . . . . . . . 12
|
41 | 38, 33, 34, 40 | syl3anc 1326 |
. . . . . . . . . . 11
SubGrp
|
42 | | simplr 792 |
. . . . . . . . . . . 12
SubGrp
SubGrp |
43 | | simprlr 803 |
. . . . . . . . . . . 12
SubGrp
|
44 | | simprrr 805 |
. . . . . . . . . . . 12
SubGrp
|
45 | 39 | subgcl 17604 |
. . . . . . . . . . . 12
SubGrp
|
46 | 42, 43, 44, 45 | syl3anc 1326 |
. . . . . . . . . . 11
SubGrp
|
47 | 41, 46 | eqeltrd 2701 |
. . . . . . . . . 10
SubGrp
|
48 | | elpreima 6337 |
. . . . . . . . . . . 12
|
49 | 21, 48 | syl 17 |
. . . . . . . . . . 11
SubGrp
|
50 | 49 | adantr 481 |
. . . . . . . . . 10
SubGrp
|
51 | 37, 47, 50 | mpbir2and 957 |
. . . . . . . . 9
SubGrp
|
52 | 51 | expr 643 |
. . . . . . . 8
SubGrp
|
53 | 31, 52 | sylbid 230 |
. . . . . . 7
SubGrp |
54 | 53 | ralrimiv 2965 |
. . . . . 6
SubGrp
|
55 | 10 | adantr 481 |
. . . . . . . 8
SubGrp
|
56 | | simprl 794 |
. . . . . . . 8
SubGrp |
57 | | eqid 2622 |
. . . . . . . . 9
|
58 | 2, 57 | grpinvcl 17467 |
. . . . . . . 8
|
59 | 55, 56, 58 | syl2anc 693 |
. . . . . . 7
SubGrp |
60 | | eqid 2622 |
. . . . . . . . . 10
|
61 | 2, 57, 60 | ghminv 17667 |
. . . . . . . . 9
|
62 | 61 | ad2ant2r 783 |
. . . . . . . 8
SubGrp |
63 | 60 | subginvcl 17603 |
. . . . . . . . 9
SubGrp |
64 | 63 | ad2ant2l 782 |
. . . . . . . 8
SubGrp |
65 | 62, 64 | eqeltrd 2701 |
. . . . . . 7
SubGrp |
66 | | elpreima 6337 |
. . . . . . . . 9
|
67 | 21, 66 | syl 17 |
. . . . . . . 8
SubGrp
|
68 | 67 | adantr 481 |
. . . . . . 7
SubGrp
|
69 | 59, 65, 68 | mpbir2and 957 |
. . . . . 6
SubGrp |
70 | 54, 69 | jca 554 |
. . . . 5
SubGrp |
71 | 70 | ex 450 |
. . . 4
SubGrp
|
72 | 28, 71 | sylbid 230 |
. . 3
SubGrp
|
73 | 72 | ralrimiv 2965 |
. 2
SubGrp
|
74 | 2, 35, 57 | issubg2 17609 |
. . 3
SubGrp
|
75 | 10, 74 | syl 17 |
. 2
SubGrp
SubGrp
|
76 | 8, 26, 73, 75 | mpbir3and 1245 |
1
SubGrp
SubGrp |