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

Metamath Proof Explorer

Theorem pjhval

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

Ref Expression
Assertion pjhval 
|- ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) = ( iota_ x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )

Proof

Step Hyp Ref Expression
1 pjhfval 
 |-  ( H e. CH -> ( projh ` H ) = ( z e. ~H |-> ( iota_ x e. H E. y e. ( _|_ ` H ) z = ( x +h y ) ) ) )
2 1 fveq1d 
 |-  ( H e. CH -> ( ( projh ` H ) ` A ) = ( ( z e. ~H |-> ( iota_ x e. H E. y e. ( _|_ ` H ) z = ( x +h y ) ) ) ` A ) )
3 eqeq1 
 |-  ( z = A -> ( z = ( x +h y ) <-> A = ( x +h y ) ) )
4 3 rexbidv 
 |-  ( z = A -> ( E. y e. ( _|_ ` H ) z = ( x +h y ) <-> E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
5 4 riotabidv 
 |-  ( z = A -> ( iota_ x e. H E. y e. ( _|_ ` H ) z = ( x +h y ) ) = ( iota_ x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
6 eqid 
 |-  ( z e. ~H |-> ( iota_ x e. H E. y e. ( _|_ ` H ) z = ( x +h y ) ) ) = ( z e. ~H |-> ( iota_ x e. H E. y e. ( _|_ ` H ) z = ( x +h y ) ) )
7 riotaex 
 |-  ( iota_ x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) e. _V
8 5 6 7 fvmpt 
 |-  ( A e. ~H -> ( ( z e. ~H |-> ( iota_ x e. H E. y e. ( _|_ ` H ) z = ( x +h y ) ) ) ` A ) = ( iota_ x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
9 2 8 sylan9eq 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) = ( iota_ x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )