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

Metamath Proof Explorer

Theorem lspindp1

Proof