Definition df-pj 20446

Description: Define orthogonal projection onto a subspace. This is just a wrapping of df-pj1 18436, 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 20443	. 2 class proj
2		vh	. . 3 setvar ℎ
3		cvv 3397	. . 3 class V
4		vx	. . . . 5 setvar 𝑥
5	2	cv 1600	. . . . . 6 class ℎ
6		clss 19324	. . . . . 6 class LSubSp
7	5, 6	cfv 6135	. . . . 5 class (LSubSp‘ℎ)
8	4	cv 1600	. . . . . 6 class 𝑥
9		cocv 20403	. . . . . . . 8 class ocv
10	5, 9	cfv 6135	. . . . . . 7 class (ocv‘ℎ)
11	8, 10	cfv 6135	. . . . . 6 class ((ocv‘ℎ)‘𝑥)
12		cpj1 18434	. . . . . . 7 class proj1
13	5, 12	cfv 6135	. . . . . 6 class (proj1‘ℎ)
14	8, 11, 13	co 6922	. . . . 5 class (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))
15	4, 7, 14	cmpt 4965	. . . 4 class (𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥)))
16		cbs 16255	. . . . . . 7 class Base
17	5, 16	cfv 6135	. . . . . 6 class (Base‘ℎ)
18		cmap 8140	. . . . . 6 class ↑𝑚
19	17, 17, 18	co 6922	. . . . 5 class ((Base‘ℎ) ↑𝑚 (Base‘ℎ))
20	3, 19	cxp 5353	. . . 4 class (V × ((Base‘ℎ) ↑𝑚 (Base‘ℎ)))
21	15, 20	cin 3790	. . 3 class ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑𝑚 (Base‘ℎ))))
22	2, 3, 21	cmpt 4965	. 2 class (ℎ ∈ V ↦ ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑𝑚 (Base‘ℎ)))))
23	1, 22	wceq 1601	1 wff proj = (ℎ ∈ V ↦ ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑𝑚 (Base‘ℎ)))))

This definition is referenced by:  pjfval  20449