Metamath Proof Explorer

Definition df-pj

Description: Define orthogonal projection onto a subspace. This is just a wrapping of df-pj1 , but we restrict the domain of this function to only total projection functions. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Assertion df-pj ⊢ proj = h ∈ V ⟼ x ∈ LSubSp ⁡ h ⟼ x proj 1 ⁡ h ocv ⁡ h ⁡ x ∩ V × Base h Base h

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpj class proj
1 vh setvar h
2 cvv class V
3 vx setvar x
4 clss class LSubSp
5 1 cv setvar h
6 5 4 cfv class LSubSp ⁡ h
7 3 cv setvar x
8 cpj1 class proj 1
9 5 8 cfv class proj 1 ⁡ h
10 cocv class ocv
11 5 10 cfv class ocv ⁡ h
12 7 11 cfv class ocv ⁡ h ⁡ x
13 7 12 9 co class x proj 1 ⁡ h ocv ⁡ h ⁡ x
14 3 6 13 cmpt class x ∈ LSubSp ⁡ h ⟼ x proj 1 ⁡ h ocv ⁡ h ⁡ x
15 cbs class Base
16 5 15 cfv class Base h
17 cmap class ↑ 𝑚
18 16 16 17 co class Base h Base h
19 2 18 cxp class V × Base h Base h
20 14 19 cin class x ∈ LSubSp ⁡ h ⟼ x proj 1 ⁡ h ocv ⁡ h ⁡ x ∩ V × Base h Base h
21 1 2 20 cmpt class h ∈ V ⟼ x ∈ LSubSp ⁡ h ⟼ x proj 1 ⁡ h ocv ⁡ h ⁡ x ∩ V × Base h Base h
22 0 21 wceq wff proj = h ∈ V ⟼ x ∈ LSubSp ⁡ h ⟼ x proj 1 ⁡ h ocv ⁡ h ⁡ x ∩ V × Base h Base h