Definition df-pj 9175

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 ‘H) ‘A is the projection of vector A onto closed subspace H. Note that the range of proj is the set of all projection operators, so T ∈ ran proj means that T is a projection operator.

Assertion

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

Distinct variable group:   f,h,x,y,z,w

Detailed syntax breakdown of Definition df-pj

Step	Hyp	Ref	Expression
1		cpj 8745	. 2 class proj
2		vh	. . . . . 6 set h
3	2	cv 953	. . . . 5 class h
4		cch 8737	. . . . 5 class Cℋ
5	3, 4	wcel 956	. . . 4 wff h ∈ Cℋ
6		vf	. . . . . 6 set f
7	6	cv 953	. . . . 5 class f
8		vx	. . . . . . . . 9 set x
9	8	cv 953	. . . . . . . 8 class x
10		chil 8727	. . . . . . . 8 class ℋ
11	9, 10	wcel 956	. . . . . . 7 wff x ∈ ℋ
12		vy	. . . . . . . . 9 set y
13	12	cv 953	. . . . . . . 8 class y
14		vz	. . . . . . . . . . . . . 14 set z
15	14	cv 953	. . . . . . . . . . . . 13 class z
16		vw	. . . . . . . . . . . . . 14 set w
17	16	cv 953	. . . . . . . . . . . . 13 class w
18		cva 8728	. . . . . . . . . . . . 13 class +h
19	15, 17, 18	co 3954	. . . . . . . . . . . 12 class (z +h w)
20	9, 19	wceq 954	. . . . . . . . . . 11 wff x = (z +h w)
21		cort 8738	. . . . . . . . . . . 12 class ⊥
22	3, 21	cfv 3177	. . . . . . . . . . 11 class (⊥ ‘h)
23	20, 16, 22	wrex 1643	. . . . . . . . . 10 wff ∃w ∈ (⊥ ‘h)x = (z +h w)
24	23, 14, 3	crab 1645	. . . . . . . . 9 class {z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +h w)}
25	24	cuni 2498	. . . . . . . 8 class ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +h w)}
26	13, 25	wceq 954	. . . . . . 7 wff y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +h w)}
27	11, 26	wa 223	. . . . . 6 wff (x ∈ ℋ ⋀ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +h w)})
28	27, 8, 12	copab 2661	. . . . 5 class {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +h w)})}
29	7, 28	wceq 954	. . . 4 wff f = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +h w)})}
30	5, 29	wa 223	. . 3 wff (h ∈ Cℋ ⋀ f = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +h w)})})
31	30, 2, 6	copab 2661	. 2 class {⟨h, f⟩∣(h ∈ Cℋ ⋀ f = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +h w)})})}
32	1, 31	wceq 954	1 wff proj = {⟨h, f⟩∣(h ∈ Cℋ ⋀ f = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ∪{z ∈ h∣∃w ∈ (⊥ ‘h)x = (z +h w)})})}

This definition is referenced by:  pjmvalt 9176  pjmfn 9600

Copyright terms: Public domain