Step | Hyp | Ref
| Expression |
1 | | eqidd 2734 |
. 2
β’ (π β LMod β
(Scalarβπ) =
(Scalarβπ)) |
2 | | eqidd 2734 |
. 2
β’ (π β LMod β
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ))) |
3 | | eqidd 2734 |
. 2
β’ (π β LMod β
(Baseβπ) =
(Baseβπ)) |
4 | | eqidd 2734 |
. 2
β’ (π β LMod β
(+gβπ) =
(+gβπ)) |
5 | | eqidd 2734 |
. 2
β’ (π β LMod β (
Β·π βπ) = ( Β·π
βπ)) |
6 | | lss0cl.s |
. . 3
β’ π = (LSubSpβπ) |
7 | 6 | a1i 11 |
. 2
β’ (π β LMod β π = (LSubSpβπ)) |
8 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
9 | | lss0cl.z |
. . . 4
β’ 0 =
(0gβπ) |
10 | 8, 9 | lmod0vcl 20366 |
. . 3
β’ (π β LMod β 0 β
(Baseβπ)) |
11 | 10 | snssd 4770 |
. 2
β’ (π β LMod β { 0 } β
(Baseβπ)) |
12 | 9 | fvexi 6857 |
. . . 4
β’ 0 β
V |
13 | 12 | snnz 4738 |
. . 3
β’ { 0 } β
β
|
14 | 13 | a1i 11 |
. 2
β’ (π β LMod β { 0 } β
β
) |
15 | | simpr2 1196 |
. . . . . . . 8
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β { 0 } β§ π β { 0 })) β π β { 0 }) |
16 | | elsni 4604 |
. . . . . . . 8
β’ (π β { 0 } β π = 0 ) |
17 | 15, 16 | syl 17 |
. . . . . . 7
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β { 0 } β§ π β { 0 })) β π = 0 ) |
18 | 17 | oveq2d 7374 |
. . . . . 6
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β { 0 } β§ π β { 0 })) β (π₯(
Β·π βπ)π) = (π₯( Β·π
βπ) 0
)) |
19 | | eqid 2733 |
. . . . . . . 8
β’
(Scalarβπ) =
(Scalarβπ) |
20 | | eqid 2733 |
. . . . . . . 8
β’ (
Β·π βπ) = ( Β·π
βπ) |
21 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
22 | 19, 20, 21, 9 | lmodvs0 20371 |
. . . . . . 7
β’ ((π β LMod β§ π₯ β
(Baseβ(Scalarβπ))) β (π₯( Β·π
βπ) 0 ) = 0
) |
23 | 22 | 3ad2antr1 1189 |
. . . . . 6
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β { 0 } β§ π β { 0 })) β (π₯(
Β·π βπ) 0 ) = 0 ) |
24 | 18, 23 | eqtrd 2773 |
. . . . 5
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β { 0 } β§ π β { 0 })) β (π₯(
Β·π βπ)π) = 0 ) |
25 | | simpr3 1197 |
. . . . . 6
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β { 0 } β§ π β { 0 })) β π β { 0 }) |
26 | | elsni 4604 |
. . . . . 6
β’ (π β { 0 } β π = 0 ) |
27 | 25, 26 | syl 17 |
. . . . 5
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β { 0 } β§ π β { 0 })) β π = 0 ) |
28 | 24, 27 | oveq12d 7376 |
. . . 4
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β { 0 } β§ π β { 0 })) β ((π₯(
Β·π βπ)π)(+gβπ)π) = ( 0 (+gβπ) 0 )) |
29 | | eqid 2733 |
. . . . . . 7
β’
(+gβπ) = (+gβπ) |
30 | 8, 29, 9 | lmod0vlid 20367 |
. . . . . 6
β’ ((π β LMod β§ 0 β
(Baseβπ)) β (
0
(+gβπ)
0 ) =
0
) |
31 | 10, 30 | mpdan 686 |
. . . . 5
β’ (π β LMod β ( 0
(+gβπ)
0 ) =
0
) |
32 | 31 | adantr 482 |
. . . 4
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β { 0 } β§ π β { 0 })) β ( 0
(+gβπ)
0 ) =
0
) |
33 | 28, 32 | eqtrd 2773 |
. . 3
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β { 0 } β§ π β { 0 })) β ((π₯(
Β·π βπ)π)(+gβπ)π) = 0 ) |
34 | | ovex 7391 |
. . . 4
β’ ((π₯(
Β·π βπ)π)(+gβπ)π) β V |
35 | 34 | elsn 4602 |
. . 3
β’ (((π₯(
Β·π βπ)π)(+gβπ)π) β { 0 } β ((π₯(
Β·π βπ)π)(+gβπ)π) = 0 ) |
36 | 33, 35 | sylibr 233 |
. 2
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β { 0 } β§ π β { 0 })) β ((π₯(
Β·π βπ)π)(+gβπ)π) β { 0 }) |
37 | 1, 2, 3, 4, 5, 7, 11, 14, 36 | islssd 20411 |
1
β’ (π β LMod β { 0 } β
π) |