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

Metamath Proof Explorer

Theorem dvhdimlem

Description: Lemma for dvh2dim and dvh3dim . TODO: make this obsolete and use dvh4dimlem directly? (Contributed by NM, 24-Apr-2015)

Ref Expression
Hypotheses dvh3dim.h ⊢ H = LHyp ⁡ K
dvh3dim.u ⊢ U = DVecH ⁡ K ⁡ W
dvh3dim.v ⊢ V = Base U
dvh3dim.n ⊢ N = LSpan ⁡ U
dvh3dim.k ⊢ φ → K ∈ HL ∧ W ∈ H
dvh3dim.x ⊢ φ → X ∈ V
dvhdim.y ⊢ φ → Y ∈ V
dvhdim.o ⊢ 0 ˙ = 0 U
dvhdim.x ⊢ φ → X ≠ 0 ˙
dvhdimlem.y ⊢ φ → Y ≠ 0 ˙
Assertion dvhdimlem ⊢ φ → ∃ z ∈ V ¬ z ∈ N ⁡ X Y

Proof

Step Hyp Ref Expression
1 dvh3dim.h ⊢ H = LHyp ⁡ K
2 dvh3dim.u ⊢ U = DVecH ⁡ K ⁡ W
3 dvh3dim.v ⊢ V = Base U
4 dvh3dim.n ⊢ N = LSpan ⁡ U
5 dvh3dim.k ⊢ φ → K ∈ HL ∧ W ∈ H
6 dvh3dim.x ⊢ φ → X ∈ V
7 dvhdim.y ⊢ φ → Y ∈ V
8 dvhdim.o ⊢ 0 ˙ = 0 U
9 dvhdim.x ⊢ φ → X ≠ 0 ˙
10 dvhdimlem.y ⊢ φ → Y ≠ 0 ˙
11 1 2 3 4 5 6 7 7 8 9 10 10 dvh4dimlem ⊢ φ → ∃ z ∈ V ¬ z ∈ N ⁡ X Y Y
12 1 2 5 dvhlmod ⊢ φ → U ∈ LMod
13 df-tp ⊢ X Y Y = X Y ∪ Y
14 prssi ⊢ X ∈ V ∧ Y ∈ V → X Y ⊆ V
15 6 7 14 syl2anc ⊢ φ → X Y ⊆ V
16 7 snssd ⊢ φ → Y ⊆ V
17 15 16 unssd ⊢ φ → X Y ∪ Y ⊆ V
18 13 17 eqsstrid ⊢ φ → X Y Y ⊆ V
19 ssun1 ⊢ X Y ⊆ X Y ∪ Y
20 19 13 sseqtrri ⊢ X Y ⊆ X Y Y
21 20 a1i ⊢ φ → X Y ⊆ X Y Y
22 3 4 lspss ⊢ U ∈ LMod ∧ X Y Y ⊆ V ∧ X Y ⊆ X Y Y → N ⁡ X Y ⊆ N ⁡ X Y Y
23 12 18 21 22 syl3anc ⊢ φ → N ⁡ X Y ⊆ N ⁡ X Y Y
24 23 ssneld ⊢ φ → ¬ z ∈ N ⁡ X Y Y → ¬ z ∈ N ⁡ X Y
25 24 reximdv ⊢ φ → ∃ z ∈ V ¬ z ∈ N ⁡ X Y Y → ∃ z ∈ V ¬ z ∈ N ⁡ X Y
26 11 25 mpd ⊢ φ → ∃ z ∈ V ¬ z ∈ N ⁡ X Y