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