Theorem dfpjop

Description: Definition of projection operator in Hughes p. 47, except that we do not need linearity to be explicit by virtue of hmoplin . (Contributed by NM, 24-Apr-2006) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	dfpjop	|- ( T e. ran projh <-> ( T e. HrmOp /\ ( T o. T ) = T ) )

Proof

Step	Hyp	Ref	Expression
1		pjmfn	|- projh Fn CH
2		fvelrnb	|- ( projh Fn CH -> ( T e. ran projh <-> E. x e. CH ( projh ` x ) = T ) )
3	1 2	ax-mp	|- ( T e. ran projh <-> E. x e. CH ( projh ` x ) = T )
4		pjhmop	|- ( x e. CH -> ( projh ` x ) e. HrmOp )
5		pjidmco	|- ( x e. CH -> ( ( projh ` x ) o. ( projh ` x ) ) = ( projh ` x ) )
6	4 5	jca	|- ( x e. CH -> ( ( projh ` x ) e. HrmOp /\ ( ( projh ` x ) o. ( projh ` x ) ) = ( projh ` x ) ) )
7		eleq1	|- ( ( projh ` x ) = T -> ( ( projh ` x ) e. HrmOp <-> T e. HrmOp ) )
8		id	|- ( ( projh ` x ) = T -> ( projh ` x ) = T )
9	8 8	coeq12d	|- ( ( projh ` x ) = T -> ( ( projh ` x ) o. ( projh ` x ) ) = ( T o. T ) )
10	9 8	eqeq12d	|- ( ( projh ` x ) = T -> ( ( ( projh ` x ) o. ( projh ` x ) ) = ( projh ` x ) <-> ( T o. T ) = T ) )
11	7 10	anbi12d	|- ( ( projh ` x ) = T -> ( ( ( projh ` x ) e. HrmOp /\ ( ( projh ` x ) o. ( projh ` x ) ) = ( projh ` x ) ) <-> ( T e. HrmOp /\ ( T o. T ) = T ) ) )
12	6 11	syl5ibcom	|- ( x e. CH -> ( ( projh ` x ) = T -> ( T e. HrmOp /\ ( T o. T ) = T ) ) )
13	12	rexlimiv	|- ( E. x e. CH ( projh ` x ) = T -> ( T e. HrmOp /\ ( T o. T ) = T ) )
14	3 13	sylbi	|- ( T e. ran projh -> ( T e. HrmOp /\ ( T o. T ) = T ) )
15		hmopidmpj	|- ( ( T e. HrmOp /\ ( T o. T ) = T ) -> T = ( projh ` ran T ) )
16		hmopidmch	|- ( ( T e. HrmOp /\ ( T o. T ) = T ) -> ran T e. CH )
17		fnfvelrn	|- ( ( projh Fn CH /\ ran T e. CH ) -> ( projh ` ran T ) e. ran projh )
18	1 16 17	sylancr	|- ( ( T e. HrmOp /\ ( T o. T ) = T ) -> ( projh ` ran T ) e. ran projh )
19	15 18	eqeltrd	|- ( ( T e. HrmOp /\ ( T o. T ) = T ) -> T e. ran projh )
20	14 19	impbii	|- ( T e. ran projh <-> ( T e. HrmOp /\ ( T o. T ) = T ) )