Metamath Proof Explorer

Theorem pjhfval

Description: The value of the projection map. (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion pjhfval 
|- ( H e. CH -> ( projh ` H ) = ( x e. ~H |-> ( iota_ z e. H E. y e. ( _|_ ` H ) x = ( z +h y ) ) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( h = H -> h = H )
2 fveq2 
 |-  ( h = H -> ( _|_ ` h ) = ( _|_ ` H ) )
3 2 rexeqdv 
 |-  ( h = H -> ( E. y e. ( _|_ ` h ) x = ( z +h y ) <-> E. y e. ( _|_ ` H ) x = ( z +h y ) ) )
4 1 3 riotaeqbidv 
 |-  ( h = H -> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) = ( iota_ z e. H E. y e. ( _|_ ` H ) x = ( z +h y ) ) )
5 4 mpteq2dv 
 |-  ( h = H -> ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) ) = ( x e. ~H |-> ( iota_ z e. H E. y e. ( _|_ ` H ) x = ( z +h y ) ) ) )
6 df-pjh 
 |-  projh = ( h e. CH |-> ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) ) )
7 ax-hilex 
 |-  ~H e. _V
8 7 mptex 
 |-  ( x e. ~H |-> ( iota_ z e. H E. y e. ( _|_ ` H ) x = ( z +h y ) ) ) e. _V
9 5 6 8 fvmpt 
 |-  ( H e. CH -> ( projh ` H ) = ( x e. ~H |-> ( iota_ z e. H E. y e. ( _|_ ` H ) x = ( z +h y ) ) ) )