Metamath Proof Explorer

Theorem pj11

Description: One-to-one correspondence of projection and subspace. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pj11 
|- ( ( G e. CH /\ H e. CH ) -> ( ( projh ` G ) = ( projh ` H ) <-> G = H ) )

Proof

Step Hyp Ref Expression
1 fveqeq2 
 |-  ( G = if ( G e. CH , G , 0H ) -> ( ( projh ` G ) = ( projh ` H ) <-> ( projh ` if ( G e. CH , G , 0H ) ) = ( projh ` H ) ) )
2 eqeq1 
 |-  ( G = if ( G e. CH , G , 0H ) -> ( G = H <-> if ( G e. CH , G , 0H ) = H ) )
3 1 2 bibi12d 
 |-  ( G = if ( G e. CH , G , 0H ) -> ( ( ( projh ` G ) = ( projh ` H ) <-> G = H ) <-> ( ( projh ` if ( G e. CH , G , 0H ) ) = ( projh ` H ) <-> if ( G e. CH , G , 0H ) = H ) ) )
4 fveq2 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( projh ` H ) = ( projh ` if ( H e. CH , H , 0H ) ) )
5 4 eqeq2d 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( ( projh ` if ( G e. CH , G , 0H ) ) = ( projh ` H ) <-> ( projh ` if ( G e. CH , G , 0H ) ) = ( projh ` if ( H e. CH , H , 0H ) ) ) )
6 eqeq2 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( if ( G e. CH , G , 0H ) = H <-> if ( G e. CH , G , 0H ) = if ( H e. CH , H , 0H ) ) )
7 5 6 bibi12d 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( ( ( projh ` if ( G e. CH , G , 0H ) ) = ( projh ` H ) <-> if ( G e. CH , G , 0H ) = H ) <-> ( ( projh ` if ( G e. CH , G , 0H ) ) = ( projh ` if ( H e. CH , H , 0H ) ) <-> if ( G e. CH , G , 0H ) = if ( H e. CH , H , 0H ) ) ) )
8 h0elch 
 |-  0H e. CH
9 8 elimel 
 |-  if ( G e. CH , G , 0H ) e. CH
10 8 elimel 
 |-  if ( H e. CH , H , 0H ) e. CH
11 9 10 pj11i 
 |-  ( ( projh ` if ( G e. CH , G , 0H ) ) = ( projh ` if ( H e. CH , H , 0H ) ) <-> if ( G e. CH , G , 0H ) = if ( H e. CH , H , 0H ) )
12 3 7 11 dedth2h 
 |-  ( ( G e. CH /\ H e. CH ) -> ( ( projh ` G ) = ( projh ` H ) <-> G = H ) )