Metamath Proof Explorer

Theorem pjdm

Description: A subspace is in the domain of the projection function iff the subspace admits a projection decomposition of the whole space. (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 pjdm 
|- ( T e. dom K <-> ( T e. L /\ ( T P ( ._|_ ` T ) ) : V --> 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 id 
 |-  ( x = T -> x = T )
7 fveq2 
 |-  ( x = T -> ( ._|_ ` x ) = ( ._|_ ` T ) )
8 6 7 oveq12d 
 |-  ( x = T -> ( x P ( ._|_ ` x ) ) = ( T P ( ._|_ ` T ) ) )
9 8 eleq1d 
 |-  ( x = T -> ( ( x P ( ._|_ ` x ) ) e. ( V ^m V ) <-> ( T P ( ._|_ ` T ) ) e. ( V ^m V ) ) )
10 1 fvexi 
 |-  V e. _V
11 10 10 elmap 
 |-  ( ( T P ( ._|_ ` T ) ) e. ( V ^m V ) <-> ( T P ( ._|_ ` T ) ) : V --> V )
12 9 11 bitrdi 
 |-  ( x = T -> ( ( x P ( ._|_ ` x ) ) e. ( V ^m V ) <-> ( T P ( ._|_ ` T ) ) : V --> V ) )
13 cnvin 
 |-  `' ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) = ( `' ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i `' ( _V X. ( V ^m V ) ) )
14 cnvxp 
 |-  `' ( _V X. ( V ^m V ) ) = ( ( V ^m V ) X. _V )
15 14 ineq2i 
 |-  ( `' ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i `' ( _V X. ( V ^m V ) ) ) = ( `' ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( ( V ^m V ) X. _V ) )
16 13 15 eqtri 
 |-  `' ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) ) = ( `' ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( ( V ^m V ) X. _V ) )
17 1 2 3 4 5 pjfval 
 |-  K = ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) )
18 17 cnveqi 
 |-  `' K = `' ( ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( V ^m V ) ) )
19 df-res 
 |-  ( `' ( x e. L |-> ( x P ( ._|_ ` x ) ) ) |` ( V ^m V ) ) = ( `' ( x e. L |-> ( x P ( ._|_ ` x ) ) ) i^i ( ( V ^m V ) X. _V ) )
20 16 18 19 3eqtr4i 
 |-  `' K = ( `' ( x e. L |-> ( x P ( ._|_ ` x ) ) ) |` ( V ^m V ) )
21 20 rneqi 
 |-  ran `' K = ran ( `' ( x e. L |-> ( x P ( ._|_ ` x ) ) ) |` ( V ^m V ) )
22 dfdm4 
 |-  dom K = ran `' K
23 df-ima 
 |-  ( `' ( x e. L |-> ( x P ( ._|_ ` x ) ) ) " ( V ^m V ) ) = ran ( `' ( x e. L |-> ( x P ( ._|_ ` x ) ) ) |` ( V ^m V ) )
24 21 22 23 3eqtr4i 
 |-  dom K = ( `' ( x e. L |-> ( x P ( ._|_ ` x ) ) ) " ( V ^m V ) )
25 eqid 
 |-  ( x e. L |-> ( x P ( ._|_ ` x ) ) ) = ( x e. L |-> ( x P ( ._|_ ` x ) ) )
26 25 mptpreima 
 |-  ( `' ( x e. L |-> ( x P ( ._|_ ` x ) ) ) " ( V ^m V ) ) = { x e. L | ( x P ( ._|_ ` x ) ) e. ( V ^m V ) }
27 24 26 eqtri 
 |-  dom K = { x e. L | ( x P ( ._|_ ` x ) ) e. ( V ^m V ) }
28 12 27 elrab2 
 |-  ( T e. dom K <-> ( T e. L /\ ( T P ( ._|_ ` T ) ) : V --> V ) )