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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )