This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ofres

Description: Restrict the operands of a function operation to the same domain as that of the operation itself. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Hypotheses ofres.1 
|- ( ph -> F Fn A )
ofres.2 
|- ( ph -> G Fn B )
ofres.3 
|- ( ph -> A e. V )
ofres.4 
|- ( ph -> B e. W )
ofres.5 
|- ( A i^i B ) = C
Assertion ofres 
|- ( ph -> ( F oF R G ) = ( ( F |` C ) oF R ( G |` C ) ) )

Proof

Step Hyp Ref Expression
1 ofres.1 
 |-  ( ph -> F Fn A )
2 ofres.2 
 |-  ( ph -> G Fn B )
3 ofres.3 
 |-  ( ph -> A e. V )
4 ofres.4 
 |-  ( ph -> B e. W )
5 ofres.5 
 |-  ( A i^i B ) = C
6 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
7 eqidd 
 |-  ( ( ph /\ x e. B ) -> ( G ` x ) = ( G ` x ) )
8 1 2 3 4 5 6 7 offval 
 |-  ( ph -> ( F oF R G ) = ( x e. C |-> ( ( F ` x ) R ( G ` x ) ) ) )
9 inss1 
 |-  ( A i^i B ) C_ A
10 5 9 eqsstrri 
 |-  C C_ A
11 fnssres 
 |-  ( ( F Fn A /\ C C_ A ) -> ( F |` C ) Fn C )
12 1 10 11 sylancl 
 |-  ( ph -> ( F |` C ) Fn C )
13 inss2 
 |-  ( A i^i B ) C_ B
14 5 13 eqsstrri 
 |-  C C_ B
15 fnssres 
 |-  ( ( G Fn B /\ C C_ B ) -> ( G |` C ) Fn C )
16 2 14 15 sylancl 
 |-  ( ph -> ( G |` C ) Fn C )
17 ssexg 
 |-  ( ( C C_ A /\ A e. V ) -> C e. _V )
18 10 3 17 sylancr 
 |-  ( ph -> C e. _V )
19 inidm 
 |-  ( C i^i C ) = C
20 fvres 
 |-  ( x e. C -> ( ( F |` C ) ` x ) = ( F ` x ) )
21 20 adantl 
 |-  ( ( ph /\ x e. C ) -> ( ( F |` C ) ` x ) = ( F ` x ) )
22 fvres 
 |-  ( x e. C -> ( ( G |` C ) ` x ) = ( G ` x ) )
23 22 adantl 
 |-  ( ( ph /\ x e. C ) -> ( ( G |` C ) ` x ) = ( G ` x ) )
24 12 16 18 18 19 21 23 offval 
 |-  ( ph -> ( ( F |` C ) oF R ( G |` C ) ) = ( x e. C |-> ( ( F ` x ) R ( G ` x ) ) ) )
25 8 24 eqtr4d 
 |-  ( ph -> ( F oF R G ) = ( ( F |` C ) oF R ( G |` C ) ) )