Metamath Proof Explorer


Theorem lspindp1

Description: Alternate way to say 3 vectors are mutually independent (swap 1st and 2nd). (Contributed by NM, 11-Apr-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 lspindp1 ( 𝜑 → ( ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ∧ ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) ) )

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 5 eldifad ( 𝜑𝑋𝑉 )
11 1 3 4 7 10 6 9 lspindpi ( 𝜑 → ( ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) ∧ ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
12 11 simprd ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
13 4 adantr ( ( 𝜑𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) ) → 𝑊 ∈ LVec )
14 5 adantr ( ( 𝜑𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
15 7 adantr ( ( 𝜑𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) ) → 𝑍𝑉 )
16 6 adantr ( ( 𝜑𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) ) → 𝑌𝑉 )
17 8 adantr ( ( 𝜑𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
18 simpr ( ( 𝜑𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) )
19 1 2 3 13 14 15 16 17 18 lspexch ( ( 𝜑𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) ) → 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
20 9 19 mtand ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) )
21 12 20 jca ( 𝜑 → ( ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ∧ ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) ) )