# Metamath Proof Explorer

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