This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspindp2l

Description: Alternate way to say 3 vectors are mutually independent (rotate left). (Contributed by NM, 10-May-2015)

Ref Expression
Hypotheses lspindp1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspindp1.o ⊢ 0 = ( 0g ‘ 𝑊 )
lspindp1.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspindp1.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lspindp1.y ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lspindp1.z ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lspindp1.x ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
lspindp1.q ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
lspindp1.e ⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
Assertion lspindp2l ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) ∧ ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )

Proof

Step Hyp Ref Expression
1 lspindp1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspindp1.o ⊢ 0 = ( 0g ‘ 𝑊 )
3 lspindp1.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspindp1.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 lspindp1.y ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
6 lspindp1.z ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7 lspindp1.x ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
8 lspindp1.q ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
9 lspindp1.e ⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
10 1 2 3 4 5 6 7 8 9 lspindp1 ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ∧ ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) ) )
11 10 simpld ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
12 11 necomd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
13 10 simprd ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) )
14 prcom ⊢ { 𝑍 , 𝑌 } = { 𝑌 , 𝑍 }
15 14 fveq2i ⊢ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) = ( 𝑁 ‘ { 𝑌 , 𝑍 } )
16 15 eleq2i ⊢ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) ↔ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
17 13 16 sylnib ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
18 12 17 jca ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) ∧ ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )