Definition df-pjh

Description: Define the projection function on a Hilbert space, as a mapping from the Hilbert lattice to a function on Hilbert space. Every closed subspace is associated with a unique projection function. Remark in Kalmbach p. 66, adopted as a definition. ( projhH )A is the projection of vector A onto closed subspace H . Note that the range of projh is the set of all projection operators, so T e. ran projh means that T is a projection operator. (Contributed by NM, 23-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	df-pjh	$$⊢{\mathrm{proj}}_{ℎ}=\left(h\in {\mathbf{C}}_{\mathscr{H}}⟼\left(x\in \mathscr{H}⟼\left(\iota z\in h|\exists y\in \perp \left(h\right)x=z{+}_{ℎ}y\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpjh	$$class{\mathrm{proj}}_{ℎ}$$
1		vh	$$setvarh$$
2		cch	$$class{\mathbf{C}}_{\mathscr{H}}$$
3		vx	$$setvarx$$
4		chba	$$class\mathscr{H}$$
5		vz	$$setvarz$$
6	1	cv	$$setvarh$$
7		vy	$$setvary$$
8		cort	$$class\perp$$
9	6 8	cfv	$$class\perp \left(h\right)$$
10	3	cv	$$setvarx$$
11	5	cv	$$setvarz$$
12		cva	$$class{+}_{ℎ}$$
13	7	cv	$$setvary$$
14	11 13 12	co	$$class\left(z{+}_{ℎ}y\right)$$
15	10 14	wceq	$$wffx=z{+}_{ℎ}y$$
16	15 7 9	wrex	$$wff\exists y\in \perp \left(h\right)x=z{+}_{ℎ}y$$
17	16 5 6	crio	$$class\left(\iota z\in h|\exists y\in \perp \left(h\right)x=z{+}_{ℎ}y\right)$$
18	3 4 17	cmpt	$$class\left(x\in \mathscr{H}⟼\left(\iota z\in h|\exists y\in \perp \left(h\right)x=z{+}_{ℎ}y\right)\right)$$
19	1 2 18	cmpt	$$class\left(h\in {\mathbf{C}}_{\mathscr{H}}⟼\left(x\in \mathscr{H}⟼\left(\iota z\in h|\exists y\in \perp \left(h\right)x=z{+}_{ℎ}y\right)\right)\right)$$
20	0 19	wceq	$$wff{\mathrm{proj}}_{ℎ}=\left(h\in {\mathbf{C}}_{\mathscr{H}}⟼\left(x\in \mathscr{H}⟼\left(\iota z\in h|\exists y\in \perp \left(h\right)x=z{+}_{ℎ}y\right)\right)\right)$$