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

Metamath Proof Explorer

Theorem chj0

Description: Join with Hilbert lattice zero. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chj0 
|- ( A e. CH -> ( A vH 0H ) = A )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( A vH 0H ) = ( if ( A e. CH , A , 0H ) vH 0H ) )
2 id 
 |-  ( A = if ( A e. CH , A , 0H ) -> A = if ( A e. CH , A , 0H ) )
3 1 2 eqeq12d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( A vH 0H ) = A <-> ( if ( A e. CH , A , 0H ) vH 0H ) = if ( A e. CH , A , 0H ) ) )
4 h0elch 
 |-  0H e. CH
5 4 elimel 
 |-  if ( A e. CH , A , 0H ) e. CH
6 5 chj0i 
 |-  ( if ( A e. CH , A , 0H ) vH 0H ) = if ( A e. CH , A , 0H )
7 3 6 dedth 
 |-  ( A e. CH -> ( A vH 0H ) = A )