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

Metamath Proof Explorer

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 )