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

Metamath Proof Explorer

Theorem lspexchn1

Description: Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch to see if this will shorten proofs. (Contributed by NM, 20-May-2015)

Ref Expression
Hypotheses lspexchn1.v ⊢ V = Base W
lspexchn1.n ⊢ N = LSpan ⁡ W
lspexchn1.w ⊢ φ → W ∈ LVec
lspexchn1.x ⊢ φ → X ∈ V
lspexchn1.y ⊢ φ → Y ∈ V
lspexchn1.z ⊢ φ → Z ∈ V
lspexchn1.q ⊢ φ → ¬ Y ∈ N ⁡ Z
lspexchn1.e ⊢ φ → ¬ X ∈ N ⁡ Y Z
Assertion lspexchn1 ⊢ φ → ¬ Y ∈ N ⁡ X Z

Proof

Step Hyp Ref Expression
1 lspexchn1.v ⊢ V = Base W
2 lspexchn1.n ⊢ N = LSpan ⁡ W
3 lspexchn1.w ⊢ φ → W ∈ LVec
4 lspexchn1.x ⊢ φ → X ∈ V
5 lspexchn1.y ⊢ φ → Y ∈ V
6 lspexchn1.z ⊢ φ → Z ∈ V
7 lspexchn1.q ⊢ φ → ¬ Y ∈ N ⁡ Z
8 lspexchn1.e ⊢ φ → ¬ X ∈ N ⁡ Y Z
9 eqid ⊢ 0 W = 0 W
10 3 adantr ⊢ φ ∧ Y ∈ N ⁡ X Z → W ∈ LVec
11 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
12 lveclmod ⊢ W ∈ LVec → W ∈ LMod
13 3 12 syl ⊢ φ → W ∈ LMod
14 1 11 2 lspsncl ⊢ W ∈ LMod ∧ Z ∈ V → N ⁡ Z ∈ LSubSp ⁡ W
15 13 6 14 syl2anc ⊢ φ → N ⁡ Z ∈ LSubSp ⁡ W
16 9 11 13 15 5 7 lssneln0 ⊢ φ → Y ∈ V ∖ 0 W
17 16 adantr ⊢ φ ∧ Y ∈ N ⁡ X Z → Y ∈ V ∖ 0 W
18 4 adantr ⊢ φ ∧ Y ∈ N ⁡ X Z → X ∈ V
19 6 adantr ⊢ φ ∧ Y ∈ N ⁡ X Z → Z ∈ V
20 1 2 13 5 6 7 lspsnne2 ⊢ φ → N ⁡ Y ≠ N ⁡ Z
21 20 adantr ⊢ φ ∧ Y ∈ N ⁡ X Z → N ⁡ Y ≠ N ⁡ Z
22 simpr ⊢ φ ∧ Y ∈ N ⁡ X Z → Y ∈ N ⁡ X Z
23 1 9 2 10 17 18 19 21 22 lspexch ⊢ φ ∧ Y ∈ N ⁡ X Z → X ∈ N ⁡ Y Z
24 8 23 mtand ⊢ φ → ¬ Y ∈ N ⁡ X Z