Definition df-pj

Description: Define orthogonal projection onto a subspace. This is just a wrapping of df-pj1 , but we restrict the domain of this function to only total projection functions. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Assertion	df-pj	$$⊢\mathrm{proj}=\left(h\in \mathrm{V}⟼\left(x\in \mathrm{LSubSp}\left(h\right)⟼x{proj}_1\left(h\right)\mathrm{ocv}\left(h\right)\left(x\right)\right)\cap \left(\mathrm{V}\times \left({{\mathrm{Base}}_h}^{{\mathrm{Base}}_h}\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpj	$$class\mathrm{proj}$$
1		vh	$$setvarh$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		clss	$$class\mathrm{LSubSp}$$
5	1	cv	$$setvarh$$
6	5 4	cfv	$$class\mathrm{LSubSp}\left(h\right)$$
7	3	cv	$$setvarx$$
8		cpj1	$$class{proj}_1$$
9	5 8	cfv	$$class{proj}_1\left(h\right)$$
10		cocv	$$class\mathrm{ocv}$$
11	5 10	cfv	$$class\mathrm{ocv}\left(h\right)$$
12	7 11	cfv	$$class\mathrm{ocv}\left(h\right)\left(x\right)$$
13	7 12 9	co	$$class\left(x{proj}_1\left(h\right)\mathrm{ocv}\left(h\right)\left(x\right)\right)$$
14	3 6 13	cmpt	$$class\left(x\in \mathrm{LSubSp}\left(h\right)⟼x{proj}_1\left(h\right)\mathrm{ocv}\left(h\right)\left(x\right)\right)$$
15		cbs	$$class\mathrm{Base}$$
16	5 15	cfv	$$class{\mathrm{Base}}_h$$
17		cmap	$$class{\uparrow }_{𝑚}$$
18	16 16 17	co	$$class\left({{\mathrm{Base}}_h}^{{\mathrm{Base}}_h}\right)$$
19	2 18	cxp	$$class\left(\mathrm{V}\times \left({{\mathrm{Base}}_h}^{{\mathrm{Base}}_h}\right)\right)$$
20	14 19	cin	$$class\left(\left(x\in \mathrm{LSubSp}\left(h\right)⟼x{proj}_1\left(h\right)\mathrm{ocv}\left(h\right)\left(x\right)\right)\cap \left(\mathrm{V}\times \left({{\mathrm{Base}}_h}^{{\mathrm{Base}}_h}\right)\right)\right)$$
21	1 2 20	cmpt	$$class\left(h\in \mathrm{V}⟼\left(x\in \mathrm{LSubSp}\left(h\right)⟼x{proj}_1\left(h\right)\mathrm{ocv}\left(h\right)\left(x\right)\right)\cap \left(\mathrm{V}\times \left({{\mathrm{Base}}_h}^{{\mathrm{Base}}_h}\right)\right)\right)$$
22	0 21	wceq	$$wff\mathrm{proj}=\left(h\in \mathrm{V}⟼\left(x\in \mathrm{LSubSp}\left(h\right)⟼x{proj}_1\left(h\right)\mathrm{ocv}\left(h\right)\left(x\right)\right)\cap \left(\mathrm{V}\times \left({{\mathrm{Base}}_h}^{{\mathrm{Base}}_h}\right)\right)\right)$$