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

Metamath Proof Explorer

Theorem lshpne

Description: A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014)

Ref Expression
Hypotheses lshpne.v 
|- V = ( Base ` W )
lshpne.h 
|- H = ( LSHyp ` W )
lshpne.w 
|- ( ph -> W e. LMod )
lshpne.u 
|- ( ph -> U e. H )
Assertion lshpne 
|- ( ph -> U =/= V )

Proof

Step Hyp Ref Expression
1 lshpne.v 
 |-  V = ( Base ` W )
2 lshpne.h 
 |-  H = ( LSHyp ` W )
3 lshpne.w 
 |-  ( ph -> W e. LMod )
4 lshpne.u 
 |-  ( ph -> U e. H )
5 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
6 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
7 1 5 6 2 islshp 
 |-  ( W e. LMod -> ( U e. H <-> ( U e. ( LSubSp ` W ) /\ U =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( U u. { v } ) ) = V ) ) )
8 3 7 syl 
 |-  ( ph -> ( U e. H <-> ( U e. ( LSubSp ` W ) /\ U =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( U u. { v } ) ) = V ) ) )
9 4 8 mpbid 
 |-  ( ph -> ( U e. ( LSubSp ` W ) /\ U =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( U u. { v } ) ) = V ) )
10 9 simp2d 
 |-  ( ph -> U =/= V )