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

Metamath Proof Explorer

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