Theorem lspindp3

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

	Ref	Expression
Hypotheses	lspindp3.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspindp3.p	⊢ + = ( +g ‘ 𝑊 )
	lspindp3.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lspindp3.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspindp3.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lspindp3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspindp3.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
	lspindp3.e	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion	lspindp3	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		lspindp3.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspindp3.p	⊢ + = ( +g ‘ 𝑊 )
3		lspindp3.o	⊢ 0 = ( 0g ‘ 𝑊 )
4		lspindp3.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
5		lspindp3.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		lspindp3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7		lspindp3.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
8		lspindp3.e	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
9	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) → 𝑊 ∈ LVec )
10	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) → 𝑋 ∈ 𝑉 )
11	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
12		simpr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
13	1 2 3 4 9 10 11 12	lspabs2	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
14	13	ex	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
15	14	necon3d	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
16	8 15	mpd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )