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=\mathrm{proj}\left(W\right)$$
	pjf.v	$$⊢V={\mathrm{Base}}_W$$
Assertion	pjf	$$⊢T\in \mathrm{dom}K\to K\left(T\right):V⟶V$$

Proof

Step	Hyp	Ref	Expression
1		pjf.k	$$⊢K=\mathrm{proj}\left(W\right)$$
2		pjf.v	$$⊢V={\mathrm{Base}}_W$$
3		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
4		eqid	$$⊢\mathrm{ocv}\left(W\right)=\mathrm{ocv}\left(W\right)$$
5		eqid	$$⊢{proj}_1\left(W\right)={proj}_1\left(W\right)$$
6	2 3 4 5 1	pjdm	$$⊢T\in \mathrm{dom}K\leftrightarrow \left(T\in \mathrm{LSubSp}\left(W\right)\wedge \left(T{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(T\right)\right):V⟶V\right)$$
7	6	simprbi	$$⊢T\in \mathrm{dom}K\to \left(T{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(T\right)\right):V⟶V$$
8	4 5 1	pjval	$$⊢T\in \mathrm{dom}K\to K\left(T\right)=T{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(T\right)$$
9	8	feq1d	$$⊢T\in \mathrm{dom}K\to \left(K\left(T\right):V⟶V\leftrightarrow \left(T{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(T\right)\right):V⟶V\right)$$
10	7 9	mpbird	$$⊢T\in \mathrm{dom}K\to K\left(T\right):V⟶V$$