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

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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lshpne.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lshpne.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lshpne.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
Assertion lshpne ( 𝜑 → 𝑈 ≠ 𝑉 )

Proof

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