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 ) ) )