| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eqid 2728 |
. . . 4
β’
(BaseβπΊ) =
(BaseβπΊ) |
| 2 | | 0subm.z |
. . . 4
β’ 0 =
(0gβπΊ) |
| 3 | 1, 2 | mndidcl 18709 |
. . 3
β’ (πΊ β Mnd β 0 β
(BaseβπΊ)) |
| 4 | 3 | snssd 4813 |
. 2
β’ (πΊ β Mnd β { 0 } β
(BaseβπΊ)) |
| 5 | 2 | fvexi 6911 |
. . . 4
β’ 0 β
V |
| 6 | 5 | snid 4665 |
. . 3
β’ 0 β {
0
} |
| 7 | 6 | a1i 11 |
. 2
β’ (πΊ β Mnd β 0 β {
0
}) |
| 8 | | velsn 4645 |
. . . . 5
β’ (π β { 0 } β π = 0 ) |
| 9 | | velsn 4645 |
. . . . 5
β’ (π β { 0 } β π = 0 ) |
| 10 | 8, 9 | anbi12i 627 |
. . . 4
β’ ((π β { 0 } β§ π β { 0 }) β (π = 0 β§ π = 0 )) |
| 11 | | eqid 2728 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
| 12 | 1, 11, 2 | mndlid 18714 |
. . . . . . 7
β’ ((πΊ β Mnd β§ 0 β
(BaseβπΊ)) β (
0
(+gβπΊ)
0 ) =
0
) |
| 13 | 3, 12 | mpdan 686 |
. . . . . 6
β’ (πΊ β Mnd β ( 0
(+gβπΊ)
0 ) =
0
) |
| 14 | | ovex 7453 |
. . . . . . 7
β’ ( 0
(+gβπΊ)
0 )
β V |
| 15 | 14 | elsn 4644 |
. . . . . 6
β’ (( 0
(+gβπΊ)
0 )
β { 0 } β ( 0
(+gβπΊ)
0 ) =
0
) |
| 16 | 13, 15 | sylibr 233 |
. . . . 5
β’ (πΊ β Mnd β ( 0
(+gβπΊ)
0 )
β { 0 }) |
| 17 | | oveq12 7429 |
. . . . . 6
β’ ((π = 0 β§ π = 0 ) β (π(+gβπΊ)π) = ( 0 (+gβπΊ) 0 )) |
| 18 | 17 | eleq1d 2814 |
. . . . 5
β’ ((π = 0 β§ π = 0 ) β ((π(+gβπΊ)π) β { 0 } β ( 0
(+gβπΊ)
0 )
β { 0 })) |
| 19 | 16, 18 | syl5ibrcom 246 |
. . . 4
β’ (πΊ β Mnd β ((π = 0 β§ π = 0 ) β (π(+gβπΊ)π) β { 0 })) |
| 20 | 10, 19 | biimtrid 241 |
. . 3
β’ (πΊ β Mnd β ((π β { 0 } β§ π β { 0 }) β (π(+gβπΊ)π) β { 0 })) |
| 21 | 20 | ralrimivv 3195 |
. 2
β’ (πΊ β Mnd β βπ β { 0 }βπ β { 0 } (π(+gβπΊ)π) β { 0 }) |
| 22 | 1, 2, 11 | issubm 18755 |
. 2
β’ (πΊ β Mnd β ({ 0 } β
(SubMndβπΊ) β ({
0 }
β (BaseβπΊ)
β§ 0
β { 0 } β§ βπ β { 0 }βπ β { 0 } (π(+gβπΊ)π) β { 0 }))) |
| 23 | 4, 7, 21, 22 | mpbir3and 1340 |
1
β’ (πΊ β Mnd β { 0 } β
(SubMndβπΊ)) |
