| Step | Hyp | Ref
| Expression |
|---|
| 1 | | submacs.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
| 2 | | eqid 2730 |
. . . . . 6
β’
(0gβπΊ) = (0gβπΊ) |
| 3 | | eqid 2730 |
. . . . . 6
β’
(+gβπΊ) = (+gβπΊ) |
| 4 | 1, 2, 3 | issubm 18720 |
. . . . 5
β’ (πΊ β Mnd β (π β (SubMndβπΊ) β (π β π΅ β§ (0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π ))) |
| 5 | | velpw 4606 |
. . . . . . 7
β’ (π β π« π΅ β π β π΅) |
| 6 | 5 | anbi1i 622 |
. . . . . 6
β’ ((π β π« π΅ β§
((0gβπΊ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )) β (π β π΅ β§ ((0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π ))) |
| 7 | | 3anass 1093 |
. . . . . 6
β’ ((π β π΅ β§ (0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π ) β (π β π΅ β§ ((0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π ))) |
| 8 | 6, 7 | bitr4i 277 |
. . . . 5
β’ ((π β π« π΅ β§
((0gβπΊ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )) β (π β π΅ β§ (0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )) |
| 9 | 4, 8 | bitr4di 288 |
. . . 4
β’ (πΊ β Mnd β (π β (SubMndβπΊ) β (π β π« π΅ β§ ((0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )))) |
| 10 | 9 | eqabdv 2865 |
. . 3
β’ (πΊ β Mnd β
(SubMndβπΊ) = {π β£ (π β π« π΅ β§ ((0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π ))}) |
| 11 | | df-rab 3431 |
. . 3
β’ {π β π« π΅ β£
((0gβπΊ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )} = {π β£ (π β π« π΅ β§ ((0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π ))} |
| 12 | 10, 11 | eqtr4di 2788 |
. 2
β’ (πΊ β Mnd β
(SubMndβπΊ) = {π β π« π΅ β£
((0gβπΊ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )}) |
| 13 | | inrab 4305 |
. . 3
β’ ({π β π« π΅ β£
(0gβπΊ)
β π } β© {π β π« π΅ β£ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π }) = {π β π« π΅ β£ ((0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )} |
| 14 | 1 | fvexi 6904 |
. . . . 5
β’ π΅ β V |
| 15 | | mreacs 17606 |
. . . . 5
β’ (π΅ β V β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
| 16 | 14, 15 | mp1i 13 |
. . . 4
β’ (πΊ β Mnd β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
| 17 | 1, 2 | mndidcl 18674 |
. . . . 5
β’ (πΊ β Mnd β
(0gβπΊ)
β π΅) |
| 18 | | acsfn0 17608 |
. . . . 5
β’ ((π΅ β V β§
(0gβπΊ)
β π΅) β {π β π« π΅ β£
(0gβπΊ)
β π } β
(ACSβπ΅)) |
| 19 | 14, 17, 18 | sylancr 585 |
. . . 4
β’ (πΊ β Mnd β {π β π« π΅ β£
(0gβπΊ)
β π } β
(ACSβπ΅)) |
| 20 | 1, 3 | mndcl 18667 |
. . . . . . 7
β’ ((πΊ β Mnd β§ π₯ β π΅ β§ π¦ β π΅) β (π₯(+gβπΊ)π¦) β π΅) |
| 21 | 20 | 3expb 1118 |
. . . . . 6
β’ ((πΊ β Mnd β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΊ)π¦) β π΅) |
| 22 | 21 | ralrimivva 3198 |
. . . . 5
β’ (πΊ β Mnd β βπ₯ β π΅ βπ¦ β π΅ (π₯(+gβπΊ)π¦) β π΅) |
| 23 | | acsfn2 17611 |
. . . . 5
β’ ((π΅ β V β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(+gβπΊ)π¦) β π΅) β {π β π« π΅ β£ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π } β (ACSβπ΅)) |
| 24 | 14, 22, 23 | sylancr 585 |
. . . 4
β’ (πΊ β Mnd β {π β π« π΅ β£ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π } β (ACSβπ΅)) |
| 25 | | mreincl 17547 |
. . . 4
β’
(((ACSβπ΅)
β (Mooreβπ« π΅) β§ {π β π« π΅ β£ (0gβπΊ) β π } β (ACSβπ΅) β§ {π β π« π΅ β£ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π } β (ACSβπ΅)) β ({π β π« π΅ β£ (0gβπΊ) β π } β© {π β π« π΅ β£ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π }) β (ACSβπ΅)) |
| 26 | 16, 19, 24, 25 | syl3anc 1369 |
. . 3
β’ (πΊ β Mnd β ({π β π« π΅ β£
(0gβπΊ)
β π } β© {π β π« π΅ β£ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π }) β (ACSβπ΅)) |
| 27 | 13, 26 | eqeltrrid 2836 |
. 2
β’ (πΊ β Mnd β {π β π« π΅ β£
((0gβπΊ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )} β (ACSβπ΅)) |
| 28 | 12, 27 | eqeltrd 2831 |
1
β’ (πΊ β Mnd β
(SubMndβπΊ) β
(ACSβπ΅)) |
