# Metamath Proof Explorer

## 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}}_{ℋ}⟼\left({x}\in ℋ⟼\left(\iota {z}\in {h}|\exists {y}\in \perp \left({h}\right)\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{y}\right)\right)\right)$

### Detailed syntax breakdown

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