Metamath Proof Explorer

Theorem resfval2

Description: Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses resfval.c 
|- ( ph -> F e. V )
resfval.d 
|- ( ph -> H e. W )
resfval2.g 
|- ( ph -> G e. X )
resfval2.d 
|- ( ph -> H Fn ( S X. S ) )
Assertion resfval2 
|- ( ph -> ( <. F , G >. |`f H ) = <. ( F |` S ) , ( x e. S , y e. S |-> ( ( x G y ) |` ( x H y ) ) ) >. )

Proof

Step Hyp Ref Expression
1 resfval.c 
 |-  ( ph -> F e. V )
2 resfval.d 
 |-  ( ph -> H e. W )
3 resfval2.g 
 |-  ( ph -> G e. X )
4 resfval2.d 
 |-  ( ph -> H Fn ( S X. S ) )
5 opex 
 |-  <. F , G >. e. _V
6 5 a1i 
 |-  ( ph -> <. F , G >. e. _V )
7 6 2 resfval 
 |-  ( ph -> ( <. F , G >. |`f H ) = <. ( ( 1st ` <. F , G >. ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` <. F , G >. ) ` z ) |` ( H ` z ) ) ) >. )
8 op1stg 
 |-  ( ( F e. V /\ G e. X ) -> ( 1st ` <. F , G >. ) = F )
9 1 3 8 syl2anc 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
10 4 fndmd 
 |-  ( ph -> dom H = ( S X. S ) )
11 10 dmeqd 
 |-  ( ph -> dom dom H = dom ( S X. S ) )
12 dmxpid 
 |-  dom ( S X. S ) = S
13 11 12 eqtrdi 
 |-  ( ph -> dom dom H = S )
14 9 13 reseq12d 
 |-  ( ph -> ( ( 1st ` <. F , G >. ) |` dom dom H ) = ( F |` S ) )
15 op2ndg 
 |-  ( ( F e. V /\ G e. X ) -> ( 2nd ` <. F , G >. ) = G )
16 1 3 15 syl2anc 
 |-  ( ph -> ( 2nd ` <. F , G >. ) = G )
17 16 fveq1d 
 |-  ( ph -> ( ( 2nd ` <. F , G >. ) ` z ) = ( G ` z ) )
18 17 reseq1d 
 |-  ( ph -> ( ( ( 2nd ` <. F , G >. ) ` z ) |` ( H ` z ) ) = ( ( G ` z ) |` ( H ` z ) ) )
19 10 18 mpteq12dv 
 |-  ( ph -> ( z e. dom H |-> ( ( ( 2nd ` <. F , G >. ) ` z ) |` ( H ` z ) ) ) = ( z e. ( S X. S ) |-> ( ( G ` z ) |` ( H ` z ) ) ) )
20 fveq2 
 |-  ( z = <. x , y >. -> ( G ` z ) = ( G ` <. x , y >. ) )
21 df-ov 
 |-  ( x G y ) = ( G ` <. x , y >. )
22 20 21 eqtr4di 
 |-  ( z = <. x , y >. -> ( G ` z ) = ( x G y ) )
23 fveq2 
 |-  ( z = <. x , y >. -> ( H ` z ) = ( H ` <. x , y >. ) )
24 df-ov 
 |-  ( x H y ) = ( H ` <. x , y >. )
25 23 24 eqtr4di 
 |-  ( z = <. x , y >. -> ( H ` z ) = ( x H y ) )
26 22 25 reseq12d 
 |-  ( z = <. x , y >. -> ( ( G ` z ) |` ( H ` z ) ) = ( ( x G y ) |` ( x H y ) ) )
27 26 mpompt 
 |-  ( z e. ( S X. S ) |-> ( ( G ` z ) |` ( H ` z ) ) ) = ( x e. S , y e. S |-> ( ( x G y ) |` ( x H y ) ) )
28 19 27 eqtrdi 
 |-  ( ph -> ( z e. dom H |-> ( ( ( 2nd ` <. F , G >. ) ` z ) |` ( H ` z ) ) ) = ( x e. S , y e. S |-> ( ( x G y ) |` ( x H y ) ) ) )
29 14 28 opeq12d 
 |-  ( ph -> <. ( ( 1st ` <. F , G >. ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` <. F , G >. ) ` z ) |` ( H ` z ) ) ) >. = <. ( F |` S ) , ( x e. S , y e. S |-> ( ( x G y ) |` ( x H y ) ) ) >. )
30 7 29 eqtrd 
 |-  ( ph -> ( <. F , G >. |`f H ) = <. ( F |` S ) , ( x e. S , y e. S |-> ( ( x G y ) |` ( x H y ) ) ) >. )