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 
|- ( A e. CH -> ( A =/= 0H <-> E. x e. A x =/= 0h ) )

Proof

Step Hyp Ref Expression
1 neeq1 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( A =/= 0H <-> if ( A e. CH , A , 0H ) =/= 0H ) )
2 rexeq 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( E. x e. A x =/= 0h <-> E. x e. if ( A e. CH , A , 0H ) x =/= 0h ) )
3 1 2 bibi12d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( A =/= 0H <-> E. x e. A x =/= 0h ) <-> ( if ( A e. CH , A , 0H ) =/= 0H <-> E. x e. if ( A e. CH , A , 0H ) x =/= 0h ) ) )
4 h0elch 
 |-  0H e. CH
5 4 elimel 
 |-  if ( A e. CH , A , 0H ) e. CH
6 5 chne0i 
 |-  ( if ( A e. CH , A , 0H ) =/= 0H <-> E. x e. if ( A e. CH , A , 0H ) x =/= 0h )
7 3 6 dedth 
 |-  ( A e. CH -> ( A =/= 0H <-> E. x e. A x =/= 0h ) )