Metamath Proof Explorer

Theorem pjch1

Description: Property of identity projection. Remark in Beran p. 111. (Contributed by NM, 28-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion pjch1 
|- ( A e. ~H -> ( ( projh ` ~H ) ` A ) = A )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( A e. ~H <-> if ( A e. ~H , A , 0h ) e. ~H ) )
2 fveq2 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( projh ` ~H ) ` A ) = ( ( projh ` ~H ) ` if ( A e. ~H , A , 0h ) ) )
3 id 
 |-  ( A = if ( A e. ~H , A , 0h ) -> A = if ( A e. ~H , A , 0h ) )
4 2 3 eqeq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( projh ` ~H ) ` A ) = A <-> ( ( projh ` ~H ) ` if ( A e. ~H , A , 0h ) ) = if ( A e. ~H , A , 0h ) ) )
5 1 4 bibi12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( A e. ~H <-> ( ( projh ` ~H ) ` A ) = A ) <-> ( if ( A e. ~H , A , 0h ) e. ~H <-> ( ( projh ` ~H ) ` if ( A e. ~H , A , 0h ) ) = if ( A e. ~H , A , 0h ) ) ) )
6 helch 
 |-  ~H e. CH
7 ifhvhv0 
 |-  if ( A e. ~H , A , 0h ) e. ~H
8 6 7 pjchi 
 |-  ( if ( A e. ~H , A , 0h ) e. ~H <-> ( ( projh ` ~H ) ` if ( A e. ~H , A , 0h ) ) = if ( A e. ~H , A , 0h ) )
9 5 8 dedth 
 |-  ( A e. ~H -> ( A e. ~H <-> ( ( projh ` ~H ) ` A ) = A ) )
10 9 ibi 
 |-  ( A e. ~H -> ( ( projh ` ~H ) ` A ) = A )