Step |
Hyp |
Ref |
Expression |
1 |
|
lspsnsubn0.v |
|- V = ( Base ` W ) |
2 |
|
lspsnsubn0.o |
|- .0. = ( 0g ` W ) |
3 |
|
lspsnsubn0.m |
|- .- = ( -g ` W ) |
4 |
|
lspsnsubn0.w |
|- ( ph -> W e. LMod ) |
5 |
|
lspsnsubn0.x |
|- ( ph -> X e. V ) |
6 |
|
lspsnsubn0.y |
|- ( ph -> Y e. V ) |
7 |
|
lspsnsubn0.e |
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
8 |
1 2 3
|
lmodsubeq0 |
|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( ( X .- Y ) = .0. <-> X = Y ) ) |
9 |
4 5 6 8
|
syl3anc |
|- ( ph -> ( ( X .- Y ) = .0. <-> X = Y ) ) |
10 |
|
sneq |
|- ( X = Y -> { X } = { Y } ) |
11 |
10
|
fveq2d |
|- ( X = Y -> ( N ` { X } ) = ( N ` { Y } ) ) |
12 |
9 11
|
syl6bi |
|- ( ph -> ( ( X .- Y ) = .0. -> ( N ` { X } ) = ( N ` { Y } ) ) ) |
13 |
12
|
necon3d |
|- ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) -> ( X .- Y ) =/= .0. ) ) |
14 |
7 13
|
mpd |
|- ( ph -> ( X .- Y ) =/= .0. ) |