Definition df-pj 21724

Description: Define orthogonal projection onto a subspace. This is just a wrapping of df-pj1 19656, 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‘ℎ) ↑m (Base‘ℎ)))))

Distinct variable group:   𝑥,ℎ

Detailed syntax breakdown of Definition df-pj

Step	Hyp	Ref	Expression
1		cpj 21721	. 2 class proj
2		vh	. . 3 setvar ℎ
3		cvv 3479	. . 3 class V
4		vx	. . . . 5 setvar 𝑥
5	2	cv 1538	. . . . . 6 class ℎ
6		clss 20930	. . . . . 6 class LSubSp
7	5, 6	cfv 6560	. . . . 5 class (LSubSp‘ℎ)
8	4	cv 1538	. . . . . 6 class 𝑥
9		cocv 21679	. . . . . . . 8 class ocv
10	5, 9	cfv 6560	. . . . . . 7 class (ocv‘ℎ)
11	8, 10	cfv 6560	. . . . . 6 class ((ocv‘ℎ)‘𝑥)
12		cpj1 19654	. . . . . . 7 class proj1
13	5, 12	cfv 6560	. . . . . 6 class (proj1‘ℎ)
14	8, 11, 13	co 7432	. . . . 5 class (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))
15	4, 7, 14	cmpt 5224	. . . 4 class (𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥)))
16		cbs 17248	. . . . . . 7 class Base
17	5, 16	cfv 6560	. . . . . 6 class (Base‘ℎ)
18		cmap 8867	. . . . . 6 class ↑m
19	17, 17, 18	co 7432	. . . . 5 class ((Base‘ℎ) ↑m (Base‘ℎ))
20	3, 19	cxp 5682	. . . 4 class (V × ((Base‘ℎ) ↑m (Base‘ℎ)))
21	15, 20	cin 3949	. . 3 class ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑m (Base‘ℎ))))
22	2, 3, 21	cmpt 5224	. 2 class (ℎ ∈ V ↦ ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑m (Base‘ℎ)))))
23	1, 22	wceq 1539	1 wff proj = (ℎ ∈ V ↦ ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑m (Base‘ℎ)))))

This definition is referenced by:  pjfval  21727