Theorem pjeq

Description: Equality with a projection. (Contributed by NM, 20-Jan-2007) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		pjhth	|- ( H e. CH -> ( H +H ( _|_ ` H ) ) = ~H )
2	1	eleq2d	|- ( H e. CH -> ( A e. ( H +H ( _|_ ` H ) ) <-> A e. ~H ) )
3	2	biimpar	|- ( ( H e. CH /\ A e. ~H ) -> A e. ( H +H ( _|_ ` H ) ) )
4		pjpreeq	|- ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> ( ( ( projh ` H ) ` A ) = B <-> ( B e. H /\ E. x e. ( _|_ ` H ) A = ( B +h x ) ) ) )
5	3 4	syldan	|- ( ( H e. CH /\ A e. ~H ) -> ( ( ( projh ` H ) ` A ) = B <-> ( B e. H /\ E. x e. ( _|_ ` H ) A = ( B +h x ) ) ) )