Theorem pjpm

Description: The projection map is a partial function from subspaces of the pre-Hilbert space to total operators. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	pjpm.v	$$⊢V={\mathrm{Base}}_W$$
	pjpm.l	$$⊢L=\mathrm{LSubSp}\left(W\right)$$
	pjpm.k	$$⊢K=\mathrm{proj}\left(W\right)$$
Assertion	pjpm	$$⊢K\in \left(\left(V^V\right){\uparrow }_{𝑝𝑚}L\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjpm.v	$$⊢V={\mathrm{Base}}_W$$
2		pjpm.l	$$⊢L=\mathrm{LSubSp}\left(W\right)$$
3		pjpm.k	$$⊢K=\mathrm{proj}\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	1 2 4 5 3	pjfval	$$⊢K=\left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)\cap \left(\mathrm{V}\times \left(V^V\right)\right)$$
7		inss1	$$⊢\left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)\cap \left(\mathrm{V}\times \left(V^V\right)\right)\subseteq \left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)$$
8	6 7	eqsstri	$$⊢K\subseteq \left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)$$
9		funmpt	$$⊢\mathrm{Fun}\left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)$$
10		funss	$$⊢K\subseteq \left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)\to \left(\mathrm{Fun}\left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)\to \mathrm{Fun}K\right)$$
11	8 9 10	mp2	$$⊢\mathrm{Fun}K$$
12		eqid	$$⊢\left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)=\left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)$$
13		ovexd	$$⊢x\in L\to x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\in \mathrm{V}$$
14	12 13	fmpti	$$⊢\left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right):L⟶\mathrm{V}$$
15		fssxp	$$⊢\left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right):L⟶\mathrm{V}\to \left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)\subseteq L\times \mathrm{V}$$
16		ssrin	$$⊢\left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)\subseteq L\times \mathrm{V}\to \left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)\cap \left(\mathrm{V}\times \left(V^V\right)\right)\subseteq \left(L\times \mathrm{V}\right)\cap \left(\mathrm{V}\times \left(V^V\right)\right)$$
17	14 15 16	mp2b	$$⊢\left(x\in L⟼x{proj}_1\left(W\right)\mathrm{ocv}\left(W\right)\left(x\right)\right)\cap \left(\mathrm{V}\times \left(V^V\right)\right)\subseteq \left(L\times \mathrm{V}\right)\cap \left(\mathrm{V}\times \left(V^V\right)\right)$$
18	6 17	eqsstri	$$⊢K\subseteq \left(L\times \mathrm{V}\right)\cap \left(\mathrm{V}\times \left(V^V\right)\right)$$
19		inxp	$$⊢\left(L\times \mathrm{V}\right)\cap \left(\mathrm{V}\times \left(V^V\right)\right)=\left(L\cap \mathrm{V}\right)\times \left(\mathrm{V}\cap \left(V^V\right)\right)$$
20		inv1	$$⊢L\cap \mathrm{V}=L$$
21		incom	$$⊢\mathrm{V}\cap \left(V^V\right)=\left(V^V\right)\cap \mathrm{V}$$
22		inv1	$$⊢\left(V^V\right)\cap \mathrm{V}=V^V$$
23	21 22	eqtri	$$⊢\mathrm{V}\cap \left(V^V\right)=V^V$$
24	20 23	xpeq12i	$$⊢\left(L\cap \mathrm{V}\right)\times \left(\mathrm{V}\cap \left(V^V\right)\right)=L\times \left(V^V\right)$$
25	19 24	eqtri	$$⊢\left(L\times \mathrm{V}\right)\cap \left(\mathrm{V}\times \left(V^V\right)\right)=L\times \left(V^V\right)$$
26	18 25	sseqtri	$$⊢K\subseteq L\times \left(V^V\right)$$
27		ovex	$$⊢V^V\in \mathrm{V}$$
28	2	fvexi	$$⊢L\in \mathrm{V}$$
29	27 28	elpm	$$⊢K\in \left(\left(V^V\right){\uparrow }_{𝑝𝑚}L\right)\leftrightarrow \left(\mathrm{Fun}K\wedge K\subseteq L\times \left(V^V\right)\right)$$
30	11 26 29	mpbir2an	$$⊢K\in \left(\left(V^V\right){\uparrow }_{𝑝𝑚}L\right)$$