Step | Hyp | Ref
| Expression |
1 | | simpr1 1195 |
. . 3
β’ (((πΊ β Mnd β§ π» β Mnd) β§ (π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π)))) β π β π΅) |
2 | | simpr2 1196 |
. . 3
β’ (((πΊ β Mnd β§ π» β Mnd) β§ (π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π)))) β 0 β π) |
3 | | mndmgm 18568 |
. . . . . . 7
β’ (πΊ β Mnd β πΊ β Mgm) |
4 | | mndmgm 18568 |
. . . . . . 7
β’ (π» β Mnd β π» β Mgm) |
5 | 3, 4 | anim12i 614 |
. . . . . 6
β’ ((πΊ β Mnd β§ π» β Mnd) β (πΊ β Mgm β§ π» β Mgm)) |
6 | 5 | ad2antrr 725 |
. . . . 5
β’ ((((πΊ β Mnd β§ π» β Mnd) β§ (π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π)))) β§ (π β π β§ π β π)) β (πΊ β Mgm β§ π» β Mgm)) |
7 | | 3simpb 1150 |
. . . . . 6
β’ ((π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π))) β (π β π΅ β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π)))) |
8 | 7 | ad2antlr 726 |
. . . . 5
β’ ((((πΊ β Mnd β§ π» β Mnd) β§ (π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π)))) β§ (π β π β§ π β π)) β (π β π΅ β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π)))) |
9 | | simpr 486 |
. . . . 5
β’ ((((πΊ β Mnd β§ π» β Mnd) β§ (π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π)))) β§ (π β π β§ π β π)) β (π β π β§ π β π)) |
10 | | mndissubm.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
11 | | mndissubm.s |
. . . . . 6
β’ π = (Baseβπ») |
12 | 10, 11 | mgmsscl 18507 |
. . . . 5
β’ (((πΊ β Mgm β§ π» β Mgm) β§ (π β π΅ β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π))) β§ (π β π β§ π β π)) β (π(+gβπΊ)π) β π) |
13 | 6, 8, 9, 12 | syl3anc 1372 |
. . . 4
β’ ((((πΊ β Mnd β§ π» β Mnd) β§ (π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π)))) β§ (π β π β§ π β π)) β (π(+gβπΊ)π) β π) |
14 | 13 | ralrimivva 3194 |
. . 3
β’ (((πΊ β Mnd β§ π» β Mnd) β§ (π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π)))) β βπ β π βπ β π (π(+gβπΊ)π) β π) |
15 | | mndissubm.z |
. . . . 5
β’ 0 =
(0gβπΊ) |
16 | | eqid 2733 |
. . . . 5
β’
(+gβπΊ) = (+gβπΊ) |
17 | 10, 15, 16 | issubm 18619 |
. . . 4
β’ (πΊ β Mnd β (π β (SubMndβπΊ) β (π β π΅ β§ 0 β π β§ βπ β π βπ β π (π(+gβπΊ)π) β π))) |
18 | 17 | ad2antrr 725 |
. . 3
β’ (((πΊ β Mnd β§ π» β Mnd) β§ (π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π)))) β (π β (SubMndβπΊ) β (π β π΅ β§ 0 β π β§ βπ β π βπ β π (π(+gβπΊ)π) β π))) |
19 | 1, 2, 14, 18 | mpbir3and 1343 |
. 2
β’ (((πΊ β Mnd β§ π» β Mnd) β§ (π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π)))) β π β (SubMndβπΊ)) |
20 | 19 | ex 414 |
1
β’ ((πΊ β Mnd β§ π» β Mnd) β ((π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π))) β π β (SubMndβπΊ))) |