Theorem lshplss

Description: A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014)

	Ref	Expression
Hypotheses	lshplss.s	|- S = ( LSubSp ` W )
	lshplss.h	|- H = ( LSHyp ` W )
	lshplss.w	|- ( ph -> W e. LMod )
	lshplss.u	|- ( ph -> U e. H )
Assertion	lshplss	|- ( ph -> U e. S )

Proof

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