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 ) } ) )