Definition df-pj 21568

Description: Define orthogonal projection onto a subspace. This is just a wrapping of df-pj1 19549, 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 21565	. 2 class proj
2		vh	. . 3 setvar ℎ
3		cvv 3466	. . 3 class V
4		vx	. . . . 5 setvar 𝑥
5	2	cv 1532	. . . . . 6 class ℎ
6		clss 20770	. . . . . 6 class LSubSp
7	5, 6	cfv 6534	. . . . 5 class (LSubSp‘ℎ)
8	4	cv 1532	. . . . . 6 class 𝑥
9		cocv 21523	. . . . . . . 8 class ocv
10	5, 9	cfv 6534	. . . . . . 7 class (ocv‘ℎ)
11	8, 10	cfv 6534	. . . . . 6 class ((ocv‘ℎ)‘𝑥)
12		cpj1 19547	. . . . . . 7 class proj1
13	5, 12	cfv 6534	. . . . . 6 class (proj1‘ℎ)
14	8, 11, 13	co 7402	. . . . 5 class (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))
15	4, 7, 14	cmpt 5222	. . . 4 class (𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥)))
16		cbs 17145	. . . . . . 7 class Base
17	5, 16	cfv 6534	. . . . . 6 class (Base‘ℎ)
18		cmap 8817	. . . . . 6 class ↑m
19	17, 17, 18	co 7402	. . . . 5 class ((Base‘ℎ) ↑m (Base‘ℎ))
20	3, 19	cxp 5665	. . . 4 class (V × ((Base‘ℎ) ↑m (Base‘ℎ)))
21	15, 20	cin 3940	. . 3 class ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑m (Base‘ℎ))))
22	2, 3, 21	cmpt 5222	. 2 class (ℎ ∈ V ↦ ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑m (Base‘ℎ)))))
23	1, 22	wceq 1533	1 wff proj = (ℎ ∈ V ↦ ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑m (Base‘ℎ)))))

This definition is referenced by:  pjfval  21571