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 )