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

Metamath Proof Explorer

Theorem lspindp2

Description: Alternate way to say 3 vectors are mutually independent (rotate right). (Contributed by NM, 12-Apr-2015)

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

Proof

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