Step | Hyp | Ref
| Expression |
1 | | lspsneleq.y |
. 2
β’ (π β π β (πβ{π})) |
2 | | lspsneleq.w |
. . . . 5
β’ (π β π β LVec) |
3 | | lveclmod 20582 |
. . . . 5
β’ (π β LVec β π β LMod) |
4 | 2, 3 | syl 17 |
. . . 4
β’ (π β π β LMod) |
5 | | lspsneleq.x |
. . . 4
β’ (π β π β π) |
6 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
7 | | eqid 2733 |
. . . . 5
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
8 | | lspsneleq.v |
. . . . 5
β’ π = (Baseβπ) |
9 | | eqid 2733 |
. . . . 5
β’ (
Β·π βπ) = ( Β·π
βπ) |
10 | | lspsneleq.n |
. . . . 5
β’ π = (LSpanβπ) |
11 | 6, 7, 8, 9, 10 | lspsnel 20479 |
. . . 4
β’ ((π β LMod β§ π β π) β (π β (πβ{π}) β βπ β (Baseβ(Scalarβπ))π = (π( Β·π
βπ)π))) |
12 | 4, 5, 11 | syl2anc 585 |
. . 3
β’ (π β (π β (πβ{π}) β βπ β (Baseβ(Scalarβπ))π = (π( Β·π
βπ)π))) |
13 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β π = (π( Β·π
βπ)π)) |
14 | 13 | sneqd 4599 |
. . . . . 6
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β {π} = {(π( Β·π
βπ)π)}) |
15 | 14 | fveq2d 6847 |
. . . . 5
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β (πβ{π}) = (πβ{(π( Β·π
βπ)π)})) |
16 | 2 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β π β LVec) |
17 | | simplr 768 |
. . . . . 6
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β π β (Baseβ(Scalarβπ))) |
18 | | lspsneleq.z |
. . . . . . . 8
β’ (π β π β 0 ) |
19 | 18 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β π β 0 ) |
20 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β§ π = (0gβ(Scalarβπ))) β π = (π( Β·π
βπ)π)) |
21 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β§ π = (0gβ(Scalarβπ))) β π = (0gβ(Scalarβπ))) |
22 | 21 | oveq1d 7373 |
. . . . . . . . . 10
β’ ((((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β§ π = (0gβ(Scalarβπ))) β (π( Β·π
βπ)π) =
((0gβ(Scalarβπ))( Β·π
βπ)π)) |
23 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
24 | | lspsneleq.o |
. . . . . . . . . . . . 13
β’ 0 =
(0gβπ) |
25 | 8, 6, 9, 23, 24 | lmod0vs 20370 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π β π) β
((0gβ(Scalarβπ))( Β·π
βπ)π) = 0 ) |
26 | 4, 5, 25 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β
((0gβ(Scalarβπ))( Β·π
βπ)π) = 0 ) |
27 | 26 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β§ π = (0gβ(Scalarβπ))) β
((0gβ(Scalarβπ))( Β·π
βπ)π) = 0 ) |
28 | 20, 22, 27 | 3eqtrd 2777 |
. . . . . . . . 9
β’ ((((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β§ π = (0gβ(Scalarβπ))) β π = 0 ) |
29 | 28 | ex 414 |
. . . . . . . 8
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β (π = (0gβ(Scalarβπ)) β π = 0 )) |
30 | 29 | necon3d 2961 |
. . . . . . 7
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β (π β 0 β π β
(0gβ(Scalarβπ)))) |
31 | 19, 30 | mpd 15 |
. . . . . 6
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β π β
(0gβ(Scalarβπ))) |
32 | 5 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β π β π) |
33 | 8, 6, 9, 7, 23, 10 | lspsnvs 20591 |
. . . . . 6
β’ ((π β LVec β§ (π β
(Baseβ(Scalarβπ)) β§ π β
(0gβ(Scalarβπ))) β§ π β π) β (πβ{(π( Β·π
βπ)π)}) = (πβ{π})) |
34 | 16, 17, 31, 32, 33 | syl121anc 1376 |
. . . . 5
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β (πβ{(π( Β·π
βπ)π)}) = (πβ{π})) |
35 | 15, 34 | eqtrd 2773 |
. . . 4
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ π = (π( Β·π
βπ)π)) β (πβ{π}) = (πβ{π})) |
36 | 35 | rexlimdva2 3151 |
. . 3
β’ (π β (βπ β (Baseβ(Scalarβπ))π = (π( Β·π
βπ)π) β (πβ{π}) = (πβ{π}))) |
37 | 12, 36 | sylbid 239 |
. 2
β’ (π β (π β (πβ{π}) β (πβ{π}) = (πβ{π}))) |
38 | 1, 37 | mpd 15 |
1
β’ (π β (πβ{π}) = (πβ{π})) |