Metamath Proof Explorer


Theorem lshpnelb

Description: The subspace sum of a hyperplane and the span of an element equals the vector space iff the element is not in the hyperplane. (Contributed by NM, 2-Oct-2014)

Ref Expression
Hypotheses lshpnelb.v V=BaseW
lshpnelb.n N=LSpanW
lshpnelb.p ˙=LSSumW
lshpnelb.h H=LSHypW
lshpnelb.w φWLVec
lshpnelb.u φUH
lshpnelb.x φXV
Assertion lshpnelb φ¬XUU˙NX=V

Proof

Step Hyp Ref Expression
1 lshpnelb.v V=BaseW
2 lshpnelb.n N=LSpanW
3 lshpnelb.p ˙=LSSumW
4 lshpnelb.h H=LSHypW
5 lshpnelb.w φWLVec
6 lshpnelb.u φUH
7 lshpnelb.x φXV
8 eqid LSubSpW=LSubSpW
9 lveclmod WLVecWLMod
10 5 9 syl φWLMod
11 1 2 8 3 4 10 islshpsm φUHULSubSpWUVvVU˙Nv=V
12 6 11 mpbid φULSubSpWUVvVU˙Nv=V
13 12 simp3d φvVU˙Nv=V
14 13 adantr φ¬XUvVU˙Nv=V
15 simp1l φ¬XUvVU˙Nv=Vφ
16 simp2 φ¬XUvVU˙Nv=VvV
17 8 lsssssubg WLModLSubSpWSubGrpW
18 10 17 syl φLSubSpWSubGrpW
19 8 4 10 6 lshplss φULSubSpW
20 18 19 sseldd φUSubGrpW
21 1 8 2 lspsncl WLModXVNXLSubSpW
22 10 7 21 syl2anc φNXLSubSpW
23 18 22 sseldd φNXSubGrpW
24 3 lsmub1 USubGrpWNXSubGrpWUU˙NX
25 20 23 24 syl2anc φUU˙NX
26 25 adantr φ¬XUUU˙NX
27 3 lsmub2 USubGrpWNXSubGrpWNXU˙NX
28 20 23 27 syl2anc φNXU˙NX
29 1 2 lspsnid WLModXVXNX
30 10 7 29 syl2anc φXNX
31 28 30 sseldd φXU˙NX
32 nelne1 XU˙NX¬XUU˙NXU
33 31 32 sylan φ¬XUU˙NXU
34 33 necomd φ¬XUUU˙NX
35 df-pss UU˙NXUU˙NXUU˙NX
36 26 34 35 sylanbrc φ¬XUUU˙NX
37 36 3ad2ant1 φ¬XUvVU˙Nv=VUU˙NX
38 8 3 lsmcl WLModULSubSpWNXLSubSpWU˙NXLSubSpW
39 10 19 22 38 syl3anc φU˙NXLSubSpW
40 1 8 lssss U˙NXLSubSpWU˙NXV
41 39 40 syl φU˙NXV
42 41 adantr φU˙Nv=VU˙NXV
43 simpr φU˙Nv=VU˙Nv=V
44 42 43 sseqtrrd φU˙Nv=VU˙NXU˙Nv
45 44 adantlr φ¬XUU˙Nv=VU˙NXU˙Nv
46 45 3adant2 φ¬XUvVU˙Nv=VU˙NXU˙Nv
47 5 adantr φvVWLVec
48 19 adantr φvVULSubSpW
49 39 adantr φvVU˙NXLSubSpW
50 simpr φvVvV
51 1 8 2 3 47 48 49 50 lsmcv φvVUU˙NXU˙NXU˙NvU˙NX=U˙Nv
52 15 16 37 46 51 syl211anc φ¬XUvVU˙Nv=VU˙NX=U˙Nv
53 simp3 φ¬XUvVU˙Nv=VU˙Nv=V
54 52 53 eqtrd φ¬XUvVU˙Nv=VU˙NX=V
55 54 rexlimdv3a φ¬XUvVU˙Nv=VU˙NX=V
56 14 55 mpd φ¬XUU˙NX=V
57 10 adantr φU˙NX=VWLMod
58 6 adantr φU˙NX=VUH
59 7 adantr φU˙NX=VXV
60 simpr φU˙NX=VU˙NX=V
61 1 2 3 4 57 58 59 60 lshpnel φU˙NX=V¬XU
62 56 61 impbida φ¬XUU˙NX=V