Theorem lspindp4

Description: (Partial) independence of 3 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015)

	Ref	Expression
Hypotheses	lspindp3.v	|- V = ( Base ` W )
	lspindp3.p	|- .+ = ( +g ` W )
	lspindp4.n	|- N = ( LSpan ` W )
	lspindp4.w	|- ( ph -> W e. LMod )
	lspindp4.x	|- ( ph -> X e. V )
	lspindp4.y	|- ( ph -> Y e. V )
	lspindp4.z	|- ( ph -> Z e. V )
	lspindp4.e	|- ( ph -> -. Z e. ( N ` { X , Y } ) )
Assertion	lspindp4	|- ( ph -> -. Z e. ( N ` { X , ( X .+ Y ) } ) )

Proof

Step	Hyp	Ref	Expression
1		lspindp3.v	|- V = ( Base ` W )
2		lspindp3.p	|- .+ = ( +g ` W )
3		lspindp4.n	|- N = ( LSpan ` W )
4		lspindp4.w	|- ( ph -> W e. LMod )
5		lspindp4.x	|- ( ph -> X e. V )
6		lspindp4.y	|- ( ph -> Y e. V )
7		lspindp4.z	|- ( ph -> Z e. V )
8		lspindp4.e	|- ( ph -> -. Z e. ( N ` { X , Y } ) )
9	1 2 3 4 5 6	lspprabs	|- ( ph -> ( N ` { X , ( X .+ Y ) } ) = ( N ` { X , Y } ) )
10	8 9	neleqtrrd	|- ( ph -> -. Z e. ( N ` { X , ( X .+ Y ) } ) )