Theorem lshplss

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

	Ref	Expression
Hypotheses	lshplss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lshplss.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
	lshplss.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lshplss.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
Assertion	lshplss	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		lshplss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lshplss.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
3		lshplss.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
4		lshplss.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
5		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
7	5 6 1 2	islshp	⊢ ( 𝑊 ∈ LMod → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ ( Base ‘ 𝑊 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑈 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) ) ) )
8	3 7	syl	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ ( Base ‘ 𝑊 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑈 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) ) ) )
9	4 8	mpbid	⊢ ( 𝜑 → ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ ( Base ‘ 𝑊 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑈 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑊 ) ) )
10	9	simp1d	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )