Metamath Proof Explorer

Theorem offres

Description: Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion offres 
|- ( ( F e. V /\ G e. W ) -> ( ( F oF R G ) |` D ) = ( ( F |` D ) oF R ( G |` D ) ) )

Proof

Step Hyp Ref Expression
1 elinel2 
 |-  ( x e. ( ( dom F i^i dom G ) i^i D ) -> x e. D )
2 fvres 
 |-  ( x e. D -> ( ( F |` D ) ` x ) = ( F ` x ) )
3 fvres 
 |-  ( x e. D -> ( ( G |` D ) ` x ) = ( G ` x ) )
4 2 3 oveq12d 
 |-  ( x e. D -> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) = ( ( F ` x ) R ( G ` x ) ) )
5 1 4 syl 
 |-  ( x e. ( ( dom F i^i dom G ) i^i D ) -> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) = ( ( F ` x ) R ( G ` x ) ) )
6 5 mpteq2ia 
 |-  ( x e. ( ( dom F i^i dom G ) i^i D ) |-> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) ) = ( x e. ( ( dom F i^i dom G ) i^i D ) |-> ( ( F ` x ) R ( G ` x ) ) )
7 inindi 
 |-  ( D i^i ( dom F i^i dom G ) ) = ( ( D i^i dom F ) i^i ( D i^i dom G ) )
8 incom 
 |-  ( ( dom F i^i dom G ) i^i D ) = ( D i^i ( dom F i^i dom G ) )
9 dmres 
 |-  dom ( F |` D ) = ( D i^i dom F )
10 dmres 
 |-  dom ( G |` D ) = ( D i^i dom G )
11 9 10 ineq12i 
 |-  ( dom ( F |` D ) i^i dom ( G |` D ) ) = ( ( D i^i dom F ) i^i ( D i^i dom G ) )
12 7 8 11 3eqtr4ri 
 |-  ( dom ( F |` D ) i^i dom ( G |` D ) ) = ( ( dom F i^i dom G ) i^i D )
13 12 mpteq1i 
 |-  ( x e. ( dom ( F |` D ) i^i dom ( G |` D ) ) |-> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) ) = ( x e. ( ( dom F i^i dom G ) i^i D ) |-> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) )
14 resmpt3 
 |-  ( ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) |` D ) = ( x e. ( ( dom F i^i dom G ) i^i D ) |-> ( ( F ` x ) R ( G ` x ) ) )
15 6 13 14 3eqtr4ri 
 |-  ( ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) |` D ) = ( x e. ( dom ( F |` D ) i^i dom ( G |` D ) ) |-> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) )
16 offval3 
 |-  ( ( F e. V /\ G e. W ) -> ( F oF R G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )
17 16 reseq1d 
 |-  ( ( F e. V /\ G e. W ) -> ( ( F oF R G ) |` D ) = ( ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) |` D ) )
18 resexg 
 |-  ( F e. V -> ( F |` D ) e. _V )
19 resexg 
 |-  ( G e. W -> ( G |` D ) e. _V )
20 offval3 
 |-  ( ( ( F |` D ) e. _V /\ ( G |` D ) e. _V ) -> ( ( F |` D ) oF R ( G |` D ) ) = ( x e. ( dom ( F |` D ) i^i dom ( G |` D ) ) |-> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) ) )
21 18 19 20 syl2an 
 |-  ( ( F e. V /\ G e. W ) -> ( ( F |` D ) oF R ( G |` D ) ) = ( x e. ( dom ( F |` D ) i^i dom ( G |` D ) ) |-> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) ) )
22 15 17 21 3eqtr4a 
 |-  ( ( F e. V /\ G e. W ) -> ( ( F oF R G ) |` D ) = ( ( F |` D ) oF R ( G |` D ) ) )