Metamath Proof Explorer

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 = ( h e. _V |-> ( ( x e. ( LSubSp ` h ) |-> ( x ( proj1 ` h ) ( ( ocv ` h ) ` x ) ) ) i^i ( _V X. ( ( Base ` h ) ^m ( Base ` h ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpj 
 |-  proj
1 vh 
 |-  h
2 cvv 
 |-  _V
3 vx 
 |-  x
4 clss 
 |-  LSubSp
5 1 cv 
 |-  h
6 5 4 cfv 
 |-  ( LSubSp ` h )
7 3 cv 
 |-  x
8 cpj1 
 |-  proj1
9 5 8 cfv 
 |-  ( proj1 ` h )
10 cocv 
 |-  ocv
11 5 10 cfv 
 |-  ( ocv ` h )
12 7 11 cfv 
 |-  ( ( ocv ` h ) ` x )
13 7 12 9 co 
 |-  ( x ( proj1 ` h ) ( ( ocv ` h ) ` x ) )
14 3 6 13 cmpt 
 |-  ( x e. ( LSubSp ` h ) |-> ( x ( proj1 ` h ) ( ( ocv ` h ) ` x ) ) )
15 cbs 
 |-  Base
16 5 15 cfv 
 |-  ( Base ` h )
17 cmap 
 |-  ^m
18 16 16 17 co 
 |-  ( ( Base ` h ) ^m ( Base ` h ) )
19 2 18 cxp 
 |-  ( _V X. ( ( Base ` h ) ^m ( Base ` h ) ) )
20 14 19 cin 
 |-  ( ( x e. ( LSubSp ` h ) |-> ( x ( proj1 ` h ) ( ( ocv ` h ) ` x ) ) ) i^i ( _V X. ( ( Base ` h ) ^m ( Base ` h ) ) ) )
21 1 2 20 cmpt 
 |-  ( h e. _V |-> ( ( x e. ( LSubSp ` h ) |-> ( x ( proj1 ` h ) ( ( ocv ` h ) ` x ) ) ) i^i ( _V X. ( ( Base ` h ) ^m ( Base ` h ) ) ) ) )
22 0 21 wceq 
 |-  proj = ( h e. _V |-> ( ( x e. ( LSubSp ` h ) |-> ( x ( proj1 ` h ) ( ( ocv ` h ) ` x ) ) ) i^i ( _V X. ( ( Base ` h ) ^m ( Base ` h ) ) ) ) )