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