Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . 6
β’
(invgβπΊ) = (invgβπΊ) |
2 | 1 | issubg3 18953 |
. . . . 5
β’ (πΊ β Grp β (π β (SubGrpβπΊ) β (π β (SubMndβπΊ) β§ βπ₯ β π ((invgβπΊ)βπ₯) β π ))) |
3 | | subgacs.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΊ) |
4 | 3 | submss 18627 |
. . . . . . . . 9
β’ (π β (SubMndβπΊ) β π β π΅) |
5 | 4 | adantl 483 |
. . . . . . . 8
β’ ((πΊ β Grp β§ π β (SubMndβπΊ)) β π β π΅) |
6 | | velpw 4570 |
. . . . . . . 8
β’ (π β π« π΅ β π β π΅) |
7 | 5, 6 | sylibr 233 |
. . . . . . 7
β’ ((πΊ β Grp β§ π β (SubMndβπΊ)) β π β π« π΅) |
8 | | eleq2w 2822 |
. . . . . . . . 9
β’ (π¦ = π β (((invgβπΊ)βπ₯) β π¦ β ((invgβπΊ)βπ₯) β π )) |
9 | 8 | raleqbi1dv 3310 |
. . . . . . . 8
β’ (π¦ = π β (βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦ β βπ₯ β π ((invgβπΊ)βπ₯) β π )) |
10 | 9 | elrab3 3651 |
. . . . . . 7
β’ (π β π« π΅ β (π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β βπ₯ β π ((invgβπΊ)βπ₯) β π )) |
11 | 7, 10 | syl 17 |
. . . . . 6
β’ ((πΊ β Grp β§ π β (SubMndβπΊ)) β (π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β βπ₯ β π ((invgβπΊ)βπ₯) β π )) |
12 | 11 | pm5.32da 580 |
. . . . 5
β’ (πΊ β Grp β ((π β (SubMndβπΊ) β§ π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}) β (π β (SubMndβπΊ) β§ βπ₯ β π ((invgβπΊ)βπ₯) β π ))) |
13 | 2, 12 | bitr4d 282 |
. . . 4
β’ (πΊ β Grp β (π β (SubGrpβπΊ) β (π β (SubMndβπΊ) β§ π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}))) |
14 | | elin 3931 |
. . . 4
β’ (π β ((SubMndβπΊ) β© {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}) β (π β (SubMndβπΊ) β§ π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦})) |
15 | 13, 14 | bitr4di 289 |
. . 3
β’ (πΊ β Grp β (π β (SubGrpβπΊ) β π β ((SubMndβπΊ) β© {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}))) |
16 | 15 | eqrdv 2735 |
. 2
β’ (πΊ β Grp β
(SubGrpβπΊ) =
((SubMndβπΊ) β©
{π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦})) |
17 | 3 | fvexi 6861 |
. . . 4
β’ π΅ β V |
18 | | mreacs 17545 |
. . . 4
β’ (π΅ β V β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
19 | 17, 18 | mp1i 13 |
. . 3
β’ (πΊ β Grp β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
20 | | grpmnd 18762 |
. . . 4
β’ (πΊ β Grp β πΊ β Mnd) |
21 | 3 | submacs 18644 |
. . . 4
β’ (πΊ β Mnd β
(SubMndβπΊ) β
(ACSβπ΅)) |
22 | 20, 21 | syl 17 |
. . 3
β’ (πΊ β Grp β
(SubMndβπΊ) β
(ACSβπ΅)) |
23 | 3, 1 | grpinvcl 18805 |
. . . . 5
β’ ((πΊ β Grp β§ π₯ β π΅) β ((invgβπΊ)βπ₯) β π΅) |
24 | 23 | ralrimiva 3144 |
. . . 4
β’ (πΊ β Grp β βπ₯ β π΅ ((invgβπΊ)βπ₯) β π΅) |
25 | | acsfn1 17548 |
. . . 4
β’ ((π΅ β V β§ βπ₯ β π΅ ((invgβπΊ)βπ₯) β π΅) β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β (ACSβπ΅)) |
26 | 17, 24, 25 | sylancr 588 |
. . 3
β’ (πΊ β Grp β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β (ACSβπ΅)) |
27 | | mreincl 17486 |
. . 3
β’
(((ACSβπ΅)
β (Mooreβπ« π΅) β§ (SubMndβπΊ) β (ACSβπ΅) β§ {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β (ACSβπ΅)) β ((SubMndβπΊ) β© {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}) β (ACSβπ΅)) |
28 | 19, 22, 26, 27 | syl3anc 1372 |
. 2
β’ (πΊ β Grp β
((SubMndβπΊ) β©
{π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}) β (ACSβπ΅)) |
29 | 16, 28 | eqeltrd 2838 |
1
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβπ΅)) |