| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eqid 2731 |
. . . . . 6
β’
(invgβπΊ) = (invgβπΊ) |
| 2 | 1 | issubg3 19067 |
. . . . 5
β’ (πΊ β Grp β (π β (SubGrpβπΊ) β (π β (SubMndβπΊ) β§ βπ₯ β π ((invgβπΊ)βπ₯) β π ))) |
| 3 | | subgacs.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΊ) |
| 4 | 3 | submss 18732 |
. . . . . . . . 9
β’ (π β (SubMndβπΊ) β π β π΅) |
| 5 | 4 | adantl 481 |
. . . . . . . 8
β’ ((πΊ β Grp β§ π β (SubMndβπΊ)) β π β π΅) |
| 6 | | velpw 4607 |
. . . . . . . 8
β’ (π β π« π΅ β π β π΅) |
| 7 | 5, 6 | sylibr 233 |
. . . . . . 7
β’ ((πΊ β Grp β§ π β (SubMndβπΊ)) β π β π« π΅) |
| 8 | | eleq2w 2816 |
. . . . . . . . 9
β’ (π¦ = π β (((invgβπΊ)βπ₯) β π¦ β ((invgβπΊ)βπ₯) β π )) |
| 9 | 8 | raleqbi1dv 3332 |
. . . . . . . 8
β’ (π¦ = π β (βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦ β βπ₯ β π ((invgβπΊ)βπ₯) β π )) |
| 10 | 9 | elrab3 3684 |
. . . . . . 7
β’ (π β π« π΅ β (π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β βπ₯ β π ((invgβπΊ)βπ₯) β π )) |
| 11 | 7, 10 | syl 17 |
. . . . . 6
β’ ((πΊ β Grp β§ π β (SubMndβπΊ)) β (π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β βπ₯ β π ((invgβπΊ)βπ₯) β π )) |
| 12 | 11 | pm5.32da 578 |
. . . . 5
β’ (πΊ β Grp β ((π β (SubMndβπΊ) β§ π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}) β (π β (SubMndβπΊ) β§ βπ₯ β π ((invgβπΊ)βπ₯) β π ))) |
| 13 | 2, 12 | bitr4d 282 |
. . . 4
β’ (πΊ β Grp β (π β (SubGrpβπΊ) β (π β (SubMndβπΊ) β§ π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}))) |
| 14 | | elin 3964 |
. . . 4
β’ (π β ((SubMndβπΊ) β© {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}) β (π β (SubMndβπΊ) β§ π β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦})) |
| 15 | 13, 14 | bitr4di 289 |
. . 3
β’ (πΊ β Grp β (π β (SubGrpβπΊ) β π β ((SubMndβπΊ) β© {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}))) |
| 16 | 15 | eqrdv 2729 |
. 2
β’ (πΊ β Grp β
(SubGrpβπΊ) =
((SubMndβπΊ) β©
{π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦})) |
| 17 | 3 | fvexi 6905 |
. . . 4
β’ π΅ β V |
| 18 | | mreacs 17609 |
. . . 4
β’ (π΅ β V β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
| 19 | 17, 18 | mp1i 13 |
. . 3
β’ (πΊ β Grp β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
| 20 | | grpmnd 18868 |
. . . 4
β’ (πΊ β Grp β πΊ β Mnd) |
| 21 | 3 | submacs 18750 |
. . . 4
β’ (πΊ β Mnd β
(SubMndβπΊ) β
(ACSβπ΅)) |
| 22 | 20, 21 | syl 17 |
. . 3
β’ (πΊ β Grp β
(SubMndβπΊ) β
(ACSβπ΅)) |
| 23 | 3, 1 | grpinvcl 18915 |
. . . . 5
β’ ((πΊ β Grp β§ π₯ β π΅) β ((invgβπΊ)βπ₯) β π΅) |
| 24 | 23 | ralrimiva 3145 |
. . . 4
β’ (πΊ β Grp β βπ₯ β π΅ ((invgβπΊ)βπ₯) β π΅) |
| 25 | | acsfn1 17612 |
. . . 4
β’ ((π΅ β V β§ βπ₯ β π΅ ((invgβπΊ)βπ₯) β π΅) β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β (ACSβπ΅)) |
| 26 | 17, 24, 25 | sylancr 586 |
. . 3
β’ (πΊ β Grp β {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β (ACSβπ΅)) |
| 27 | | mreincl 17550 |
. . 3
β’
(((ACSβπ΅)
β (Mooreβπ« π΅) β§ (SubMndβπΊ) β (ACSβπ΅) β§ {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦} β (ACSβπ΅)) β ((SubMndβπΊ) β© {π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}) β (ACSβπ΅)) |
| 28 | 19, 22, 26, 27 | syl3anc 1370 |
. 2
β’ (πΊ β Grp β
((SubMndβπΊ) β©
{π¦ β π« π΅ β£ βπ₯ β π¦ ((invgβπΊ)βπ₯) β π¦}) β (ACSβπ΅)) |
| 29 | 16, 28 | eqeltrd 2832 |
1
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβπ΅)) |
