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 ⊢ S = LSubSp ⁡ W
lshplss.h ⊢ H = LSHyp ⁡ W
lshplss.w ⊢ φ → W ∈ LMod
lshplss.u ⊢ φ → U ∈ H
Assertion lshplss ⊢ φ → U ∈ S

Proof

Step Hyp Ref Expression
1 lshplss.s ⊢ S = LSubSp ⁡ W
2 lshplss.h ⊢ H = LSHyp ⁡ W
3 lshplss.w ⊢ φ → W ∈ LMod
4 lshplss.u ⊢ φ → U ∈ H
5 eqid ⊢ Base W = Base W
6 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
7 5 6 1 2 islshp ⊢ W ∈ LMod → U ∈ H ↔ U ∈ S ∧ U ≠ Base W ∧ ∃ v ∈ Base W LSpan ⁡ W ⁡ U ∪ v = Base W
8 3 7 syl ⊢ φ → U ∈ H ↔ U ∈ S ∧ U ≠ Base W ∧ ∃ v ∈ Base W LSpan ⁡ W ⁡ U ∪ v = Base W
9 4 8 mpbid ⊢ φ → U ∈ S ∧ U ≠ Base W ∧ ∃ v ∈ Base W LSpan ⁡ W ⁡ U ∪ v = Base W
10 9 simp1d ⊢ φ → U ∈ S