Definition df-pjh

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpjh	|- projh
1		vh	|- h
2		cch	|- CH
3		vx	|- x
4		chba	|- ~H
5		vz	|- z
6	1	cv	|- h
7		vy	|- y
8		cort	|- _|_
9	6 8	cfv	|- ( _|_ ` h )
10	3	cv	|- x
11	5	cv	|- z
12		cva	|- +h
13	7	cv	|- y
14	11 13 12	co	|- ( z +h y )
15	10 14	wceq	|- x = ( z +h y )
16	15 7 9	wrex	|- E. y e. ( _|_ ` h ) x = ( z +h y )
17	16 5 6	crio	|- ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) )
18	3 4 17	cmpt	|- ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) )
19	1 2 18	cmpt	|- ( h e. CH |-> ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) ) )
20	0 19	wceq	|- projh = ( h e. CH |-> ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) ) )