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 = ( Base ` W )
lshpnelb.n
|- N = ( LSpan ` W )
lshpnelb.p
|- .(+) = ( LSSum ` W )
lshpnelb.h
|- H = ( LSHyp ` W )
lshpnelb.w
|- ( ph -> W e. LVec )
lshpnelb.u
|- ( ph -> U e. H )
lshpnelb.x
|- ( ph -> X e. V )
Assertion lshpnelb
|- ( ph -> ( -. X e. U <-> ( U .(+) ( N ` { X } ) ) = V ) )

Proof

Step Hyp Ref Expression
1 lshpnelb.v
 |-  V = ( Base ` W )
2 lshpnelb.n
 |-  N = ( LSpan ` W )
3 lshpnelb.p
 |-  .(+) = ( LSSum ` W )
4 lshpnelb.h
 |-  H = ( LSHyp ` W )
5 lshpnelb.w
 |-  ( ph -> W e. LVec )
6 lshpnelb.u
 |-  ( ph -> U e. H )
7 lshpnelb.x
 |-  ( ph -> X e. V )
8 eqid
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
9 lveclmod
 |-  ( W e. LVec -> W e. LMod )
10 5 9 syl
 |-  ( ph -> W e. LMod )
11 1 2 8 3 4 10 islshpsm
 |-  ( ph -> ( U e. H <-> ( U e. ( LSubSp ` W ) /\ U =/= V /\ E. v e. V ( U .(+) ( N ` { v } ) ) = V ) ) )
12 6 11 mpbid
 |-  ( ph -> ( U e. ( LSubSp ` W ) /\ U =/= V /\ E. v e. V ( U .(+) ( N ` { v } ) ) = V ) )
13 12 simp3d
 |-  ( ph -> E. v e. V ( U .(+) ( N ` { v } ) ) = V )
14 13 adantr
 |-  ( ( ph /\ -. X e. U ) -> E. v e. V ( U .(+) ( N ` { v } ) ) = V )
15 simp1l
 |-  ( ( ( ph /\ -. X e. U ) /\ v e. V /\ ( U .(+) ( N ` { v } ) ) = V ) -> ph )
16 simp2
 |-  ( ( ( ph /\ -. X e. U ) /\ v e. V /\ ( U .(+) ( N ` { v } ) ) = V ) -> v e. V )
17 8 lsssssubg
 |-  ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
18 10 17 syl
 |-  ( ph -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
19 8 4 10 6 lshplss
 |-  ( ph -> U e. ( LSubSp ` W ) )
20 18 19 sseldd
 |-  ( ph -> U e. ( SubGrp ` W ) )
21 1 8 2 lspsncl
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
22 10 7 21 syl2anc
 |-  ( ph -> ( N ` { X } ) e. ( LSubSp ` W ) )
23 18 22 sseldd
 |-  ( ph -> ( N ` { X } ) e. ( SubGrp ` W ) )
24 3 lsmub1
 |-  ( ( U e. ( SubGrp ` W ) /\ ( N ` { X } ) e. ( SubGrp ` W ) ) -> U C_ ( U .(+) ( N ` { X } ) ) )
25 20 23 24 syl2anc
 |-  ( ph -> U C_ ( U .(+) ( N ` { X } ) ) )
26 25 adantr
 |-  ( ( ph /\ -. X e. U ) -> U C_ ( U .(+) ( N ` { X } ) ) )
27 3 lsmub2
 |-  ( ( U e. ( SubGrp ` W ) /\ ( N ` { X } ) e. ( SubGrp ` W ) ) -> ( N ` { X } ) C_ ( U .(+) ( N ` { X } ) ) )
28 20 23 27 syl2anc
 |-  ( ph -> ( N ` { X } ) C_ ( U .(+) ( N ` { X } ) ) )
29 1 2 lspsnid
 |-  ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )
30 10 7 29 syl2anc
 |-  ( ph -> X e. ( N ` { X } ) )
31 28 30 sseldd
 |-  ( ph -> X e. ( U .(+) ( N ` { X } ) ) )
32 nelne1
 |-  ( ( X e. ( U .(+) ( N ` { X } ) ) /\ -. X e. U ) -> ( U .(+) ( N ` { X } ) ) =/= U )
33 31 32 sylan
 |-  ( ( ph /\ -. X e. U ) -> ( U .(+) ( N ` { X } ) ) =/= U )
34 33 necomd
 |-  ( ( ph /\ -. X e. U ) -> U =/= ( U .(+) ( N ` { X } ) ) )
35 df-pss
 |-  ( U C. ( U .(+) ( N ` { X } ) ) <-> ( U C_ ( U .(+) ( N ` { X } ) ) /\ U =/= ( U .(+) ( N ` { X } ) ) ) )
36 26 34 35 sylanbrc
 |-  ( ( ph /\ -. X e. U ) -> U C. ( U .(+) ( N ` { X } ) ) )
37 36 3ad2ant1
 |-  ( ( ( ph /\ -. X e. U ) /\ v e. V /\ ( U .(+) ( N ` { v } ) ) = V ) -> U C. ( U .(+) ( N ` { X } ) ) )
38 8 3 lsmcl
 |-  ( ( W e. LMod /\ U e. ( LSubSp ` W ) /\ ( N ` { X } ) e. ( LSubSp ` W ) ) -> ( U .(+) ( N ` { X } ) ) e. ( LSubSp ` W ) )
39 10 19 22 38 syl3anc
 |-  ( ph -> ( U .(+) ( N ` { X } ) ) e. ( LSubSp ` W ) )
40 1 8 lssss
 |-  ( ( U .(+) ( N ` { X } ) ) e. ( LSubSp ` W ) -> ( U .(+) ( N ` { X } ) ) C_ V )
41 39 40 syl
 |-  ( ph -> ( U .(+) ( N ` { X } ) ) C_ V )
42 41 adantr
 |-  ( ( ph /\ ( U .(+) ( N ` { v } ) ) = V ) -> ( U .(+) ( N ` { X } ) ) C_ V )
43 simpr
 |-  ( ( ph /\ ( U .(+) ( N ` { v } ) ) = V ) -> ( U .(+) ( N ` { v } ) ) = V )
44 42 43 sseqtrrd
 |-  ( ( ph /\ ( U .(+) ( N ` { v } ) ) = V ) -> ( U .(+) ( N ` { X } ) ) C_ ( U .(+) ( N ` { v } ) ) )
45 44 adantlr
 |-  ( ( ( ph /\ -. X e. U ) /\ ( U .(+) ( N ` { v } ) ) = V ) -> ( U .(+) ( N ` { X } ) ) C_ ( U .(+) ( N ` { v } ) ) )
46 45 3adant2
 |-  ( ( ( ph /\ -. X e. U ) /\ v e. V /\ ( U .(+) ( N ` { v } ) ) = V ) -> ( U .(+) ( N ` { X } ) ) C_ ( U .(+) ( N ` { v } ) ) )
47 5 adantr
 |-  ( ( ph /\ v e. V ) -> W e. LVec )
48 19 adantr
 |-  ( ( ph /\ v e. V ) -> U e. ( LSubSp ` W ) )
49 39 adantr
 |-  ( ( ph /\ v e. V ) -> ( U .(+) ( N ` { X } ) ) e. ( LSubSp ` W ) )
50 simpr
 |-  ( ( ph /\ v e. V ) -> v e. V )
51 1 8 2 3 47 48 49 50 lsmcv
 |-  ( ( ( ph /\ v e. V ) /\ U C. ( U .(+) ( N ` { X } ) ) /\ ( U .(+) ( N ` { X } ) ) C_ ( U .(+) ( N ` { v } ) ) ) -> ( U .(+) ( N ` { X } ) ) = ( U .(+) ( N ` { v } ) ) )
52 15 16 37 46 51 syl211anc
 |-  ( ( ( ph /\ -. X e. U ) /\ v e. V /\ ( U .(+) ( N ` { v } ) ) = V ) -> ( U .(+) ( N ` { X } ) ) = ( U .(+) ( N ` { v } ) ) )
53 simp3
 |-  ( ( ( ph /\ -. X e. U ) /\ v e. V /\ ( U .(+) ( N ` { v } ) ) = V ) -> ( U .(+) ( N ` { v } ) ) = V )
54 52 53 eqtrd
 |-  ( ( ( ph /\ -. X e. U ) /\ v e. V /\ ( U .(+) ( N ` { v } ) ) = V ) -> ( U .(+) ( N ` { X } ) ) = V )
55 54 rexlimdv3a
 |-  ( ( ph /\ -. X e. U ) -> ( E. v e. V ( U .(+) ( N ` { v } ) ) = V -> ( U .(+) ( N ` { X } ) ) = V ) )
56 14 55 mpd
 |-  ( ( ph /\ -. X e. U ) -> ( U .(+) ( N ` { X } ) ) = V )
57 10 adantr
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> W e. LMod )
58 6 adantr
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> U e. H )
59 7 adantr
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> X e. V )
60 simpr
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> ( U .(+) ( N ` { X } ) ) = V )
61 1 2 3 4 57 58 59 60 lshpnel
 |-  ( ( ph /\ ( U .(+) ( N ` { X } ) ) = V ) -> -. X e. U )
62 56 61 impbida
 |-  ( ph -> ( -. X e. U <-> ( U .(+) ( N ` { X } ) ) = V ) )