Definition df-pjh 27638

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 27178	. 2 class projℎ
2		vh	. . 3 setvar ℎ
3		cch 27170	. . 3 class Cℋ
4		vx	. . . 4 setvar 𝑥
5		chil 27160	. . . 4 class ℋ
6	4	cv 1474	. . . . . . 7 class 𝑥
7		vz	. . . . . . . . 9 setvar 𝑧
8	7	cv 1474	. . . . . . . 8 class 𝑧
9		vy	. . . . . . . . 9 setvar 𝑦
10	9	cv 1474	. . . . . . . 8 class 𝑦
11		cva 27161	. . . . . . . 8 class +ℎ
12	8, 10, 11	co 6549	. . . . . . 7 class (𝑧 +ℎ 𝑦)
13	6, 12	wceq 1475	. . . . . 6 wff 𝑥 = (𝑧 +ℎ 𝑦)
14	2	cv 1474	. . . . . . 7 class ℎ
15		cort 27171	. . . . . . 7 class ⊥
16	14, 15	cfv 5804	. . . . . 6 class (⊥‘ℎ)
17	13, 9, 16	wrex 2897	. . . . 5 wff ∃𝑦 ∈ (⊥‘ℎ)𝑥 = (𝑧 +ℎ 𝑦)
18	17, 7, 14	crio 6510	. . . 4 class (℩𝑧 ∈ ℎ ∃𝑦 ∈ (⊥‘ℎ)𝑥 = (𝑧 +ℎ 𝑦))
19	4, 5, 18	cmpt 4643	. . 3 class (𝑥 ∈ ℋ ↦ (℩𝑧 ∈ ℎ ∃𝑦 ∈ (⊥‘ℎ)𝑥 = (𝑧 +ℎ 𝑦)))
20	2, 3, 19	cmpt 4643	. 2 class (ℎ ∈ Cℋ ↦ (𝑥 ∈ ℋ ↦ (℩𝑧 ∈ ℎ ∃𝑦 ∈ (⊥‘ℎ)𝑥 = (𝑧 +ℎ 𝑦))))
21	1, 20	wceq 1475	1 wff projℎ = (ℎ ∈ Cℋ ↦ (𝑥 ∈ ℋ ↦ (℩𝑧 ∈ ℎ ∃𝑦 ∈ (⊥‘ℎ)𝑥 = (𝑧 +ℎ 𝑦))))

This definition is referenced by:  pjhfval  27639  pjmfn  27958