Theorem pjf

Description: A projection is a function on the base set. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	pjf.k	|- K = ( proj ` W )
	pjf.v	|- V = ( Base ` W )
Assertion	pjf	|- ( T e. dom K -> ( K ` T ) : V --> V )

Proof

Step	Hyp	Ref	Expression
1		pjf.k	|- K = ( proj ` W )
2		pjf.v	|- V = ( Base ` W )
3		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
4		eqid	|- ( ocv ` W ) = ( ocv ` W )
5		eqid	|- ( proj1 ` W ) = ( proj1 ` W )
6	2 3 4 5 1	pjdm	|- ( T e. dom K <-> ( T e. ( LSubSp ` W ) /\ ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) : V --> V ) )
7	6	simprbi	|- ( T e. dom K -> ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) : V --> V )
8	4 5 1	pjval	|- ( T e. dom K -> ( K ` T ) = ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) )
9	8	feq1d	|- ( T e. dom K -> ( ( K ` T ) : V --> V <-> ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) : V --> V ) )
10	7 9	mpbird	|- ( T e. dom K -> ( K ` T ) : V --> V )