Metamath Proof Explorer

Theorem pjfval2

Description: Value of the projection map with implicit domain. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses pjfval2.o 
|- ._|_ = ( ocv ` W )
pjfval2.p 
|- P = ( proj1 ` W )
pjfval2.k 
|- K = ( proj ` W )
Assertion pjfval2 
|- K = ( x e. dom K |-> ( x P ( ._|_ ` x ) ) )

Proof

Step Hyp Ref Expression
1 pjfval2.o 
 |-  ._|_ = ( ocv ` W )
2 pjfval2.p 
 |-  P = ( proj1 ` W )
3 pjfval2.k 
 |-  K = ( proj ` W )
4 df-mpt 
 |-  ( x e. ( LSubSp ` W ) |-> ( x P ( ._|_ ` x ) ) ) = { <. x , y >. | ( x e. ( LSubSp ` W ) /\ y = ( x P ( ._|_ ` x ) ) ) }
5 df-xp 
 |-  ( _V X. ( ( Base ` W ) ^m ( Base ` W ) ) ) = { <. x , y >. | ( x e. _V /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) }
6 4 5 ineq12i 
 |-  ( ( x e. ( LSubSp ` W ) |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( ( Base ` W ) ^m ( Base ` W ) ) ) ) = ( { <. x , y >. | ( x e. ( LSubSp ` W ) /\ y = ( x P ( ._|_ ` x ) ) ) } i^i { <. x , y >. | ( x e. _V /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) } )
7 eqid 
 |-  ( Base ` W ) = ( Base ` W )
8 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
9 7 8 1 2 3 pjfval 
 |-  K = ( ( x e. ( LSubSp ` W ) |-> ( x P ( ._|_ ` x ) ) ) i^i ( _V X. ( ( Base ` W ) ^m ( Base ` W ) ) ) )
10 7 8 1 2 3 pjdm 
 |-  ( x e. dom K <-> ( x e. ( LSubSp ` W ) /\ ( x P ( ._|_ ` x ) ) : ( Base ` W ) --> ( Base ` W ) ) )
11 eleq1 
 |-  ( y = ( x P ( ._|_ ` x ) ) -> ( y e. ( ( Base ` W ) ^m ( Base ` W ) ) <-> ( x P ( ._|_ ` x ) ) e. ( ( Base ` W ) ^m ( Base ` W ) ) ) )
12 fvex 
 |-  ( Base ` W ) e. _V
13 12 12 elmap 
 |-  ( ( x P ( ._|_ ` x ) ) e. ( ( Base ` W ) ^m ( Base ` W ) ) <-> ( x P ( ._|_ ` x ) ) : ( Base ` W ) --> ( Base ` W ) )
14 11 13 bitr2di 
 |-  ( y = ( x P ( ._|_ ` x ) ) -> ( ( x P ( ._|_ ` x ) ) : ( Base ` W ) --> ( Base ` W ) <-> y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) )
15 14 anbi2d 
 |-  ( y = ( x P ( ._|_ ` x ) ) -> ( ( x e. ( LSubSp ` W ) /\ ( x P ( ._|_ ` x ) ) : ( Base ` W ) --> ( Base ` W ) ) <-> ( x e. ( LSubSp ` W ) /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) ) )
16 10 15 syl5bb 
 |-  ( y = ( x P ( ._|_ ` x ) ) -> ( x e. dom K <-> ( x e. ( LSubSp ` W ) /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) ) )
17 16 pm5.32ri 
 |-  ( ( x e. dom K /\ y = ( x P ( ._|_ ` x ) ) ) <-> ( ( x e. ( LSubSp ` W ) /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) /\ y = ( x P ( ._|_ ` x ) ) ) )
18 an32 
 |-  ( ( ( x e. ( LSubSp ` W ) /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) /\ y = ( x P ( ._|_ ` x ) ) ) <-> ( ( x e. ( LSubSp ` W ) /\ y = ( x P ( ._|_ ` x ) ) ) /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) )
19 vex 
 |-  x e. _V
20 19 biantrur 
 |-  ( y e. ( ( Base ` W ) ^m ( Base ` W ) ) <-> ( x e. _V /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) )
21 20 anbi2i 
 |-  ( ( ( x e. ( LSubSp ` W ) /\ y = ( x P ( ._|_ ` x ) ) ) /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) <-> ( ( x e. ( LSubSp ` W ) /\ y = ( x P ( ._|_ ` x ) ) ) /\ ( x e. _V /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) ) )
22 17 18 21 3bitri 
 |-  ( ( x e. dom K /\ y = ( x P ( ._|_ ` x ) ) ) <-> ( ( x e. ( LSubSp ` W ) /\ y = ( x P ( ._|_ ` x ) ) ) /\ ( x e. _V /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) ) )
23 22 opabbii 
 |-  { <. x , y >. | ( x e. dom K /\ y = ( x P ( ._|_ ` x ) ) ) } = { <. x , y >. | ( ( x e. ( LSubSp ` W ) /\ y = ( x P ( ._|_ ` x ) ) ) /\ ( x e. _V /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) ) }
24 df-mpt 
 |-  ( x e. dom K |-> ( x P ( ._|_ ` x ) ) ) = { <. x , y >. | ( x e. dom K /\ y = ( x P ( ._|_ ` x ) ) ) }
25 inopab 
 |-  ( { <. x , y >. | ( x e. ( LSubSp ` W ) /\ y = ( x P ( ._|_ ` x ) ) ) } i^i { <. x , y >. | ( x e. _V /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) } ) = { <. x , y >. | ( ( x e. ( LSubSp ` W ) /\ y = ( x P ( ._|_ ` x ) ) ) /\ ( x e. _V /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) ) }
26 23 24 25 3eqtr4i 
 |-  ( x e. dom K |-> ( x P ( ._|_ ` x ) ) ) = ( { <. x , y >. | ( x e. ( LSubSp ` W ) /\ y = ( x P ( ._|_ ` x ) ) ) } i^i { <. x , y >. | ( x e. _V /\ y e. ( ( Base ` W ) ^m ( Base ` W ) ) ) } )
27 6 9 26 3eqtr4i 
 |-  K = ( x e. dom K |-> ( x P ( ._|_ ` x ) ) )