Definition df-pj 10662

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 10230	. 2 class proj
2		vh	. . . . . 6 set h
3	2	cv 1135	. . . . 5 class h
4		cch 10222	. . . . 5 class CH
5	3, 4	wcel 1138	. . . 4 wff h e. CH
6		vf	. . . . . 6 set f
7	6	cv 1135	. . . . 5 class f
8		vx	. . . . . . . . 9 set x
9	8	cv 1135	. . . . . . . 8 class x
10		chil 10212	. . . . . . . 8 class ~H
11	9, 10	wcel 1138	. . . . . . 7 wff x e. ~H
12		vy	. . . . . . . . 9 set y
13	12	cv 1135	. . . . . . . 8 class y
14		vz	. . . . . . . . . . . . . 14 set z
15	14	cv 1135	. . . . . . . . . . . . 13 class z
16		vw	. . . . . . . . . . . . . 14 set w
17	16	cv 1135	. . . . . . . . . . . . 13 class w
18		cva 10213	. . . . . . . . . . . . 13 class +h
19	15, 17, 18	co 4695	. . . . . . . . . . . 12 class (z +h w)
20	9, 19	wceq 1136	. . . . . . . . . . 11 wff x = (z +h w)
21		cort 10223	. . . . . . . . . . . 12 class _|_
22	3, 21	cfv 3809	. . . . . . . . . . 11 class (_|_` h)
23	20, 16, 22	wrex 1940	. . . . . . . . . 10 wff E.w e. (_|_` h)x = (z +h w)
24	23, 14, 3	crab 1942	. . . . . . . . 9 class {z e. h | E.w e. (_|_` h)x = (z +h w)}
25	24	cuni 2999	. . . . . . . 8 class U.{z e. h | E.w e. (_|_` h)x = (z +h w)}
26	13, 25	wceq 1136	. . . . . . 7 wff y = U.{z e. h | E.w e. (_|_` h)x = (z +h w)}
27	11, 26	wa 239	. . . . . 6 wff (x e. ~H /\ y = U.{z e. h | E.w e. (_|_` h)x = (z +h w)})
28	27, 8, 12	copab 3213	. . . . 5 class {<.x, y>. | (x e. ~H /\ y = U.{z e. h | E.w e. (_|_` h)x = (z +h w)})}
29	7, 28	wceq 1136	. . . 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 239	. . 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 3213	. 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 1136	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:  pjmval 10663  pjmfn 11087

Copyright terms: Public domain