| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eqid 2732 |
. . . . . 6
β’
(invgβπΊ) = (invgβπΊ) |
| 2 | 1 | issubg3 19018 |
. . . . 5
β’ (πΊ β Grp β (π β (SubGrpβπΊ) β (π β (SubMndβπΊ) β§ βπ₯ β π ((invgβπΊ)βπ₯) β π ))) |
| 3 | | subgacs.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΊ) |
| 4 | 3 | submss 18686 |
. . . . . . . . 9
β’ (π β (SubMndβπΊ) β π β π΅) |
| 5 | 4 | adantl 482 |
. . . . . . . 8
β’ ((πΊ β Grp β§ π β (SubMndβπΊ)) β π β π΅) |
| 6 | | velpw 4606 |
. . . . . . . 8
β’ (π β π« π΅ β π β π΅) |
| 7 | 5, 6 | sylibr 233 |
. . . . . . 7
β’ ((πΊ β Grp β§ π β (SubMndβπΊ)) β π β π« π΅) |
| 8 | | eleq2w 2817 |
. . . . . . . . 9
β’ (π¦ = π β (((invgβπΊ)βπ₯) β π¦ β ((invgβπΊ)βπ₯) β π )) |
| 9 | 8 | raleqbi1dv 3333 |
. . . . . . . 8
β’ (π¦ = π β (βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦ β βπ₯ β π ((invgβπΊ)βπ₯) β π )) |
| 10 | 9 | elrab3 3683 |
. . . . . . 7
β’ (π β π« π΅ β (π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β βπ₯ β π ((invgβπΊ)βπ₯) β π )) |
| 11 | 7, 10 | syl 17 |
. . . . . 6
β’ ((πΊ β Grp β§ π β (SubMndβπΊ)) β (π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β βπ₯ β π ((invgβπΊ)βπ₯) β π )) |
| 12 | 11 | pm5.32da 579 |
. . . . 5
β’ (πΊ β Grp β ((π β (SubMndβπΊ) β§ π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}) β (π β (SubMndβπΊ) β§ βπ₯ β π ((invgβπΊ)βπ₯) β π ))) |
| 13 | 2, 12 | bitr4d 281 |
. . . 4
β’ (πΊ β Grp β (π β (SubGrpβπΊ) β (π β (SubMndβπΊ) β§ π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}))) |
| 14 | | elin 3963 |
. . . 4
β’ (π β ((SubMndβπΊ) β© {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}) β (π β (SubMndβπΊ) β§ π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦})) |
| 15 | 13, 14 | bitr4di 288 |
. . 3
β’ (πΊ β Grp β (π β (SubGrpβπΊ) β π β ((SubMndβπΊ) β© {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}))) |
| 16 | 15 | eqrdv 2730 |
. 2
β’ (πΊ β Grp β
(SubGrpβπΊ) =
((SubMndβπΊ) β©
{π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦})) |
| 17 | 3 | fvexi 6902 |
. . . 4
β’ π΅ β V |
| 18 | | mreacs 17598 |
. . . 4
β’ (π΅ β V β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
| 19 | 17, 18 | mp1i 13 |
. . 3
β’ (πΊ β Grp β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
| 20 | | grpmnd 18822 |
. . . 4
β’ (πΊ β Grp β πΊ β Mnd) |
| 21 | 3 | submacs 18704 |
. . . 4
β’ (πΊ β Mnd β
(SubMndβπΊ) β
(ACSβπ΅)) |
| 22 | 20, 21 | syl 17 |
. . 3
β’ (πΊ β Grp β
(SubMndβπΊ) β
(ACSβπ΅)) |
| 23 | 3, 1 | grpinvcl 18868 |
. . . . 5
β’ ((πΊ β Grp β§ π₯ β π΅) β ((invgβπΊ)βπ₯) β π΅) |
| 24 | 23 | ralrimiva 3146 |
. . . 4
β’ (πΊ β Grp β βπ₯ β π΅ ((invgβπΊ)βπ₯) β π΅) |
| 25 | | acsfn1 17601 |
. . . 4
β’ ((π΅ β V β§ βπ₯ β π΅ ((invgβπΊ)βπ₯) β π΅) β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β (ACSβπ΅)) |
| 26 | 17, 24, 25 | sylancr 587 |
. . 3
β’ (πΊ β Grp β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β (ACSβπ΅)) |
| 27 | | mreincl 17539 |
. . 3
β’
(((ACSβπ΅)
β (Mooreβπ« π΅) β§ (SubMndβπΊ) β (ACSβπ΅) β§ {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β (ACSβπ΅)) β ((SubMndβπΊ) β© {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}) β (ACSβπ΅)) |
| 28 | 19, 22, 26, 27 | syl3anc 1371 |
. 2
β’ (πΊ β Grp β
((SubMndβπΊ) β©
{π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}) β (ACSβπ΅)) |
| 29 | 16, 28 | eqeltrd 2833 |
1
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβπ΅)) |
