Metamath Proof Explorer

Theorem pjfval

Description: The value of the projection function. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses pjfval.v 
|- V = ( Base ` W )
pjfval.l 
|- L = ( LSubSp ` W )
pjfval.o 
|- ._|_ = ( ocv ` W )
pjfval.p 
|- P = ( proj1 ` W )
pjfval.k 
|- K = ( proj ` W )
Assertion pjfval 
|- K = ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) )

Proof

Step Hyp Ref Expression
1 pjfval.v 
 |-  V = ( Base ` W )
2 pjfval.l 
 |-  L = ( LSubSp ` W )
3 pjfval.o 
 |-  ._|_ = ( ocv ` W )
4 pjfval.p 
 |-  P = ( proj1 ` W )
5 pjfval.k 
 |-  K = ( proj ` W )
6 fveq2 
 |-  ( w = W -> ( LSubSp ` w ) = ( LSubSp ` W ) )
7 6 2 eqtr4di 
 |-  ( w = W -> ( LSubSp ` w ) = L )
8 fveq2 
 |-  ( w = W -> ( proj1 ` w ) = ( proj1 ` W ) )
9 8 4 eqtr4di 
 |-  ( w = W -> ( proj1 ` w ) = P )
10 eqidd 
 |-  ( w = W -> x = x )
11 fveq2 
 |-  ( w = W -> ( ocv ` w ) = ( ocv ` W ) )
12 11 3 eqtr4di 
 |-  ( w = W -> ( ocv ` w ) = ._|_ )
13 12 fveq1d 
 |-  ( w = W -> ( ( ocv ` w ) ` x ) = ( ._|_ ` x ) )
14 9 10 13 oveq123d 
 |-  ( w = W -> ( x ( proj1 ` w ) ( ( ocv ` w ) ` x ) ) = ( x P ( ._|_ ` x ) ) )
15 7 14 mpteq12dv 
 |-  ( w = W -> ( x e. ( LSubSp ` w ) |-> ( x ( proj1 ` w ) ( ( ocv ` w ) ` x ) ) ) = ( x e. L |-> ( x P ( ._|_ ` x ) ) ) )
16 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
17 16 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = V )
18 17 17 oveq12d 
 |-  ( w = W -> ( ( Base ` w ) ^m ( Base ` w ) ) = ( V ^m V ) )
19 18 xpeq2d 
 |-  ( w = W -> ( _V X. ( ( Base ` w ) ^m ( Base ` w ) ) ) = ( _V X. ( V ^m V ) ) )
20 15 19 ineq12d 
 |-  ( w = W -> ( ( x e. ( LSubSp ` w ) |-> ( x ( proj1 ` w ) ( ( ocv ` w ) ` x ) ) ) i^i ( _V X. ( ( Base ` w ) ^m ( Base ` w ) ) ) ) = ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) )
21 df-pj 
 |-  proj = ( w e. _V |-> ( ( x e. ( LSubSp ` w ) |-> ( x ( proj1 ` w ) ( ( ocv ` w ) ` x ) ) ) i^i ( _V X. ( ( Base ` w ) ^m ( Base ` w ) ) ) ) )
22 2 fvexi 
 |-  L e. _V
23 22 inex1 
 |-  ( L i^i _V ) e. _V
24 ovex 
 |-  ( V ^m V ) e. _V
25 24 inex2 
 |-  ( _V i^i ( V ^m V ) ) e. _V
26 23 25 xpex 
 |-  ( ( L i^i _V ) X. ( _V i^i ( V ^m V ) ) ) e. _V
27 eqid 
 |-  ( x e. L |-> ( x P ( ._|_ ` x ) ) ) = ( x e. L |-> ( x P ( ._|_ ` x ) ) )
28 ovexd 
 |-  ( x e. L -> ( x P ( ._|_ ` x ) ) e. _V )
29 27 28 fmpti 
 |-  ( x e. L |-> ( x P ( ._|_ ` x ) ) ) : L --> _V
30 fssxp 
 |-  ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) : L --> _V -> ( x e. L |-> ( x P ( ._|_ ` x ) ) ) C_ ( L X. _V ) )
31 ssrin 
 |-  ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) C_ ( L X. _V ) -> ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) C_ ( ( L X. _V ) i^i ( _V X. ( V ^m V ) ) ) )
32 29 30 31 mp2b 
 |-  ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) C_ ( ( L X. _V ) i^i ( _V X. ( V ^m V ) ) )
33 inxp 
 |-  ( ( L X. _V ) i^i ( _V X. ( V ^m V ) ) ) = ( ( L i^i _V ) X. ( _V i^i ( V ^m V ) ) )
34 32 33 sseqtri 
 |-  ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) C_ ( ( L i^i _V ) X. ( _V i^i ( V ^m V ) ) )
35 26 34 ssexi 
 |-  ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) e. _V
36 20 21 35 fvmpt 
 |-  ( W e. _V -> ( proj ` W ) = ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) )
37 fvprc 
 |-  ( -. W e. _V -> ( proj ` W ) = (/) )
38 inss1 
 |-  ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) C_ ( x e. L |-> ( x P ( ._|_ ` x ) ) )
39 fvprc 
 |-  ( -. W e. _V -> ( LSubSp ` W ) = (/) )
40 2 39 syl5eq 
 |-  ( -. W e. _V -> L = (/) )
41 40 mpteq1d 
 |-  ( -. W e. _V -> ( x e. L |-> ( x P ( ._|_ ` x ) ) ) = ( x e. (/) |-> ( x P ( ._|_ ` x ) ) ) )
42 mpt0 
 |-  ( x e. (/) |-> ( x P ( ._|_ ` x ) ) ) = (/)
43 41 42 eqtrdi 
 |-  ( -. W e. _V -> ( x e. L |-> ( x P ( ._|_ ` x ) ) ) = (/) )
44 sseq0 
 |-  ( ( ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) C_ ( x e. L |-> ( x P ( ._|_ ` x ) ) ) /\ ( x e. L |-> ( x P ( ._|_ ` x ) ) ) = (/) ) -> ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) = (/) )
45 38 43 44 sylancr 
 |-  ( -. W e. _V -> ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) = (/) )
46 37 45 eqtr4d 
 |-  ( -. W e. _V -> ( proj ` W ) = ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) )
47 36 46 pm2.61i 
 |-  ( proj ` W ) = ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) )
48 5 47 eqtri 
 |-  K = ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) )