This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lshpnel

Description: A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014)

Ref Expression
Hypotheses lshpnel.v 
|- V = ( Base ` W )
lshpnel.n 
|- N = ( LSpan ` W )
lshpnel.p 
|- .(+) = ( LSSum ` W )
lshpnel.h 
|- H = ( LSHyp ` W )
lshpnel.w 
|- ( ph -> W e. LMod )
lshpnel.u 
|- ( ph -> U e. H )
lshpnel.x 
|- ( ph -> X e. V )
lshpnel.e 
|- ( ph -> ( U .(+) ( N ` { X } ) ) = V )
Assertion lshpnel 
|- ( ph -> -. X e. U )

Proof

Step Hyp Ref Expression
1 lshpnel.v 
 |-  V = ( Base ` W )
2 lshpnel.n 
 |-  N = ( LSpan ` W )
3 lshpnel.p 
 |-  .(+) = ( LSSum ` W )
4 lshpnel.h 
 |-  H = ( LSHyp ` W )
5 lshpnel.w 
 |-  ( ph -> W e. LMod )
6 lshpnel.u 
 |-  ( ph -> U e. H )
7 lshpnel.x 
 |-  ( ph -> X e. V )
8 lshpnel.e 
 |-  ( ph -> ( U .(+) ( N ` { X } ) ) = V )
9 1 4 5 6 lshpne 
 |-  ( ph -> U =/= V )
10 5 adantr 
 |-  ( ( ph /\ X e. U ) -> W e. LMod )
11 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
12 11 lsssssubg 
 |-  ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
13 10 12 syl 
 |-  ( ( ph /\ X e. U ) -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
14 11 4 5 6 lshplss 
 |-  ( ph -> U e. ( LSubSp ` W ) )
15 14 adantr 
 |-  ( ( ph /\ X e. U ) -> U e. ( LSubSp ` W ) )
16 13 15 sseldd 
 |-  ( ( ph /\ X e. U ) -> U e. ( SubGrp ` W ) )
17 7 adantr 
 |-  ( ( ph /\ X e. U ) -> X e. V )
18 1 11 2 lspsncl 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
19 10 17 18 syl2anc 
 |-  ( ( ph /\ X e. U ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
20 13 19 sseldd 
 |-  ( ( ph /\ X e. U ) -> ( N ` { X } ) e. ( SubGrp ` W ) )
21 simpr 
 |-  ( ( ph /\ X e. U ) -> X e. U )
22 11 2 10 15 21 ellspsn5 
 |-  ( ( ph /\ X e. U ) -> ( N ` { X } ) C_ U )
23 3 lsmss2 
 |-  ( ( U e. ( SubGrp ` W ) /\ ( N ` { X } ) e. ( SubGrp ` W ) /\ ( N ` { X } ) C_ U ) -> ( U .(+) ( N ` { X } ) ) = U )
24 16 20 22 23 syl3anc 
 |-  ( ( ph /\ X e. U ) -> ( U .(+) ( N ` { X } ) ) = U )
25 8 adantr 
 |-  ( ( ph /\ X e. U ) -> ( U .(+) ( N ` { X } ) ) = V )
26 24 25 eqtr3d 
 |-  ( ( ph /\ X e. U ) -> U = V )
27 26 ex 
 |-  ( ph -> ( X e. U -> U = V ) )
28 27 necon3ad 
 |-  ( ph -> ( U =/= V -> -. X e. U ) )
29 9 28 mpd 
 |-  ( ph -> -. X e. U )