Theorem lspindp4

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

	Ref	Expression
Hypotheses	lspindp3.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspindp3.p	⊢ + = ( +g ‘ 𝑊 )
	lspindp4.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspindp4.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lspindp4.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspindp4.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	lspindp4.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
	lspindp4.e	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
Assertion	lspindp4	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , ( 𝑋 + 𝑌 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		lspindp3.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspindp3.p	⊢ + = ( +g ‘ 𝑊 )
3		lspindp4.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lspindp4.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
5		lspindp4.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6		lspindp4.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7		lspindp4.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
8		lspindp4.e	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
9	1 2 3 4 5 6	lspprabs	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , ( 𝑋 + 𝑌 ) } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
10	8 9	neleqtrrd	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , ( 𝑋 + 𝑌 ) } ) )