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 ) )