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

Metamath Proof Explorer

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

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 lspindp2.x ⊢ φ → X ∈ V
6 lspindp2.y ⊢ φ → Y ∈ V ∖ 0 ˙
7 lspindp2.z ⊢ φ → Z ∈ V
8 lspindp2.q ⊢ φ → N ⁡ X ≠ N ⁡ Y
9 lspindp2.e ⊢ φ → ¬ Z ∈ N ⁡ X Y
10 8 necomd ⊢ φ → N ⁡ Y ≠ N ⁡ X
11 prcom ⊢ X Y = Y X
12 11 fveq2i ⊢ N ⁡ X Y = N ⁡ Y X
13 12 eleq2i ⊢ Z ∈ N ⁡ X Y ↔ Z ∈ N ⁡ Y X
14 9 13 sylnib ⊢ φ → ¬ Z ∈ N ⁡ Y X
15 1 2 3 4 6 5 7 10 14 lspindp1 ⊢ φ → N ⁡ Z ≠ N ⁡ X ∧ ¬ Y ∈ N ⁡ Z X