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 ( 𝜑 → ( ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑋 } ) ) )