Metamath Proof Explorer

Theorem lshpne

Description: A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014)

Ref Expression
Hypotheses lshpne.v ⊢ V = Base W
lshpne.h ⊢ H = LSHyp ⁡ W
lshpne.w ⊢ φ → W ∈ LMod
lshpne.u ⊢ φ → U ∈ H
Assertion lshpne ⊢ φ → U ≠ V

Proof

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