This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ V = Base W
lspindp1.o ⊢ 0 ˙ = 0 W
lspindp1.n ⊢ N = LSpan ⁡ W
lspindp1.w ⊢ φ → W ∈ LVec
lspindp1.y ⊢ φ → X ∈ V ∖ 0 ˙
lspindp1.z ⊢ φ → Y ∈ V
lspindp1.x ⊢ φ → Z ∈ V
lspindp1.q ⊢ φ → N ⁡ X ≠ N ⁡ Y
lspindp1.e ⊢ φ → ¬ Z ∈ N ⁡ X Y
Assertion lspindp2l ⊢ φ → N ⁡ Y ≠ N ⁡ Z ∧ ¬ X ∈ N ⁡ Y Z

Proof

Step Hyp Ref Expression
1 lspindp1.v ⊢ V = Base W
2 lspindp1.o ⊢ 0 ˙ = 0 W
3 lspindp1.n ⊢ N = LSpan ⁡ W
4 lspindp1.w ⊢ φ → W ∈ LVec
5 lspindp1.y ⊢ φ → X ∈ V ∖ 0 ˙
6 lspindp1.z ⊢ φ → Y ∈ V
7 lspindp1.x ⊢ φ → Z ∈ V
8 lspindp1.q ⊢ φ → N ⁡ X ≠ N ⁡ Y
9 lspindp1.e ⊢ φ → ¬ Z ∈ N ⁡ X Y
10 1 2 3 4 5 6 7 8 9 lspindp1 ⊢ φ → N ⁡ Z ≠ N ⁡ Y ∧ ¬ X ∈ N ⁡ Z Y
11 10 simpld ⊢ φ → N ⁡ Z ≠ N ⁡ Y
12 11 necomd ⊢ φ → N ⁡ Y ≠ N ⁡ Z
13 10 simprd ⊢ φ → ¬ X ∈ N ⁡ Z Y
14 prcom ⊢ Z Y = Y Z
15 14 fveq2i ⊢ N ⁡ Z Y = N ⁡ Y Z
16 15 eleq2i ⊢ X ∈ N ⁡ Z Y ↔ X ∈ N ⁡ Y Z
17 13 16 sylnib ⊢ φ → ¬ X ∈ N ⁡ Y Z
18 12 17 jca ⊢ φ → N ⁡ Y ≠ N ⁡ Z ∧ ¬ X ∈ N ⁡ Y Z