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 lspsnel5 φ 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