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 = ( ℎ ∈ V ↦ ( ( 𝑥 ∈ ( LSubSp ‘ ℎ ) ↦ ( 𝑥 ( proj1 ‘ ℎ ) ( ( ocv ‘ ℎ ) ‘ 𝑥 ) ) ) ∩ ( V × ( ( Base ‘ ℎ ) ↑m ( Base ‘ ℎ ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpj	⊢ proj
1		vh	⊢ ℎ
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		clss	⊢ LSubSp
5	1	cv	⊢ ℎ
6	5 4	cfv	⊢ ( LSubSp ‘ ℎ )
7	3	cv	⊢ 𝑥
8		cpj1	⊢ proj1
9	5 8	cfv	⊢ ( proj1 ‘ ℎ )
10		cocv	⊢ ocv
11	5 10	cfv	⊢ ( ocv ‘ ℎ )
12	7 11	cfv	⊢ ( ( ocv ‘ ℎ ) ‘ 𝑥 )
13	7 12 9	co	⊢ ( 𝑥 ( proj1 ‘ ℎ ) ( ( ocv ‘ ℎ ) ‘ 𝑥 ) )
14	3 6 13	cmpt	⊢ ( 𝑥 ∈ ( LSubSp ‘ ℎ ) ↦ ( 𝑥 ( proj1 ‘ ℎ ) ( ( ocv ‘ ℎ ) ‘ 𝑥 ) ) )
15		cbs	⊢ Base
16	5 15	cfv	⊢ ( Base ‘ ℎ )
17		cmap	⊢ ↑m
18	16 16 17	co	⊢ ( ( Base ‘ ℎ ) ↑m ( Base ‘ ℎ ) )
19	2 18	cxp	⊢ ( V × ( ( Base ‘ ℎ ) ↑m ( Base ‘ ℎ ) ) )
20	14 19	cin	⊢ ( ( 𝑥 ∈ ( LSubSp ‘ ℎ ) ↦ ( 𝑥 ( proj1 ‘ ℎ ) ( ( ocv ‘ ℎ ) ‘ 𝑥 ) ) ) ∩ ( V × ( ( Base ‘ ℎ ) ↑m ( Base ‘ ℎ ) ) ) )
21	1 2 20	cmpt	⊢ ( ℎ ∈ V ↦ ( ( 𝑥 ∈ ( LSubSp ‘ ℎ ) ↦ ( 𝑥 ( proj1 ‘ ℎ ) ( ( ocv ‘ ℎ ) ‘ 𝑥 ) ) ) ∩ ( V × ( ( Base ‘ ℎ ) ↑m ( Base ‘ ℎ ) ) ) ) )
22	0 21	wceq	⊢ proj = ( ℎ ∈ V ↦ ( ( 𝑥 ∈ ( LSubSp ‘ ℎ ) ↦ ( 𝑥 ( proj1 ‘ ℎ ) ( ( ocv ‘ ℎ ) ‘ 𝑥 ) ) ) ∩ ( V × ( ( Base ‘ ℎ ) ↑m ( Base ‘ ℎ ) ) ) ) )