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 ⊢ 𝑉 = ( 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 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )