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 ffvelrnda
 |-  ( ( 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 ) ) )