This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ proj ℎ = h ∈ C ℋ ⟼ x ∈ ℋ ⟼ ι z ∈ h | ∃ y ∈ ⊥ ⁡ h x = z + ℎ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpjh class proj ℎ
1 vh setvar h
2 cch class C ℋ
3 vx setvar x
4 chba class ℋ
5 vz setvar z
6 1 cv setvar h
7 vy setvar y
8 cort class ⊥
9 6 8 cfv class ⊥ ⁡ h
10 3 cv setvar x
11 5 cv setvar z
12 cva class + ℎ
13 7 cv setvar y
14 11 13 12 co class z + ℎ y
15 10 14 wceq wff x = z + ℎ y
16 15 7 9 wrex wff ∃ y ∈ ⊥ ⁡ h x = z + ℎ y
17 16 5 6 crio class ι z ∈ h | ∃ y ∈ ⊥ ⁡ h x = z + ℎ y
18 3 4 17 cmpt class x ∈ ℋ ⟼ ι z ∈ h | ∃ y ∈ ⊥ ⁡ h x = z + ℎ y
19 1 2 18 cmpt class h ∈ C ℋ ⟼ x ∈ ℋ ⟼ ι z ∈ h | ∃ y ∈ ⊥ ⁡ h x = z + ℎ y
20 0 19 wceq wff proj ℎ = h ∈ C ℋ ⟼ x ∈ ℋ ⟼ ι z ∈ h | ∃ y ∈ ⊥ ⁡ h x = z + ℎ y