Step | Hyp | Ref
| Expression |
1 | | ssrab2 4038 |
. . 3
β’ {π§ β π΅ β£ π} β π΅ |
2 | 1 | a1i 11 |
. 2
β’ (π β {π§ β π΅ β£ π} β π΅) |
3 | | issubmd.ch |
. . 3
β’ (π§ = 0 β (π β π)) |
4 | | issubmd.m |
. . . 4
β’ (π β π β Mnd) |
5 | | issubmd.b |
. . . . 5
β’ π΅ = (Baseβπ) |
6 | | issubmd.z |
. . . . 5
β’ 0 =
(0gβπ) |
7 | 5, 6 | mndidcl 18576 |
. . . 4
β’ (π β Mnd β 0 β π΅) |
8 | 4, 7 | syl 17 |
. . 3
β’ (π β 0 β π΅) |
9 | | issubmd.cz |
. . 3
β’ (π β π) |
10 | 3, 8, 9 | elrabd 3648 |
. 2
β’ (π β 0 β {π§ β π΅ β£ π}) |
11 | | issubmd.th |
. . . . . 6
β’ (π§ = π₯ β (π β π)) |
12 | 11 | elrab 3646 |
. . . . 5
β’ (π₯ β {π§ β π΅ β£ π} β (π₯ β π΅ β§ π)) |
13 | | issubmd.ta |
. . . . . 6
β’ (π§ = π¦ β (π β π)) |
14 | 13 | elrab 3646 |
. . . . 5
β’ (π¦ β {π§ β π΅ β£ π} β (π¦ β π΅ β§ π)) |
15 | 12, 14 | anbi12i 628 |
. . . 4
β’ ((π₯ β {π§ β π΅ β£ π} β§ π¦ β {π§ β π΅ β£ π}) β ((π₯ β π΅ β§ π) β§ (π¦ β π΅ β§ π))) |
16 | | issubmd.et |
. . . . 5
β’ (π§ = (π₯ + π¦) β (π β π)) |
17 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π) β§ (π¦ β π΅ β§ π))) β π β Mnd) |
18 | | simprll 778 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π) β§ (π¦ β π΅ β§ π))) β π₯ β π΅) |
19 | | simprrl 780 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π) β§ (π¦ β π΅ β§ π))) β π¦ β π΅) |
20 | | issubmd.p |
. . . . . . 7
β’ + =
(+gβπ) |
21 | 5, 20 | mndcl 18569 |
. . . . . 6
β’ ((π β Mnd β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) |
22 | 17, 18, 19, 21 | syl3anc 1372 |
. . . . 5
β’ ((π β§ ((π₯ β π΅ β§ π) β§ (π¦ β π΅ β§ π))) β (π₯ + π¦) β π΅) |
23 | | an4 655 |
. . . . . 6
β’ (((π₯ β π΅ β§ π) β§ (π¦ β π΅ β§ π)) β ((π₯ β π΅ β§ π¦ β π΅) β§ (π β§ π))) |
24 | | issubmd.cp |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π β§ π))) β π) |
25 | 23, 24 | sylan2b 595 |
. . . . 5
β’ ((π β§ ((π₯ β π΅ β§ π) β§ (π¦ β π΅ β§ π))) β π) |
26 | 16, 22, 25 | elrabd 3648 |
. . . 4
β’ ((π β§ ((π₯ β π΅ β§ π) β§ (π¦ β π΅ β§ π))) β (π₯ + π¦) β {π§ β π΅ β£ π}) |
27 | 15, 26 | sylan2b 595 |
. . 3
β’ ((π β§ (π₯ β {π§ β π΅ β£ π} β§ π¦ β {π§ β π΅ β£ π})) β (π₯ + π¦) β {π§ β π΅ β£ π}) |
28 | 27 | ralrimivva 3194 |
. 2
β’ (π β βπ₯ β {π§ β π΅ β£ π}βπ¦ β {π§ β π΅ β£ π} (π₯ + π¦) β {π§ β π΅ β£ π}) |
29 | 5, 6, 20 | issubm 18619 |
. . 3
β’ (π β Mnd β ({π§ β π΅ β£ π} β (SubMndβπ) β ({π§ β π΅ β£ π} β π΅ β§ 0 β {π§ β π΅ β£ π} β§ βπ₯ β {π§ β π΅ β£ π}βπ¦ β {π§ β π΅ β£ π} (π₯ + π¦) β {π§ β π΅ β£ π}))) |
30 | 4, 29 | syl 17 |
. 2
β’ (π β ({π§ β π΅ β£ π} β (SubMndβπ) β ({π§ β π΅ β£ π} β π΅ β§ 0 β {π§ β π΅ β£ π} β§ βπ₯ β {π§ β π΅ β£ π}βπ¦ β {π§ β π΅ β£ π} (π₯ + π¦) β {π§ β π΅ β£ π}))) |
31 | 2, 10, 28, 30 | mpbir3and 1343 |
1
β’ (π β {π§ β π΅ β£ π} β (SubMndβπ)) |