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 ) )