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 )