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

Metamath Proof Explorer

Theorem lssneln0

Description: A vector X which doesn't belong to a subspace U is nonzero. (Contributed by NM, 14-May-2015) (Revised by AV, 17-Jul-2022) (Proof shortened by AV, 19-Jul-2022)

	Ref	Expression
Hypotheses	lssneln0.o	⊢ 0 = ( 0_g ‘ 𝑊 )
	lssneln0.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lssneln0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lssneln0.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lssneln0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lssneln0.n	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
Assertion	lssneln0	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		lssneln0.o	⊢ 0 = ( 0_g ‘ 𝑊 )
2		lssneln0.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lssneln0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
4		lssneln0.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
5		lssneln0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6		lssneln0.n	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
7	1 2 3 4 6	lssvneln0	⊢ ( 𝜑 → 𝑋 ≠ 0 )
8		eldifsn	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) )
9	5 7 8	sylanbrc	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )