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

Metamath Proof Explorer

Theorem lssne0

Description: A nonzero subspace has a nonzero vector. ( shne0i analog.) (Contributed by NM, 20-Apr-2014) (Proof shortened by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypotheses lss0cl.z ⊢ 0 = ( 0g ‘ 𝑊 )
lss0cl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion lssne0 ( 𝑋 ∈ 𝑆 → ( 𝑋 ≠ { 0 } ↔ ∃ 𝑦 ∈ 𝑋 𝑦 ≠ 0 ) )

Proof

Step Hyp Ref Expression
1 lss0cl.z ⊢ 0 = ( 0g ‘ 𝑊 )
2 lss0cl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 2 lssn0 ⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ≠ ∅ )
4 eqsn ⊢ ( 𝑋 ≠ ∅ → ( 𝑋 = { 0 } ↔ ∀ 𝑦 ∈ 𝑋 𝑦 = 0 ) )
5 3 4 syl ⊢ ( 𝑋 ∈ 𝑆 → ( 𝑋 = { 0 } ↔ ∀ 𝑦 ∈ 𝑋 𝑦 = 0 ) )
6 nne ⊢ ( ¬ 𝑦 ≠ 0 ↔ 𝑦 = 0 )
7 6 ralbii ⊢ ( ∀ 𝑦 ∈ 𝑋 ¬ 𝑦 ≠ 0 ↔ ∀ 𝑦 ∈ 𝑋 𝑦 = 0 )
8 ralnex ⊢ ( ∀ 𝑦 ∈ 𝑋 ¬ 𝑦 ≠ 0 ↔ ¬ ∃ 𝑦 ∈ 𝑋 𝑦 ≠ 0 )
9 7 8 bitr3i ⊢ ( ∀ 𝑦 ∈ 𝑋 𝑦 = 0 ↔ ¬ ∃ 𝑦 ∈ 𝑋 𝑦 ≠ 0 )
10 5 9 bitr2di ⊢ ( 𝑋 ∈ 𝑆 → ( ¬ ∃ 𝑦 ∈ 𝑋 𝑦 ≠ 0 ↔ 𝑋 = { 0 } ) )
11 10 necon1abid ⊢ ( 𝑋 ∈ 𝑆 → ( 𝑋 ≠ { 0 } ↔ ∃ 𝑦 ∈ 𝑋 𝑦 ≠ 0 ) )