Step | Hyp | Ref
| Expression |
1 | | submacs.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
2 | | eqid 2733 |
. . . . . 6
β’
(0gβπΊ) = (0gβπΊ) |
3 | | eqid 2733 |
. . . . . 6
β’
(+gβπΊ) = (+gβπΊ) |
4 | 1, 2, 3 | issubm 18619 |
. . . . 5
β’ (πΊ β Mnd β (π β (SubMndβπΊ) β (π β π΅ β§ (0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π ))) |
5 | | velpw 4566 |
. . . . . . 7
β’ (π β π« π΅ β π β π΅) |
6 | 5 | anbi1i 625 |
. . . . . 6
β’ ((π β π« π΅ β§
((0gβπΊ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )) β (π β π΅ β§ ((0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π ))) |
7 | | 3anass 1096 |
. . . . . 6
β’ ((π β π΅ β§ (0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π ) β (π β π΅ β§ ((0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π ))) |
8 | 6, 7 | bitr4i 278 |
. . . . 5
β’ ((π β π« π΅ β§
((0gβπΊ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )) β (π β π΅ β§ (0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )) |
9 | 4, 8 | bitr4di 289 |
. . . 4
β’ (πΊ β Mnd β (π β (SubMndβπΊ) β (π β π« π΅ β§ ((0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )))) |
10 | 9 | abbi2dv 2868 |
. . 3
β’ (πΊ β Mnd β
(SubMndβπΊ) = {π β£ (π β π« π΅ β§ ((0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π ))}) |
11 | | df-rab 3407 |
. . 3
β’ {π β π« π΅ β£
((0gβπΊ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )} = {π β£ (π β π« π΅ β§ ((0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π ))} |
12 | 10, 11 | eqtr4di 2791 |
. 2
β’ (πΊ β Mnd β
(SubMndβπΊ) = {π β π« π΅ β£
((0gβπΊ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )}) |
13 | | inrab 4267 |
. . 3
β’ ({π β π« π΅ β£
(0gβπΊ)
β π } β© {π β π« π΅ β£ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π }) = {π β π« π΅ β£ ((0gβπΊ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )} |
14 | 1 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
15 | | mreacs 17543 |
. . . . 5
β’ (π΅ β V β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
16 | 14, 15 | mp1i 13 |
. . . 4
β’ (πΊ β Mnd β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
17 | 1, 2 | mndidcl 18576 |
. . . . 5
β’ (πΊ β Mnd β
(0gβπΊ)
β π΅) |
18 | | acsfn0 17545 |
. . . . 5
β’ ((π΅ β V β§
(0gβπΊ)
β π΅) β {π β π« π΅ β£
(0gβπΊ)
β π } β
(ACSβπ΅)) |
19 | 14, 17, 18 | sylancr 588 |
. . . 4
β’ (πΊ β Mnd β {π β π« π΅ β£
(0gβπΊ)
β π } β
(ACSβπ΅)) |
20 | 1, 3 | mndcl 18569 |
. . . . . . 7
β’ ((πΊ β Mnd β§ π₯ β π΅ β§ π¦ β π΅) β (π₯(+gβπΊ)π¦) β π΅) |
21 | 20 | 3expb 1121 |
. . . . . 6
β’ ((πΊ β Mnd β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΊ)π¦) β π΅) |
22 | 21 | ralrimivva 3194 |
. . . . 5
β’ (πΊ β Mnd β βπ₯ β π΅ βπ¦ β π΅ (π₯(+gβπΊ)π¦) β π΅) |
23 | | acsfn2 17548 |
. . . . 5
β’ ((π΅ β V β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(+gβπΊ)π¦) β π΅) β {π β π« π΅ β£ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π } β (ACSβπ΅)) |
24 | 14, 22, 23 | sylancr 588 |
. . . 4
β’ (πΊ β Mnd β {π β π« π΅ β£ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π } β (ACSβπ΅)) |
25 | | mreincl 17484 |
. . . 4
β’
(((ACSβπ΅)
β (Mooreβπ« π΅) β§ {π β π« π΅ β£ (0gβπΊ) β π } β (ACSβπ΅) β§ {π β π« π΅ β£ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π } β (ACSβπ΅)) β ({π β π« π΅ β£ (0gβπΊ) β π } β© {π β π« π΅ β£ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π }) β (ACSβπ΅)) |
26 | 16, 19, 24, 25 | syl3anc 1372 |
. . 3
β’ (πΊ β Mnd β ({π β π« π΅ β£
(0gβπΊ)
β π } β© {π β π« π΅ β£ βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π }) β (ACSβπ΅)) |
27 | 13, 26 | eqeltrrid 2839 |
. 2
β’ (πΊ β Mnd β {π β π« π΅ β£
((0gβπΊ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπΊ)π¦) β π )} β (ACSβπ΅)) |
28 | 12, 27 | eqeltrd 2834 |
1
β’ (πΊ β Mnd β
(SubMndβπΊ) β
(ACSβπ΅)) |