Theorem lssvneln0

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

	Ref	Expression
Hypotheses	lssvneln0.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lssvneln0.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lssvneln0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lssvneln0.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lssvneln0.n	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
Assertion	lssvneln0	⊢ ( 𝜑 → 𝑋 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		lssvneln0.o	⊢ 0 = ( 0g ‘ 𝑊 )
2		lssvneln0.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lssvneln0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
4		lssvneln0.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
5		lssvneln0.n	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
6	1 2	lss0cl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 0 ∈ 𝑈 )
7	3 4 6	syl2anc	⊢ ( 𝜑 → 0 ∈ 𝑈 )
8		eleq1a	⊢ ( 0 ∈ 𝑈 → ( 𝑋 = 0 → 𝑋 ∈ 𝑈 ) )
9	7 8	syl	⊢ ( 𝜑 → ( 𝑋 = 0 → 𝑋 ∈ 𝑈 ) )
10	9	necon3bd	⊢ ( 𝜑 → ( ¬ 𝑋 ∈ 𝑈 → 𝑋 ≠ 0 ) )
11	5 10	mpd	⊢ ( 𝜑 → 𝑋 ≠ 0 )