This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspindp3

Description: Independence of 2 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015)

Ref Expression
Hypotheses lspindp3.v 
|- V = ( Base ` W )
lspindp3.p 
|- .+ = ( +g ` W )
lspindp3.o 
|- .0. = ( 0g ` W )
lspindp3.n 
|- N = ( LSpan ` W )
lspindp3.w 
|- ( ph -> W e. LVec )
lspindp3.x 
|- ( ph -> X e. V )
lspindp3.y 
|- ( ph -> Y e. ( V \ { .0. } ) )
lspindp3.e 
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
Assertion lspindp3 
|- ( ph -> ( N ` { X } ) =/= ( N ` { ( X .+ Y ) } ) )

Proof

Step Hyp Ref Expression
1 lspindp3.v 
 |-  V = ( Base ` W )
2 lspindp3.p 
 |-  .+ = ( +g ` W )
3 lspindp3.o 
 |-  .0. = ( 0g ` W )
4 lspindp3.n 
 |-  N = ( LSpan ` W )
5 lspindp3.w 
 |-  ( ph -> W e. LVec )
6 lspindp3.x 
 |-  ( ph -> X e. V )
7 lspindp3.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
8 lspindp3.e 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
9 5 adantr 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { ( X .+ Y ) } ) ) -> W e. LVec )
10 6 adantr 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { ( X .+ Y ) } ) ) -> X e. V )
11 7 adantr 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { ( X .+ Y ) } ) ) -> Y e. ( V \ { .0. } ) )
12 simpr 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { ( X .+ Y ) } ) ) -> ( N ` { X } ) = ( N ` { ( X .+ Y ) } ) )
13 1 2 3 4 9 10 11 12 lspabs2 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { ( X .+ Y ) } ) ) -> ( N ` { X } ) = ( N ` { Y } ) )
14 13 ex 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { ( X .+ Y ) } ) -> ( N ` { X } ) = ( N ` { Y } ) ) )
15 14 necon3d 
 |-  ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) -> ( N ` { X } ) =/= ( N ` { ( X .+ Y ) } ) ) )
16 8 15 mpd 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { ( X .+ Y ) } ) )