Metamath Proof Explorer

Theorem dvh4dimlem

Description: Lemma for dvh4dimN . (Contributed by NM, 22-May-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
dvh4dim.y ⊢ φ → Y ∈ V
dvhdim.z ⊢ φ → Z ∈ V
dvh4dim.o ⊢ 0 ˙ = 0 U
dvh4dim.x ⊢ φ → X ≠ 0 ˙
dvh4dimlem.y ⊢ φ → Y ≠ 0 ˙
dvh4dimlem.z ⊢ φ → Z ≠ 0 ˙
Assertion dvh4dimlem ⊢ φ → ∃ z ∈ V ¬ z ∈ N ⁡ X Y Z

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 dvh4dim.y ⊢ φ → Y ∈ V
8 dvhdim.z ⊢ φ → Z ∈ V
9 dvh4dim.o ⊢ 0 ˙ = 0 U
10 dvh4dim.x ⊢ φ → X ≠ 0 ˙
11 dvh4dimlem.y ⊢ φ → Y ≠ 0 ˙
12 dvh4dimlem.z ⊢ φ → Z ≠ 0 ˙
13 eqid ⊢ LSSum ⁡ U = LSSum ⁡ U
14 eqid ⊢ LSAtoms ⁡ U = LSAtoms ⁡ U
15 1 2 5 dvhlmod ⊢ φ → U ∈ LMod
16 eldifsn ⊢ X ∈ V ∖ 0 ˙ ↔ X ∈ V ∧ X ≠ 0 ˙
17 6 10 16 sylanbrc ⊢ φ → X ∈ V ∖ 0 ˙
18 3 4 9 14 15 17 lsatlspsn ⊢ φ → N ⁡ X ∈ LSAtoms ⁡ U
19 eldifsn ⊢ Y ∈ V ∖ 0 ˙ ↔ Y ∈ V ∧ Y ≠ 0 ˙
20 7 11 19 sylanbrc ⊢ φ → Y ∈ V ∖ 0 ˙
21 3 4 9 14 15 20 lsatlspsn ⊢ φ → N ⁡ Y ∈ LSAtoms ⁡ U
22 eldifsn ⊢ Z ∈ V ∖ 0 ˙ ↔ Z ∈ V ∧ Z ≠ 0 ˙
23 8 12 22 sylanbrc ⊢ φ → Z ∈ V ∖ 0 ˙
24 3 4 9 14 15 23 lsatlspsn ⊢ φ → N ⁡ Z ∈ LSAtoms ⁡ U
25 1 2 13 14 5 18 21 24 dvh4dimat ⊢ φ → ∃ p ∈ LSAtoms ⁡ U ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z
26 15 3ad2ant1 ⊢ φ ∧ p ∈ LSAtoms ⁡ U ∧ ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z → U ∈ LMod
27 simp2 ⊢ φ ∧ p ∈ LSAtoms ⁡ U ∧ ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z → p ∈ LSAtoms ⁡ U
28 3 4 14 islsati ⊢ U ∈ LMod ∧ p ∈ LSAtoms ⁡ U → ∃ z ∈ V p = N ⁡ z
29 26 27 28 syl2anc ⊢ φ ∧ p ∈ LSAtoms ⁡ U ∧ ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z → ∃ z ∈ V p = N ⁡ z
30 simp2 ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → p = N ⁡ z
31 15 3ad2ant1 ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → U ∈ LMod
32 6 3ad2ant1 ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → X ∈ V
33 7 3ad2ant1 ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → Y ∈ V
34 3 4 13 31 32 33 lsmpr ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → N ⁡ X Y = N ⁡ X LSSum ⁡ U N ⁡ Y
35 34 oveq1d ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → N ⁡ X Y LSSum ⁡ U N ⁡ Z = N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z
36 prssi ⊢ X ∈ V ∧ Y ∈ V → X Y ⊆ V
37 6 7 36 syl2anc ⊢ φ → X Y ⊆ V
38 37 3ad2ant1 ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → X Y ⊆ V
39 8 snssd ⊢ φ → Z ⊆ V
40 39 3ad2ant1 ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → Z ⊆ V
41 3 4 13 lsmsp2 ⊢ U ∈ LMod ∧ X Y ⊆ V ∧ Z ⊆ V → N ⁡ X Y LSSum ⁡ U N ⁡ Z = N ⁡ X Y ∪ Z
42 31 38 40 41 syl3anc ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → N ⁡ X Y LSSum ⁡ U N ⁡ Z = N ⁡ X Y ∪ Z
43 35 42 eqtr3d ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z = N ⁡ X Y ∪ Z
44 30 43 sseq12d ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z ↔ N ⁡ z ⊆ N ⁡ X Y ∪ Z
45 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
46 37 39 unssd ⊢ φ → X Y ∪ Z ⊆ V
47 3 45 4 lspcl ⊢ U ∈ LMod ∧ X Y ∪ Z ⊆ V → N ⁡ X Y ∪ Z ∈ LSubSp ⁡ U
48 15 46 47 syl2anc ⊢ φ → N ⁡ X Y ∪ Z ∈ LSubSp ⁡ U
49 48 3ad2ant1 ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → N ⁡ X Y ∪ Z ∈ LSubSp ⁡ U
50 simp3 ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → z ∈ V
51 3 45 4 31 49 50 ellspsn5b ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → z ∈ N ⁡ X Y ∪ Z ↔ N ⁡ z ⊆ N ⁡ X Y ∪ Z
52 44 51 bitr4d ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z ↔ z ∈ N ⁡ X Y ∪ Z
53 df-tp ⊢ X Y Z = X Y ∪ Z
54 53 fveq2i ⊢ N ⁡ X Y Z = N ⁡ X Y ∪ Z
55 54 eleq2i ⊢ z ∈ N ⁡ X Y Z ↔ z ∈ N ⁡ X Y ∪ Z
56 52 55 bitr4di ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z ↔ z ∈ N ⁡ X Y Z
57 56 notbid ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z ↔ ¬ z ∈ N ⁡ X Y Z
58 57 biimpd ⊢ φ ∧ p = N ⁡ z ∧ z ∈ V → ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z → ¬ z ∈ N ⁡ X Y Z
59 58 3exp ⊢ φ → p = N ⁡ z → z ∈ V → ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z → ¬ z ∈ N ⁡ X Y Z
60 59 com24 ⊢ φ → ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z → z ∈ V → p = N ⁡ z → ¬ z ∈ N ⁡ X Y Z
61 60 a1d ⊢ φ → p ∈ LSAtoms ⁡ U → ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z → z ∈ V → p = N ⁡ z → ¬ z ∈ N ⁡ X Y Z
62 61 3imp ⊢ φ ∧ p ∈ LSAtoms ⁡ U ∧ ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z → z ∈ V → p = N ⁡ z → ¬ z ∈ N ⁡ X Y Z
63 62 reximdvai ⊢ φ ∧ p ∈ LSAtoms ⁡ U ∧ ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z → ∃ z ∈ V p = N ⁡ z → ∃ z ∈ V ¬ z ∈ N ⁡ X Y Z
64 29 63 mpd ⊢ φ ∧ p ∈ LSAtoms ⁡ U ∧ ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z → ∃ z ∈ V ¬ z ∈ N ⁡ X Y Z
65 64 rexlimdv3a ⊢ φ → ∃ p ∈ LSAtoms ⁡ U ¬ p ⊆ N ⁡ X LSSum ⁡ U N ⁡ Y LSSum ⁡ U N ⁡ Z → ∃ z ∈ V ¬ z ∈ N ⁡ X Y Z
66 25 65 mpd ⊢ φ → ∃ z ∈ V ¬ z ∈ N ⁡ X Y Z