Definition df-pjh 28254

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 ` H ) ` A is the projection of vector A onto closed subspace H. Note that the range of proj h is the set of all projection operators, so T e. ran proj h means that T is a projection operator. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
df-pjh	|- proj h = ( h e. CH |-> ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) ) )

Distinct variable group:   x, h, y, z

Detailed syntax breakdown of Definition df-pjh

Step	Hyp	Ref	Expression
1		cpjh 27794	. 2 class proj h
2		vh	. . 3 setvar h
3		cch 27786	. . 3 class CH
4		vx	. . . 4 setvar x
5		chil 27776	. . . 4 class ~H
6	4	cv 1482	. . . . . . 7 class x
7		vz	. . . . . . . . 9 setvar z
8	7	cv 1482	. . . . . . . 8 class z
9		vy	. . . . . . . . 9 setvar y
10	9	cv 1482	. . . . . . . 8 class y
11		cva 27777	. . . . . . . 8 class +h
12	8, 10, 11	co 6650	. . . . . . 7 class ( z +h y )
13	6, 12	wceq 1483	. . . . . 6 wff x = ( z +h y )
14	2	cv 1482	. . . . . . 7 class h
15		cort 27787	. . . . . . 7 class _|_
16	14, 15	cfv 5888	. . . . . 6 class ( _|_ ` h )
17	13, 9, 16	wrex 2913	. . . . 5 wff E. y e. ( _|_ ` h ) x = ( z +h y )
18	17, 7, 14	crio 6610	. . . 4 class ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) )
19	4, 5, 18	cmpt 4729	. . 3 class ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) )
20	2, 3, 19	cmpt 4729	. 2 class ( h e. CH |-> ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) ) )
21	1, 20	wceq 1483	1 wff proj h = ( h e. CH |-> ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) ) )

This definition is referenced by:  pjhfval  28255  pjmfn  28574