Metamath Proof Explorer

Theorem pjpm

Description: The projection map is a partial function from subspaces of the pre-Hilbert space to total operators. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses pjpm.v 
|- V = ( Base ` W )
pjpm.l 
|- L = ( LSubSp ` W )
pjpm.k 
|- K = ( proj ` W )
Assertion pjpm 
|- K e. ( ( V ^m V ) ^pm L )

Proof

Step Hyp Ref Expression
1 pjpm.v 
 |-  V = ( Base ` W )
2 pjpm.l 
 |-  L = ( LSubSp ` W )
3 pjpm.k 
 |-  K = ( proj ` W )
4 eqid 
 |-  ( ocv ` W ) = ( ocv ` W )
5 eqid 
 |-  ( proj1 ` W ) = ( proj1 ` W )
6 1 2 4 5 3 pjfval 
 |-  K = ( ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) ) i^i ( _V X. ( V ^m V ) ) )
7 inss1 
 |-  ( ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) C_ ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) )
8 6 7 eqsstri 
 |-  K C_ ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) )
9 funmpt 
 |-  Fun ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) )
10 funss 
 |-  ( K C_ ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) ) -> ( Fun ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) ) -> Fun K ) )
11 8 9 10 mp2 
 |-  Fun K
12 eqid 
 |-  ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) ) = ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) )
13 ovexd 
 |-  ( x e. L -> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) e. _V )
14 12 13 fmpti 
 |-  ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) ) : L --> _V
15 fssxp 
 |-  ( ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) ) : L --> _V -> ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) ) C_ ( L X. _V ) )
16 ssrin 
 |-  ( ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) ) C_ ( L X. _V ) -> ( ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) C_ ( ( L X. _V ) i^i ( _V X. ( V ^m V ) ) ) )
17 14 15 16 mp2b 
 |-  ( ( x e. L |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) C_ ( ( L X. _V ) i^i ( _V X. ( V ^m V ) ) )
18 6 17 eqsstri 
 |-  K C_ ( ( L X. _V ) i^i ( _V X. ( V ^m V ) ) )
19 inxp 
 |-  ( ( L X. _V ) i^i ( _V X. ( V ^m V ) ) ) = ( ( L i^i _V ) X. ( _V i^i ( V ^m V ) ) )
20 inv1 
 |-  ( L i^i _V ) = L
21 incom 
 |-  ( _V i^i ( V ^m V ) ) = ( ( V ^m V ) i^i _V )
22 inv1 
 |-  ( ( V ^m V ) i^i _V ) = ( V ^m V )
23 21 22 eqtri 
 |-  ( _V i^i ( V ^m V ) ) = ( V ^m V )
24 20 23 xpeq12i 
 |-  ( ( L i^i _V ) X. ( _V i^i ( V ^m V ) ) ) = ( L X. ( V ^m V ) )
25 19 24 eqtri 
 |-  ( ( L X. _V ) i^i ( _V X. ( V ^m V ) ) ) = ( L X. ( V ^m V ) )
26 18 25 sseqtri 
 |-  K C_ ( L X. ( V ^m V ) )
27 ovex 
 |-  ( V ^m V ) e. _V
28 2 fvexi 
 |-  L e. _V
29 27 28 elpm 
 |-  ( K e. ( ( V ^m V ) ^pm L ) <-> ( Fun K /\ K C_ ( L X. ( V ^m V ) ) ) )
30 11 26 29 mpbir2an 
 |-  K e. ( ( V ^m V ) ^pm L )