Definition df-pj 9232

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 e. ran proj means that T is a projection operator.

Assertion

Ref	Expression
df-pj	|- proj = {<.h, f>. | (h e. CH /\ f = {<.x, y>. | (x e. H~ /\ y = U.{z e. h | E.w e. (_|_` 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 8801	. 2 class proj
2		vh	. . . . . 6 set h
3	2	cv 957	. . . . 5 class h
4		cch 8793	. . . . 5 class CH
5	3, 4	wcel 960	. . . 4 wff h e. CH
6		vf	. . . . . 6 set f
7	6	cv 957	. . . . 5 class f
8		vx	. . . . . . . . 9 set x
9	8	cv 957	. . . . . . . 8 class x
10		chil 8783	. . . . . . . 8 class H~
11	9, 10	wcel 960	. . . . . . 7 wff x e. H~
12		vy	. . . . . . . . 9 set y
13	12	cv 957	. . . . . . . 8 class y
14		vz	. . . . . . . . . . . . . 14 set z
15	14	cv 957	. . . . . . . . . . . . 13 class z
16		vw	. . . . . . . . . . . . . 14 set w
17	16	cv 957	. . . . . . . . . . . . 13 class w
18		cva 8784	. . . . . . . . . . . . 13 class +h
19	15, 17, 18	co 3969	. . . . . . . . . . . 12 class (z +h w)
20	9, 19	wceq 958	. . . . . . . . . . 11 wff x = (z +h w)
21		cort 8794	. . . . . . . . . . . 12 class _|_
22	3, 21	cfv 3188	. . . . . . . . . . 11 class (_|_` h)
23	20, 16, 22	wrex 1649	. . . . . . . . . 10 wff E.w e. (_|_` h)x = (z +h w)
24	23, 14, 3	crab 1651	. . . . . . . . 9 class {z e. h | E.w e. (_|_` h)x = (z +h w)}
25	24	cuni 2507	. . . . . . . 8 class U.{z e. h | E.w e. (_|_` h)x = (z +h w)}
26	13, 25	wceq 958	. . . . . . 7 wff y = U.{z e. h | E.w e. (_|_` h)x = (z +h w)}
27	11, 26	wa 223	. . . . . 6 wff (x e. H~ /\ y = U.{z e. h | E.w e. (_|_` h)x = (z +h w)})
28	27, 8, 12	copab 2671	. . . . 5 class {<.x, y>. | (x e. H~ /\ y = U.{z e. h | E.w e. (_|_` h)x = (z +h w)})}
29	7, 28	wceq 958	. . . 4 wff f = {<.x, y>. | (x e. H~ /\ y = U.{z e. h | E.w e. (_|_` h)x = (z +h w)})}
30	5, 29	wa 223	. . 3 wff (h e. CH /\ f = {<.x, y>. | (x e. H~ /\ y = U.{z e. h | E.w e. (_|_` h)x = (z +h w)})})
31	30, 2, 6	copab 2671	. 2 class {<.h, f>. | (h e. CH /\ f = {<.x, y>. | (x e. H~ /\ y = U.{z e. h | E.w e. (_|_` h)x = (z +h w)})})}
32	1, 31	wceq 958	1 wff proj = {<.h, f>. | (h e. CH /\ f = {<.x, y>. | (x e. H~ /\ y = U.{z e. h | E.w e. (_|_` h)x = (z +h w)})})}

This definition is referenced by:  pjmvalt 9233  pjmfn 9655

Copyright terms: Public domain