| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eqid 2177 |
. . . 4
β’
(BaseβπΊ) =
(BaseβπΊ) |
| 2 | | 0subm.z |
. . . 4
β’ 0 =
(0gβπΊ) |
| 3 | 1, 2 | mndidcl 12831 |
. . 3
β’ (πΊ β Mnd β 0 β
(BaseβπΊ)) |
| 4 | 3 | snssd 3738 |
. 2
β’ (πΊ β Mnd β { 0 } β
(BaseβπΊ)) |
| 5 | | snidg 3622 |
. . 3
β’ ( 0 β
(BaseβπΊ) β 0 β {
0
}) |
| 6 | 3, 5 | syl 14 |
. 2
β’ (πΊ β Mnd β 0 β {
0
}) |
| 7 | | velsn 3610 |
. . . . 5
β’ (π β { 0 } β π = 0 ) |
| 8 | | velsn 3610 |
. . . . 5
β’ (π β { 0 } β π = 0 ) |
| 9 | 7, 8 | anbi12i 460 |
. . . 4
β’ ((π β { 0 } β§ π β { 0 }) β (π = 0 β§ π = 0 )) |
| 10 | | eqid 2177 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
| 11 | 1, 10, 2 | mndlid 12836 |
. . . . . . 7
β’ ((πΊ β Mnd β§ 0 β
(BaseβπΊ)) β (
0
(+gβπΊ)
0 ) =
0
) |
| 12 | 3, 11 | mpdan 421 |
. . . . . 6
β’ (πΊ β Mnd β ( 0
(+gβπΊ)
0 ) =
0
) |
| 13 | 12, 3 | eqeltrd 2254 |
. . . . . . 7
β’ (πΊ β Mnd β ( 0
(+gβπΊ)
0 )
β (BaseβπΊ)) |
| 14 | | elsng 3608 |
. . . . . . 7
β’ (( 0
(+gβπΊ)
0 )
β (BaseβπΊ)
β (( 0 (+gβπΊ) 0 ) β { 0 } β (
0
(+gβπΊ)
0 ) =
0
)) |
| 15 | 13, 14 | syl 14 |
. . . . . 6
β’ (πΊ β Mnd β (( 0
(+gβπΊ)
0 )
β { 0 } β ( 0
(+gβπΊ)
0 ) =
0
)) |
| 16 | 12, 15 | mpbird 167 |
. . . . 5
β’ (πΊ β Mnd β ( 0
(+gβπΊ)
0 )
β { 0 }) |
| 17 | | oveq12 5884 |
. . . . . 6
β’ ((π = 0 β§ π = 0 ) β (π(+gβπΊ)π) = ( 0 (+gβπΊ) 0 )) |
| 18 | 17 | eleq1d 2246 |
. . . . 5
β’ ((π = 0 β§ π = 0 ) β ((π(+gβπΊ)π) β { 0 } β ( 0
(+gβπΊ)
0 )
β { 0 })) |
| 19 | 16, 18 | syl5ibrcom 157 |
. . . 4
β’ (πΊ β Mnd β ((π = 0 β§ π = 0 ) β (π(+gβπΊ)π) β { 0 })) |
| 20 | 9, 19 | biimtrid 152 |
. . 3
β’ (πΊ β Mnd β ((π β { 0 } β§ π β { 0 }) β (π(+gβπΊ)π) β { 0 })) |
| 21 | 20 | ralrimivv 2558 |
. 2
β’ (πΊ β Mnd β βπ β { 0 }βπ β { 0 } (π(+gβπΊ)π) β { 0 }) |
| 22 | 1, 2, 10 | issubm 12863 |
. 2
β’ (πΊ β Mnd β ({ 0 } β
(SubMndβπΊ) β ({
0 }
β (BaseβπΊ)
β§ 0
β { 0 } β§ βπ β { 0 }βπ β { 0 } (π(+gβπΊ)π) β { 0 }))) |
| 23 | 4, 6, 21, 22 | mpbir3and 1180 |
1
β’ (πΊ β Mnd β { 0 } β
(SubMndβπΊ)) |
