Theorem chne0

Description: A nonzero closed subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	chne0	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ≠ 0ℋ ↔ ∃ 𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ ) )

Proof

Step	Hyp	Ref	Expression
1		neeq1	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 ≠ 0ℋ ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ≠ 0ℋ ) )
2		rexeq	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ∃ 𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ ↔ ∃ 𝑥 ∈ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝑥 ≠ 0ℎ ) )
3	1 2	bibi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( 𝐴 ≠ 0ℋ ↔ ∃ 𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ≠ 0ℋ ↔ ∃ 𝑥 ∈ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝑥 ≠ 0ℎ ) ) )
4		h0elch	⊢ 0ℋ ∈ Cℋ
5	4	elimel	⊢ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ Cℋ
6	5	chne0i	⊢ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ≠ 0ℋ ↔ ∃ 𝑥 ∈ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝑥 ≠ 0ℎ )
7	3 6	dedth	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ≠ 0ℋ ↔ ∃ 𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ ) )