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 ) ) ) )
13 12 adantr 
 |-  ( ( ( 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 ) ) ) )
24 23 adantr 
 |-  ( ( ( 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 ) ) )