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	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )