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	⊢ proj_ℎ = ( ℎ ∈ C_ℋ ↦ ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ ℎ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +_ℎ 𝑦 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpjh	⊢ proj_ℎ
1		vh	⊢ ℎ
2		cch	⊢ C_ℋ
3		vx	⊢ 𝑥
4		chba	⊢ ℋ
5		vz	⊢ 𝑧
6	1	cv	⊢ ℎ
7		vy	⊢ 𝑦
8		cort	⊢ ⊥
9	6 8	cfv	⊢ ( ⊥ ‘ ℎ )
10	3	cv	⊢ 𝑥
11	5	cv	⊢ 𝑧
12		cva	⊢ +_ℎ
13	7	cv	⊢ 𝑦
14	11 13 12	co	⊢ ( 𝑧 +_ℎ 𝑦 )
15	10 14	wceq	⊢ 𝑥 = ( 𝑧 +_ℎ 𝑦 )
16	15 7 9	wrex	⊢ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +_ℎ 𝑦 )
17	16 5 6	crio	⊢ ( ℩ 𝑧 ∈ ℎ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +_ℎ 𝑦 ) )
18	3 4 17	cmpt	⊢ ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ ℎ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +_ℎ 𝑦 ) ) )
19	1 2 18	cmpt	⊢ ( ℎ ∈ C_ℋ ↦ ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ ℎ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +_ℎ 𝑦 ) ) ) )
20	0 19	wceq	⊢ proj_ℎ = ( ℎ ∈ C_ℋ ↦ ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ ℎ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +_ℎ 𝑦 ) ) ) )

Metamath Proof Explorer

Definition df-pjh

Detailed syntax breakdown