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