Definition df-pj 5244

Description: Define the projection map 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. Remark of [Kalmbach] p. 66, adopted as a definition.

Assertion

Ref	Expression
df-pj	⊢ Proj = {⟨h, f⟩∣(h ∈ Cℋ ∧ f = {⟨x, y⟩∣(x ∈ ℋ ∧ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +v w)})})}

Distinct variable group(s):   f,h,x,y,z,w

Detailed syntax breakdown of Definition df-pj

Step	Hyp	Ref	Expression
1		cpj 4976	. 2 class Proj
2		vh	. . . . . 6 set h
3	2	cv 1089	. . . . 5 class h
4		cch 4968	. . . . 5 class Cℋ
5	3, 4	wcel 1092	. . . 4 wff h ∈ Cℋ
6		vf	. . . . . 6 set f
7	6	cv 1089	. . . . 5 class f
8		vx	. . . . . . . . 9 set x
9	8	cv 1089	. . . . . . . 8 class x
10		chil 4958	. . . . . . . 8 class ℋ
11	9, 10	wcel 1092	. . . . . . 7 wff x ∈ ℋ
12		vy	. . . . . . . . 9 set y
13	12	cv 1089	. . . . . . . 8 class y
14		vz	. . . . . . . . . . . . . 14 set z
15	14	cv 1089	. . . . . . . . . . . . 13 class z
16		vw	. . . . . . . . . . . . . 14 set w
17	16	cv 1089	. . . . . . . . . . . . 13 class w
18		cva 4959	. . . . . . . . . . . . 13 class +v
19	15, 17, 18	co 3001	. . . . . . . . . . . 12 class (z +v w)
20	9, 19	wceq 1091	. . . . . . . . . . 11 wff x = (z +v w)
21		cort 4969	. . . . . . . . . . . 12 class ⊥
22	3, 21	cfv 2422	. . . . . . . . . . 11 class (⊥ ‘h)
23	20, 16, 22	wrex 1202	. . . . . . . . . 10 wff ∃w ∈ (⊥ ‘h)x = (z +v w)
24	23, 14, 3	crab 1204	. . . . . . . . 9 class {z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +v w)}
25	24	cuni 1919	. . . . . . . 8 class ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +v w)}
26	13, 25	wceq 1091	. . . . . . 7 wff y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +v w)}
27	11, 26	wa 196	. . . . . 6 wff (x ∈ ℋ ∧ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +v w)})
28	27, 8, 12	copab 2055	. . . . 5 class {⟨x, y⟩∣(x ∈ ℋ ∧ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +v w)})}
29	7, 28	wceq 1091	. . . 4 wff f = {⟨x, y⟩∣(x ∈ ℋ ∧ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +v w)})}
30	5, 29	wa 196	. . 3 wff (h ∈ Cℋ ∧ f = {⟨x, y⟩∣(x ∈ ℋ ∧ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +v w)})})
31	30, 2, 6	copab 2055	. 2 class {⟨h, f⟩∣(h ∈ Cℋ ∧ f = {⟨x, y⟩∣(x ∈ ℋ ∧ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +v w)})})}
32	1, 31	wceq 1091	1 wff Proj = {⟨h, f⟩∣(h ∈ Cℋ ∧ f = {⟨x, y⟩∣(x ∈ ℋ ∧ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +v w)})})}

This definition is referenced by:  pjmvalt 5245

metamath.org