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

Metamath Proof Explorer

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 )