Theorem lshpne0

Description: The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014) (Proof shortened by AV, 19-Jul-2022)

	Ref	Expression
Hypotheses	lshpne0.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lshpne0.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lshpne0.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	lshpne0.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
	lshpne0.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lshpne0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lshpne0.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
	lshpne0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lshpne0.e	⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )
Assertion	lshpne0	⊢ ( 𝜑 → 𝑋 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		lshpne0.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lshpne0.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lshpne0.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
4		lshpne0.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
5		lshpne0.o	⊢ 0 = ( 0g ‘ 𝑊 )
6		lshpne0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
7		lshpne0.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
8		lshpne0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9		lshpne0.e	⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )
10		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
11	10 4 6 7	lshplss	⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
12	1 2 3 4 6 7 8 9	lshpnel	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
13	5 10 6 11 12	lssvneln0	⊢ ( 𝜑 → 𝑋 ≠ 0 )