Definition df-pjh 32006

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. (proj_ℎ‘𝐻)‘𝐴 is the projection of vector 𝐴 onto closed subspace 𝐻. Note that the range of proj_ℎ is the set of all projection operators, so 𝑇 ∈ ran proj_ℎ means that 𝑇 is a projection operator. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
df-pjh	⊢ projℎ = (ℎ ∈ Cℋ ↦ (𝑥 ∈ ℋ ↦ (℩𝑧 ∈ ℎ ∃𝑦 ∈ (⊥‘ℎ)𝑥 = (𝑧 +ℎ 𝑦))))

Distinct variable group:   𝑥,ℎ,𝑦,𝑧

Detailed syntax breakdown of Definition df-pjh

Step	Hyp	Ref	Expression
1		cpjh 31548	. 2 class projℎ
2		vh	. . 3 setvar ℎ
3		cch 31540	. . 3 class Cℋ
4		vx	. . . 4 setvar 𝑥
5		chba 31530	. . . 4 class ℋ
6	4	cv 1568	. . . . . . 7 class 𝑥
7		vz	. . . . . . . . 9 setvar 𝑧
8	7	cv 1568	. . . . . . . 8 class 𝑧
9		vy	. . . . . . . . 9 setvar 𝑦
10	9	cv 1568	. . . . . . . 8 class 𝑦
11		cva 31531	. . . . . . . 8 class +ℎ
12	8, 10, 11	co 7424	. . . . . . 7 class (𝑧 +ℎ 𝑦)
13	6, 12	wceq 1569	. . . . . 6 wff 𝑥 = (𝑧 +ℎ 𝑦)
14	2	cv 1568	. . . . . . 7 class ℎ
15		cort 31541	. . . . . . 7 class ⊥
16	14, 15	cfv 6543	. . . . . 6 class (⊥‘ℎ)
17	13, 9, 16	wrex 3086	. . . . 5 wff ∃𝑦 ∈ (⊥‘ℎ)𝑥 = (𝑧 +ℎ 𝑦)
18	17, 7, 14	crio 7380	. . . 4 class (℩𝑧 ∈ ℎ ∃𝑦 ∈ (⊥‘ℎ)𝑥 = (𝑧 +ℎ 𝑦))
19	4, 5, 18	cmpt 5185	. . 3 class (𝑥 ∈ ℋ ↦ (℩𝑧 ∈ ℎ ∃𝑦 ∈ (⊥‘ℎ)𝑥 = (𝑧 +ℎ 𝑦)))
20	2, 3, 19	cmpt 5185	. 2 class (ℎ ∈ Cℋ ↦ (𝑥 ∈ ℋ ↦ (℩𝑧 ∈ ℎ ∃𝑦 ∈ (⊥‘ℎ)𝑥 = (𝑧 +ℎ 𝑦))))
21	1, 20	wceq 1569	1 wff projℎ = (ℎ ∈ Cℋ ↦ (𝑥 ∈ ℋ ↦ (℩𝑧 ∈ ℎ ∃𝑦 ∈ (⊥‘ℎ)𝑥 = (𝑧 +ℎ 𝑦))))

This definition is used by:  pjhfval  32007  pjmfn  32326