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

Metamath Proof Explorer

Theorem ofco

Description: The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014)

Ref Expression
Hypotheses ofco.1 
|- ( ph -> F Fn A )
ofco.2 
|- ( ph -> G Fn B )
ofco.3 
|- ( ph -> H : D --> C )
ofco.4 
|- ( ph -> A e. V )
ofco.5 
|- ( ph -> B e. W )
ofco.6 
|- ( ph -> D e. X )
ofco.7 
|- ( A i^i B ) = C
Assertion ofco 
|- ( ph -> ( ( F oF R G ) o. H ) = ( ( F o. H ) oF R ( G o. H ) ) )

Proof

Step Hyp Ref Expression
1 ofco.1 
 |-  ( ph -> F Fn A )
2 ofco.2 
 |-  ( ph -> G Fn B )
3 ofco.3 
 |-  ( ph -> H : D --> C )
4 ofco.4 
 |-  ( ph -> A e. V )
5 ofco.5 
 |-  ( ph -> B e. W )
6 ofco.6 
 |-  ( ph -> D e. X )
7 ofco.7 
 |-  ( A i^i B ) = C
8 3 ffvelcdmda 
 |-  ( ( ph /\ x e. D ) -> ( H ` x ) e. C )
9 3 feqmptd 
 |-  ( ph -> H = ( x e. D |-> ( H ` x ) ) )
10 eqidd 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) = ( F ` y ) )
11 eqidd 
 |-  ( ( ph /\ y e. B ) -> ( G ` y ) = ( G ` y ) )
12 1 2 4 5 7 10 11 offval 
 |-  ( ph -> ( F oF R G ) = ( y e. C |-> ( ( F ` y ) R ( G ` y ) ) ) )
13 fveq2 
 |-  ( y = ( H ` x ) -> ( F ` y ) = ( F ` ( H ` x ) ) )
14 fveq2 
 |-  ( y = ( H ` x ) -> ( G ` y ) = ( G ` ( H ` x ) ) )
15 13 14 oveq12d 
 |-  ( y = ( H ` x ) -> ( ( F ` y ) R ( G ` y ) ) = ( ( F ` ( H ` x ) ) R ( G ` ( H ` x ) ) ) )
16 8 9 12 15 fmptco 
 |-  ( ph -> ( ( F oF R G ) o. H ) = ( x e. D |-> ( ( F ` ( H ` x ) ) R ( G ` ( H ` x ) ) ) ) )
17 inss1 
 |-  ( A i^i B ) C_ A
18 7 17 eqsstrri 
 |-  C C_ A
19 fss 
 |-  ( ( H : D --> C /\ C C_ A ) -> H : D --> A )
20 3 18 19 sylancl 
 |-  ( ph -> H : D --> A )
21 fnfco 
 |-  ( ( F Fn A /\ H : D --> A ) -> ( F o. H ) Fn D )
22 1 20 21 syl2anc 
 |-  ( ph -> ( F o. H ) Fn D )
23 inss2 
 |-  ( A i^i B ) C_ B
24 7 23 eqsstrri 
 |-  C C_ B
25 fss 
 |-  ( ( H : D --> C /\ C C_ B ) -> H : D --> B )
26 3 24 25 sylancl 
 |-  ( ph -> H : D --> B )
27 fnfco 
 |-  ( ( G Fn B /\ H : D --> B ) -> ( G o. H ) Fn D )
28 2 26 27 syl2anc 
 |-  ( ph -> ( G o. H ) Fn D )
29 inidm 
 |-  ( D i^i D ) = D
30 3 ffnd 
 |-  ( ph -> H Fn D )
31 fvco2 
 |-  ( ( H Fn D /\ x e. D ) -> ( ( F o. H ) ` x ) = ( F ` ( H ` x ) ) )
32 30 31 sylan 
 |-  ( ( ph /\ x e. D ) -> ( ( F o. H ) ` x ) = ( F ` ( H ` x ) ) )
33 fvco2 
 |-  ( ( H Fn D /\ x e. D ) -> ( ( G o. H ) ` x ) = ( G ` ( H ` x ) ) )
34 30 33 sylan 
 |-  ( ( ph /\ x e. D ) -> ( ( G o. H ) ` x ) = ( G ` ( H ` x ) ) )
35 22 28 6 6 29 32 34 offval 
 |-  ( ph -> ( ( F o. H ) oF R ( G o. H ) ) = ( x e. D |-> ( ( F ` ( H ` x ) ) R ( G ` ( H ` x ) ) ) ) )
36 16 35 eqtr4d 
 |-  ( ph -> ( ( F oF R G ) o. H ) = ( ( F o. H ) oF R ( G o. H ) ) )