Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(BaseβπΊ) =
(BaseβπΊ) |
2 | | 0subm.z |
. . . 4
β’ 0 =
(0gβπΊ) |
3 | 1, 2 | mndidcl 18576 |
. . 3
β’ (πΊ β Mnd β 0 β
(BaseβπΊ)) |
4 | 3 | snssd 4770 |
. 2
β’ (πΊ β Mnd β { 0 } β
(BaseβπΊ)) |
5 | 2 | fvexi 6857 |
. . . 4
β’ 0 β
V |
6 | 5 | snid 4623 |
. . 3
β’ 0 β {
0
} |
7 | 6 | a1i 11 |
. 2
β’ (πΊ β Mnd β 0 β {
0
}) |
8 | | velsn 4603 |
. . . . 5
β’ (π β { 0 } β π = 0 ) |
9 | | velsn 4603 |
. . . . 5
β’ (π β { 0 } β π = 0 ) |
10 | 8, 9 | anbi12i 628 |
. . . 4
β’ ((π β { 0 } β§ π β { 0 }) β (π = 0 β§ π = 0 )) |
11 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
12 | 1, 11, 2 | mndlid 18581 |
. . . . . . 7
β’ ((πΊ β Mnd β§ 0 β
(BaseβπΊ)) β (
0
(+gβπΊ)
0 ) =
0
) |
13 | 3, 12 | mpdan 686 |
. . . . . 6
β’ (πΊ β Mnd β ( 0
(+gβπΊ)
0 ) =
0
) |
14 | | ovex 7391 |
. . . . . . 7
β’ ( 0
(+gβπΊ)
0 )
β V |
15 | 14 | elsn 4602 |
. . . . . 6
β’ (( 0
(+gβπΊ)
0 )
β { 0 } β ( 0
(+gβπΊ)
0 ) =
0
) |
16 | 13, 15 | sylibr 233 |
. . . . 5
β’ (πΊ β Mnd β ( 0
(+gβπΊ)
0 )
β { 0 }) |
17 | | oveq12 7367 |
. . . . . 6
β’ ((π = 0 β§ π = 0 ) β (π(+gβπΊ)π) = ( 0 (+gβπΊ) 0 )) |
18 | 17 | eleq1d 2819 |
. . . . 5
β’ ((π = 0 β§ π = 0 ) β ((π(+gβπΊ)π) β { 0 } β ( 0
(+gβπΊ)
0 )
β { 0 })) |
19 | 16, 18 | syl5ibrcom 247 |
. . . 4
β’ (πΊ β Mnd β ((π = 0 β§ π = 0 ) β (π(+gβπΊ)π) β { 0 })) |
20 | 10, 19 | biimtrid 241 |
. . 3
β’ (πΊ β Mnd β ((π β { 0 } β§ π β { 0 }) β (π(+gβπΊ)π) β { 0 })) |
21 | 20 | ralrimivv 3192 |
. 2
β’ (πΊ β Mnd β βπ β { 0 }βπ β { 0 } (π(+gβπΊ)π) β { 0 }) |
22 | 1, 2, 11 | issubm 18619 |
. 2
β’ (πΊ β Mnd β ({ 0 } β
(SubMndβπΊ) β ({
0 }
β (BaseβπΊ)
β§ 0
β { 0 } β§ βπ β { 0 }βπ β { 0 } (π(+gβπΊ)π) β { 0 }))) |
23 | 4, 7, 21, 22 | mpbir3and 1343 |
1
β’ (πΊ β Mnd β { 0 } β
(SubMndβπΊ)) |