Definition df-pj 19866

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

Assertion

Ref	Expression
df-pj	⊢ proj = (ℎ ∈ V ↦ ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑𝑚 (Base‘ℎ)))))

Distinct variable group:   𝑥,ℎ

Detailed syntax breakdown of Definition df-pj

Step	Hyp	Ref	Expression
1		cpj 19863	. 2 class proj
2		vh	. . 3 setvar ℎ
3		cvv 3173	. . 3 class V
4		vx	. . . . 5 setvar 𝑥
5	2	cv 1474	. . . . . 6 class ℎ
6		clss 18753	. . . . . 6 class LSubSp
7	5, 6	cfv 5804	. . . . 5 class (LSubSp‘ℎ)
8	4	cv 1474	. . . . . 6 class 𝑥
9		cocv 19823	. . . . . . . 8 class ocv
10	5, 9	cfv 5804	. . . . . . 7 class (ocv‘ℎ)
11	8, 10	cfv 5804	. . . . . 6 class ((ocv‘ℎ)‘𝑥)
12		cpj1 17873	. . . . . . 7 class proj1
13	5, 12	cfv 5804	. . . . . 6 class (proj1‘ℎ)
14	8, 11, 13	co 6549	. . . . 5 class (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))
15	4, 7, 14	cmpt 4643	. . . 4 class (𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥)))
16		cbs 15695	. . . . . . 7 class Base
17	5, 16	cfv 5804	. . . . . 6 class (Base‘ℎ)
18		cmap 7744	. . . . . 6 class ↑𝑚
19	17, 17, 18	co 6549	. . . . 5 class ((Base‘ℎ) ↑𝑚 (Base‘ℎ))
20	3, 19	cxp 5036	. . . 4 class (V × ((Base‘ℎ) ↑𝑚 (Base‘ℎ)))
21	15, 20	cin 3539	. . 3 class ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑𝑚 (Base‘ℎ))))
22	2, 3, 21	cmpt 4643	. 2 class (ℎ ∈ V ↦ ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑𝑚 (Base‘ℎ)))))
23	1, 22	wceq 1475	1 wff proj = (ℎ ∈ V ↦ ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑𝑚 (Base‘ℎ)))))

This definition is referenced by:  pjfval  19869