Definition df-pj 20047

Description: Define orthogonal projection onto a subspace. This is just a wrapping of df-pj1 18052, 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 = ( h e. _V |-> ( ( x e. ( LSubSp ` h ) |-> ( x ( proj1 ` h ) ( ( ocv ` h ) ` x ) ) ) i^i ( _V X. ( ( Base ` h ) ^m ( Base ` h ) ) ) ) )

Distinct variable group:   x, h

Detailed syntax breakdown of Definition df-pj

Step	Hyp	Ref	Expression
1		cpj 20044	. 2 class proj
2		vh	. . 3 setvar h
3		cvv 3200	. . 3 class _V
4		vx	. . . . 5 setvar x
5	2	cv 1482	. . . . . 6 class h
6		clss 18932	. . . . . 6 class LSubSp
7	5, 6	cfv 5888	. . . . 5 class ( LSubSp ` h )
8	4	cv 1482	. . . . . 6 class x
9		cocv 20004	. . . . . . . 8 class ocv
10	5, 9	cfv 5888	. . . . . . 7 class ( ocv ` h )
11	8, 10	cfv 5888	. . . . . 6 class ( ( ocv ` h ) ` x )
12		cpj1 18050	. . . . . . 7 class proj1
13	5, 12	cfv 5888	. . . . . 6 class ( proj1 ` h )
14	8, 11, 13	co 6650	. . . . 5 class ( x ( proj1 ` h ) ( ( ocv ` h ) ` x ) )
15	4, 7, 14	cmpt 4729	. . . 4 class ( x e. ( LSubSp ` h ) |-> ( x ( proj1 ` h ) ( ( ocv ` h ) ` x ) ) )
16		cbs 15857	. . . . . . 7 class Base
17	5, 16	cfv 5888	. . . . . 6 class ( Base ` h )
18		cmap 7857	. . . . . 6 class ^m
19	17, 17, 18	co 6650	. . . . 5 class ( ( Base ` h ) ^m ( Base ` h ) )
20	3, 19	cxp 5112	. . . 4 class ( _V X. ( ( Base ` h ) ^m ( Base ` h ) ) )
21	15, 20	cin 3573	. . 3 class ( ( x e. ( LSubSp ` h ) |-> ( x ( proj1 ` h ) ( ( ocv ` h ) ` x ) ) ) i^i ( _V X. ( ( Base ` h ) ^m ( Base ` h ) ) ) )
22	2, 3, 21	cmpt 4729	. 2 class ( h e. _V |-> ( ( x e. ( LSubSp ` h ) |-> ( x ( proj1 ` h ) ( ( ocv ` h ) ` x ) ) ) i^i ( _V X. ( ( Base ` h ) ^m ( Base ` h ) ) ) ) )
23	1, 22	wceq 1483	1 wff proj = ( h e. _V |-> ( ( x e. ( LSubSp ` h ) |-> ( x ( proj1 ` h ) ( ( ocv ` h ) ` x ) ) ) i^i ( _V X. ( ( Base ` h ) ^m ( Base ` h ) ) ) ) )

This definition is referenced by:  pjfval  20050