# Metamath Proof Explorer

## Theorem ofco2

Description: Distribution law for the function operation and the composition of functions. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Assertion ofco2
`|- ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( ( F oF R G ) o. H ) = ( ( F o. H ) oF R ( G o. H ) ) )`

### Proof

Step Hyp Ref Expression
1 simpr1
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> Fun H )`
2 fvimacnvi
` |-  ( ( Fun H /\ x e. ( `' H " ( dom F i^i dom G ) ) ) -> ( H ` x ) e. ( dom F i^i dom G ) )`
3 1 2 sylan
` |-  ( ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) /\ x e. ( `' H " ( dom F i^i dom G ) ) ) -> ( H ` x ) e. ( dom F i^i dom G ) )`
4 1 funfnd
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> H Fn dom H )`
5 dffn5
` |-  ( H Fn dom H <-> H = ( x e. dom H |-> ( H ` x ) ) )`
6 4 5 sylib
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> H = ( x e. dom H |-> ( H ` x ) ) )`
7 6 reseq1d
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( H |` ( `' H " ( dom F i^i dom G ) ) ) = ( ( x e. dom H |-> ( H ` x ) ) |` ( `' H " ( dom F i^i dom G ) ) ) )`
8 cnvimass
` |-  ( `' H " ( dom F i^i dom G ) ) C_ dom H`
9 resmpt
` |-  ( ( `' H " ( dom F i^i dom G ) ) C_ dom H -> ( ( x e. dom H |-> ( H ` x ) ) |` ( `' H " ( dom F i^i dom G ) ) ) = ( x e. ( `' H " ( dom F i^i dom G ) ) |-> ( H ` x ) ) )`
10 8 9 ax-mp
` |-  ( ( x e. dom H |-> ( H ` x ) ) |` ( `' H " ( dom F i^i dom G ) ) ) = ( x e. ( `' H " ( dom F i^i dom G ) ) |-> ( H ` x ) )`
11 7 10 eqtrdi
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( H |` ( `' H " ( dom F i^i dom G ) ) ) = ( x e. ( `' H " ( dom F i^i dom G ) ) |-> ( H ` x ) ) )`
12 offval3
` |-  ( ( F e. _V /\ G e. _V ) -> ( F oF R G ) = ( y e. ( dom F i^i dom G ) |-> ( ( F ` y ) R ( G ` y ) ) ) )`
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( F oF R G ) = ( y e. ( dom F i^i dom G ) |-> ( ( F ` y ) R ( G ` y ) ) ) )`
14 fveq2
` |-  ( y = ( H ` x ) -> ( F ` y ) = ( F ` ( H ` x ) ) )`
15 fveq2
` |-  ( y = ( H ` x ) -> ( G ` y ) = ( G ` ( H ` x ) ) )`
16 14 15 oveq12d
` |-  ( y = ( H ` x ) -> ( ( F ` y ) R ( G ` y ) ) = ( ( F ` ( H ` x ) ) R ( G ` ( H ` x ) ) ) )`
17 3 11 13 16 fmptco
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( ( F oF R G ) o. ( H |` ( `' H " ( dom F i^i dom G ) ) ) ) = ( x e. ( `' H " ( dom F i^i dom G ) ) |-> ( ( F ` ( H ` x ) ) R ( G ` ( H ` x ) ) ) ) )`
18 ovex
` |-  ( ( F ` x ) R ( G ` x ) ) e. _V`
19 18 rgenw
` |-  A. x e. ( dom F i^i dom G ) ( ( F ` x ) R ( G ` x ) ) e. _V`
20 eqid
` |-  ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) )`
21 20 fnmpt
` |-  ( A. x e. ( dom F i^i dom G ) ( ( F ` x ) R ( G ` x ) ) e. _V -> ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) Fn ( dom F i^i dom G ) )`
22 19 21 mp1i
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) Fn ( dom F i^i dom G ) )`
23 offval3
` |-  ( ( F e. _V /\ G e. _V ) -> ( F oF R G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )`
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( F oF R G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )`
25 24 fneq1d
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( ( F oF R G ) Fn ( dom F i^i dom G ) <-> ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) Fn ( dom F i^i dom G ) ) )`
26 22 25 mpbird
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( F oF R G ) Fn ( dom F i^i dom G ) )`
27 26 fndmd
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> dom ( F oF R G ) = ( dom F i^i dom G ) )`
28 eqimss
` |-  ( dom ( F oF R G ) = ( dom F i^i dom G ) -> dom ( F oF R G ) C_ ( dom F i^i dom G ) )`
29 cores2
` |-  ( dom ( F oF R G ) C_ ( dom F i^i dom G ) -> ( ( F oF R G ) o. `' ( `' H |` ( dom F i^i dom G ) ) ) = ( ( F oF R G ) o. H ) )`
30 27 28 29 3syl
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( ( F oF R G ) o. `' ( `' H |` ( dom F i^i dom G ) ) ) = ( ( F oF R G ) o. H ) )`
31 funcnvres2
` |-  ( Fun H -> `' ( `' H |` ( dom F i^i dom G ) ) = ( H |` ( `' H " ( dom F i^i dom G ) ) ) )`
32 1 31 syl
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> `' ( `' H |` ( dom F i^i dom G ) ) = ( H |` ( `' H " ( dom F i^i dom G ) ) ) )`
33 32 coeq2d
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( ( F oF R G ) o. `' ( `' H |` ( dom F i^i dom G ) ) ) = ( ( F oF R G ) o. ( H |` ( `' H " ( dom F i^i dom G ) ) ) ) )`
34 30 33 eqtr3d
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( ( F oF R G ) o. H ) = ( ( F oF R G ) o. ( H |` ( `' H " ( dom F i^i dom G ) ) ) ) )`
35 simpr2
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( F o. H ) e. _V )`
36 simpr3
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( G o. H ) e. _V )`
37 offval3
` |-  ( ( ( F o. H ) e. _V /\ ( G o. H ) e. _V ) -> ( ( F o. H ) oF R ( G o. H ) ) = ( x e. ( dom ( F o. H ) i^i dom ( G o. H ) ) |-> ( ( ( F o. H ) ` x ) R ( ( G o. H ) ` x ) ) ) )`
38 35 36 37 syl2anc
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( ( F o. H ) oF R ( G o. H ) ) = ( x e. ( dom ( F o. H ) i^i dom ( G o. H ) ) |-> ( ( ( F o. H ) ` x ) R ( ( G o. H ) ` x ) ) ) )`
39 dmco
` |-  dom ( F o. H ) = ( `' H " dom F )`
40 dmco
` |-  dom ( G o. H ) = ( `' H " dom G )`
41 39 40 ineq12i
` |-  ( dom ( F o. H ) i^i dom ( G o. H ) ) = ( ( `' H " dom F ) i^i ( `' H " dom G ) )`
42 inpreima
` |-  ( Fun H -> ( `' H " ( dom F i^i dom G ) ) = ( ( `' H " dom F ) i^i ( `' H " dom G ) ) )`
43 1 42 syl
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( `' H " ( dom F i^i dom G ) ) = ( ( `' H " dom F ) i^i ( `' H " dom G ) ) )`
44 41 43 eqtr4id
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( dom ( F o. H ) i^i dom ( G o. H ) ) = ( `' H " ( dom F i^i dom G ) ) )`
45 simplr1
` |-  ( ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) /\ x e. ( dom ( F o. H ) i^i dom ( G o. H ) ) ) -> Fun H )`
46 inss2
` |-  ( dom ( F o. H ) i^i dom ( G o. H ) ) C_ dom ( G o. H )`
47 dmcoss
` |-  dom ( G o. H ) C_ dom H`
48 46 47 sstri
` |-  ( dom ( F o. H ) i^i dom ( G o. H ) ) C_ dom H`
49 48 a1i
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( dom ( F o. H ) i^i dom ( G o. H ) ) C_ dom H )`
50 49 sselda
` |-  ( ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) /\ x e. ( dom ( F o. H ) i^i dom ( G o. H ) ) ) -> x e. dom H )`
51 fvco
` |-  ( ( Fun H /\ x e. dom H ) -> ( ( F o. H ) ` x ) = ( F ` ( H ` x ) ) )`
52 45 50 51 syl2anc
` |-  ( ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) /\ x e. ( dom ( F o. H ) i^i dom ( G o. H ) ) ) -> ( ( F o. H ) ` x ) = ( F ` ( H ` x ) ) )`
53 inss1
` |-  ( dom ( F o. H ) i^i dom ( G o. H ) ) C_ dom ( F o. H )`
54 dmcoss
` |-  dom ( F o. H ) C_ dom H`
55 53 54 sstri
` |-  ( dom ( F o. H ) i^i dom ( G o. H ) ) C_ dom H`
56 55 a1i
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( dom ( F o. H ) i^i dom ( G o. H ) ) C_ dom H )`
57 56 sselda
` |-  ( ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) /\ x e. ( dom ( F o. H ) i^i dom ( G o. H ) ) ) -> x e. dom H )`
58 fvco
` |-  ( ( Fun H /\ x e. dom H ) -> ( ( G o. H ) ` x ) = ( G ` ( H ` x ) ) )`
59 45 57 58 syl2anc
` |-  ( ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) /\ x e. ( dom ( F o. H ) i^i dom ( G o. H ) ) ) -> ( ( G o. H ) ` x ) = ( G ` ( H ` x ) ) )`
60 52 59 oveq12d
` |-  ( ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) /\ x e. ( dom ( F o. H ) i^i dom ( G o. H ) ) ) -> ( ( ( F o. H ) ` x ) R ( ( G o. H ) ` x ) ) = ( ( F ` ( H ` x ) ) R ( G ` ( H ` x ) ) ) )`
61 44 60 mpteq12dva
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( x e. ( dom ( F o. H ) i^i dom ( G o. H ) ) |-> ( ( ( F o. H ) ` x ) R ( ( G o. H ) ` x ) ) ) = ( x e. ( `' H " ( dom F i^i dom G ) ) |-> ( ( F ` ( H ` x ) ) R ( G ` ( H ` x ) ) ) ) )`
62 38 61 eqtrd
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( ( F o. H ) oF R ( G o. H ) ) = ( x e. ( `' H " ( dom F i^i dom G ) ) |-> ( ( F ` ( H ` x ) ) R ( G ` ( H ` x ) ) ) ) )`
63 17 34 62 3eqtr4d
` |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun H /\ ( F o. H ) e. _V /\ ( G o. H ) e. _V ) ) -> ( ( F oF R G ) o. H ) = ( ( F o. H ) oF R ( G o. H ) ) )`