Metamath Proof Explorer


Theorem lshpdisj

Description: A hyperplane and the span in the hyperplane definition are disjoint. (Contributed by NM, 3-Jul-2014)

Ref Expression
Hypotheses lshpdisj.v V = Base W
lshpdisj.o 0 ˙ = 0 W
lshpdisj.n N = LSpan W
lshpdisj.p ˙ = LSSum W
lshpdisj.h H = LSHyp W
lshpdisj.w φ W LVec
lshpdisj.u φ U H
lshpdisj.x φ X V
lshpdisj.e φ U ˙ N X = V
Assertion lshpdisj φ U N X = 0 ˙

Proof

Step Hyp Ref Expression
1 lshpdisj.v V = Base W
2 lshpdisj.o 0 ˙ = 0 W
3 lshpdisj.n N = LSpan W
4 lshpdisj.p ˙ = LSSum W
5 lshpdisj.h H = LSHyp W
6 lshpdisj.w φ W LVec
7 lshpdisj.u φ U H
8 lshpdisj.x φ X V
9 lshpdisj.e φ U ˙ N X = V
10 lveclmod W LVec W LMod
11 6 10 syl φ W LMod
12 11 adantr φ v U W LMod
13 8 adantr φ v U X V
14 eqid Scalar W = Scalar W
15 eqid Base Scalar W = Base Scalar W
16 eqid W = W
17 14 15 1 16 3 lspsnel W LMod X V v N X k Base Scalar W v = k W X
18 12 13 17 syl2anc φ v U v N X k Base Scalar W v = k W X
19 1 3 4 5 11 7 8 9 lshpnel φ ¬ X U
20 19 ad2antrr φ k Base Scalar W k W X 0 ˙ ¬ X U
21 eqid LSubSp W = LSubSp W
22 6 ad2antrr φ k Base Scalar W k W X 0 ˙ W LVec
23 21 5 11 7 lshplss φ U LSubSp W
24 23 ad2antrr φ k Base Scalar W k W X 0 ˙ U LSubSp W
25 8 ad2antrr φ k Base Scalar W k W X 0 ˙ X V
26 11 adantr φ k Base Scalar W W LMod
27 simpr φ k Base Scalar W k Base Scalar W
28 8 adantr φ k Base Scalar W X V
29 1 16 14 15 3 26 27 28 lspsneli φ k Base Scalar W k W X N X
30 29 adantr φ k Base Scalar W k W X 0 ˙ k W X N X
31 simpr φ k Base Scalar W k W X 0 ˙ k W X 0 ˙
32 1 2 21 3 22 24 25 30 31 lspsnel4 φ k Base Scalar W k W X 0 ˙ X U k W X U
33 20 32 mtbid φ k Base Scalar W k W X 0 ˙ ¬ k W X U
34 33 ex φ k Base Scalar W k W X 0 ˙ ¬ k W X U
35 34 necon4ad φ k Base Scalar W k W X U k W X = 0 ˙
36 eleq1 v = k W X v U k W X U
37 eqeq1 v = k W X v = 0 ˙ k W X = 0 ˙
38 36 37 imbi12d v = k W X v U v = 0 ˙ k W X U k W X = 0 ˙
39 35 38 syl5ibrcom φ k Base Scalar W v = k W X v U v = 0 ˙
40 39 ex φ k Base Scalar W v = k W X v U v = 0 ˙
41 40 com23 φ v = k W X k Base Scalar W v U v = 0 ˙
42 41 com24 φ v U k Base Scalar W v = k W X v = 0 ˙
43 42 imp31 φ v U k Base Scalar W v = k W X v = 0 ˙
44 43 rexlimdva φ v U k Base Scalar W v = k W X v = 0 ˙
45 18 44 sylbid φ v U v N X v = 0 ˙
46 45 expimpd φ v U v N X v = 0 ˙
47 elin v U N X v U v N X
48 velsn v 0 ˙ v = 0 ˙
49 46 47 48 3imtr4g φ v U N X v 0 ˙
50 49 ssrdv φ U N X 0 ˙
51 1 21 3 lspsncl W LMod X V N X LSubSp W
52 11 8 51 syl2anc φ N X LSubSp W
53 21 lssincl W LMod U LSubSp W N X LSubSp W U N X LSubSp W
54 11 23 52 53 syl3anc φ U N X LSubSp W
55 2 21 lss0ss W LMod U N X LSubSp W 0 ˙ U N X
56 11 54 55 syl2anc φ 0 ˙ U N X
57 50 56 eqssd φ U N X = 0 ˙