Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . . . 8
|
2 | | eqid 2622 |
. . . . . . . 8
|
3 | | lsmub1.p |
. . . . . . . 8
|
4 | 1, 2, 3 | lsmval 18063 |
. . . . . . 7
SubGrp SubGrp
|
5 | 4 | 3adant3 1081 |
. . . . . 6
SubGrp SubGrp
SubGrp |
6 | 5 | rexeqdv 3145 |
. . . . 5
SubGrp SubGrp
SubGrp
|
7 | | ovex 6678 |
. . . . . . 7
|
8 | 7 | rgen2w 2925 |
. . . . . 6
|
9 | | eqid 2622 |
. . . . . . 7
|
10 | | oveq1 6657 |
. . . . . . . . 9
|
11 | 10 | eqeq2d 2632 |
. . . . . . . 8
|
12 | 11 | rexbidv 3052 |
. . . . . . 7
|
13 | 9, 12 | rexrnmpt2 6776 |
. . . . . 6
|
14 | 8, 13 | ax-mp 5 |
. . . . 5
|
15 | 6, 14 | syl6bb 276 |
. . . 4
SubGrp SubGrp
SubGrp
|
16 | 1, 2, 3 | lsmval 18063 |
. . . . . . . . . 10
SubGrp SubGrp
|
17 | 16 | 3adant1 1079 |
. . . . . . . . 9
SubGrp SubGrp
SubGrp |
18 | 17 | rexeqdv 3145 |
. . . . . . . 8
SubGrp SubGrp
SubGrp
|
19 | | ovex 6678 |
. . . . . . . . . 10
|
20 | 19 | rgen2w 2925 |
. . . . . . . . 9
|
21 | | eqid 2622 |
. . . . . . . . . 10
|
22 | | oveq2 6658 |
. . . . . . . . . . 11
|
23 | 22 | eqeq2d 2632 |
. . . . . . . . . 10
|
24 | 21, 23 | rexrnmpt2 6776 |
. . . . . . . . 9
|
25 | 20, 24 | ax-mp 5 |
. . . . . . . 8
|
26 | 18, 25 | syl6bb 276 |
. . . . . . 7
SubGrp SubGrp
SubGrp
|
27 | 26 | adantr 481 |
. . . . . 6
SubGrp SubGrp
SubGrp
|
28 | | subgrcl 17599 |
. . . . . . . . . . 11
SubGrp
|
29 | 28 | 3ad2ant1 1082 |
. . . . . . . . . 10
SubGrp SubGrp
SubGrp
|
30 | 29 | ad2antrr 762 |
. . . . . . . . 9
SubGrp
SubGrp SubGrp
|
31 | 1 | subgss 17595 |
. . . . . . . . . . . 12
SubGrp
|
32 | 31 | 3ad2ant1 1082 |
. . . . . . . . . . 11
SubGrp SubGrp
SubGrp |
33 | 32 | ad2antrr 762 |
. . . . . . . . . 10
SubGrp
SubGrp SubGrp
|
34 | | simplr 792 |
. . . . . . . . . 10
SubGrp
SubGrp SubGrp
|
35 | 33, 34 | sseldd 3604 |
. . . . . . . . 9
SubGrp
SubGrp SubGrp
|
36 | 1 | subgss 17595 |
. . . . . . . . . . . 12
SubGrp
|
37 | 36 | 3ad2ant2 1083 |
. . . . . . . . . . 11
SubGrp SubGrp
SubGrp |
38 | 37 | ad2antrr 762 |
. . . . . . . . . 10
SubGrp
SubGrp SubGrp
|
39 | | simprl 794 |
. . . . . . . . . 10
SubGrp
SubGrp SubGrp
|
40 | 38, 39 | sseldd 3604 |
. . . . . . . . 9
SubGrp
SubGrp SubGrp
|
41 | 1 | subgss 17595 |
. . . . . . . . . . . 12
SubGrp
|
42 | 41 | 3ad2ant3 1084 |
. . . . . . . . . . 11
SubGrp SubGrp
SubGrp |
43 | 42 | ad2antrr 762 |
. . . . . . . . . 10
SubGrp
SubGrp SubGrp
|
44 | | simprr 796 |
. . . . . . . . . 10
SubGrp
SubGrp SubGrp
|
45 | 43, 44 | sseldd 3604 |
. . . . . . . . 9
SubGrp
SubGrp SubGrp
|
46 | 1, 2 | grpass 17431 |
. . . . . . . . 9
|
47 | 30, 35, 40, 45, 46 | syl13anc 1328 |
. . . . . . . 8
SubGrp
SubGrp SubGrp
|
48 | 47 | eqeq2d 2632 |
. . . . . . 7
SubGrp
SubGrp SubGrp
|
49 | 48 | 2rexbidva 3056 |
. . . . . 6
SubGrp SubGrp
SubGrp
|
50 | 27, 49 | bitr4d 271 |
. . . . 5
SubGrp SubGrp
SubGrp
|
51 | 50 | rexbidva 3049 |
. . . 4
SubGrp SubGrp
SubGrp
|
52 | 15, 51 | bitr4d 271 |
. . 3
SubGrp SubGrp
SubGrp
|
53 | | grpmnd 17429 |
. . . . . 6
|
54 | 29, 53 | syl 17 |
. . . . 5
SubGrp SubGrp
SubGrp
|
55 | 1, 3 | lsmssv 18058 |
. . . . 5
|
56 | 54, 32, 37, 55 | syl3anc 1326 |
. . . 4
SubGrp SubGrp
SubGrp |
57 | 1, 2, 3 | lsmelvalx 18055 |
. . . 4
|
58 | 29, 56, 42, 57 | syl3anc 1326 |
. . 3
SubGrp SubGrp
SubGrp
|
59 | 1, 3 | lsmssv 18058 |
. . . . 5
|
60 | 54, 37, 42, 59 | syl3anc 1326 |
. . . 4
SubGrp SubGrp
SubGrp |
61 | 1, 2, 3 | lsmelvalx 18055 |
. . . 4
|
62 | 29, 32, 60, 61 | syl3anc 1326 |
. . 3
SubGrp SubGrp
SubGrp
|
63 | 52, 58, 62 | 3bitr4d 300 |
. 2
SubGrp SubGrp
SubGrp
|
64 | 63 | eqrdv 2620 |
1
SubGrp SubGrp
SubGrp
|