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 V G V Fun H F H V G H V F R f G H = F H R f G H

Proof

Step Hyp Ref Expression
1 simpr1 F V G V Fun H F H V G H V Fun H
2 fvimacnvi Fun H x H -1 dom F dom G H x dom F dom G
3 1 2 sylan F V G V Fun H F H V G H V x H -1 dom F dom G H x dom F dom G
4 1 funfnd F V G V Fun H F H V G H V H Fn dom H
5 dffn5 H Fn dom H H = x dom H H x
6 4 5 sylib F V G V Fun H F H V G H V H = x dom H H x
7 6 reseq1d F V G V Fun H F H V G H V H H -1 dom F dom G = x dom H H x H -1 dom F dom G
8 cnvimass H -1 dom F dom G dom H
9 resmpt H -1 dom F dom G dom H x dom H H x H -1 dom F dom G = x H -1 dom F dom G H x
10 8 9 ax-mp x dom H H x H -1 dom F dom G = x H -1 dom F dom G H x
11 7 10 syl6eq F V G V Fun H F H V G H V H H -1 dom F dom G = x H -1 dom F dom G H x
12 offval3 F V G V F R f G = y dom F dom G F y R G y
13 12 adantr F V G V Fun H F H V G H V F R f G = y dom F 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 V G V Fun H F H V G H V F R f G H H -1 dom F dom G = x H -1 dom F dom G F H x R G H x
18 ovex F x R G x V
19 18 rgenw x dom F dom G F x R G x V
20 eqid x dom F dom G F x R G x = x dom F dom G F x R G x
21 20 fnmpt x dom F dom G F x R G x V x dom F dom G F x R G x Fn dom F dom G
22 19 21 mp1i F V G V Fun H F H V G H V x dom F dom G F x R G x Fn dom F dom G
23 offval3 F V G V F R f G = x dom F dom G F x R G x
24 23 adantr F V G V Fun H F H V G H V F R f G = x dom F dom G F x R G x
25 24 fneq1d F V G V Fun H F H V G H V F R f G Fn dom F dom G x dom F dom G F x R G x Fn dom F dom G
26 22 25 mpbird F V G V Fun H F H V G H V F R f G Fn dom F dom G
27 26 fndmd F V G V Fun H F H V G H V dom F R f G = dom F dom G
28 eqimss dom F R f G = dom F dom G dom F R f G dom F dom G
29 cores2 dom F R f G dom F dom G F R f G H -1 dom F dom G -1 = F R f G H
30 27 28 29 3syl F V G V Fun H F H V G H V F R f G H -1 dom F dom G -1 = F R f G H
31 funcnvres2 Fun H H -1 dom F dom G -1 = H H -1 dom F dom G
32 1 31 syl F V G V Fun H F H V G H V H -1 dom F dom G -1 = H H -1 dom F dom G
33 32 coeq2d F V G V Fun H F H V G H V F R f G H -1 dom F dom G -1 = F R f G H H -1 dom F dom G
34 30 33 eqtr3d F V G V Fun H F H V G H V F R f G H = F R f G H H -1 dom F dom G
35 simpr2 F V G V Fun H F H V G H V F H V
36 simpr3 F V G V Fun H F H V G H V G H V
37 offval3 F H V G H V F H R f G H = x dom F H dom G H F H x R G H x
38 35 36 37 syl2anc F V G V Fun H F H V G H V F H R f G H = x dom F H dom G H F H x R G H x
39 inpreima Fun H H -1 dom F dom G = H -1 dom F H -1 dom G
40 1 39 syl F V G V Fun H F H V G H V H -1 dom F dom G = H -1 dom F H -1 dom G
41 dmco dom F H = H -1 dom F
42 dmco dom G H = H -1 dom G
43 41 42 ineq12i dom F H dom G H = H -1 dom F H -1 dom G
44 40 43 syl6reqr F V G V Fun H F H V G H V dom F H dom G H = H -1 dom F dom G
45 simplr1 F V G V Fun H F H V G H V x dom F H dom G H Fun H
46 inss2 dom F H dom G H dom G H
47 dmcoss dom G H dom H
48 46 47 sstri dom F H dom G H dom H
49 48 a1i F V G V Fun H F H V G H V dom F H dom G H dom H
50 49 sselda F V G V Fun H F H V G H V x dom F H dom G H x dom H
51 fvco Fun H x dom H F H x = F H x
52 45 50 51 syl2anc F V G V Fun H F H V G H V x dom F H dom G H F H x = F H x
53 inss1 dom F H dom G H dom F H
54 dmcoss dom F H dom H
55 53 54 sstri dom F H dom G H dom H
56 55 a1i F V G V Fun H F H V G H V dom F H dom G H dom H
57 56 sselda F V G V Fun H F H V G H V x dom F H dom G H x dom H
58 fvco Fun H x dom H G H x = G H x
59 45 57 58 syl2anc F V G V Fun H F H V G H V x dom F H dom G H G H x = G H x
60 52 59 oveq12d F V G V Fun H F H V G H V x dom F H dom G H F H x R G H x = F H x R G H x
61 44 60 mpteq12dva F V G V Fun H F H V G H V x dom F H dom G H F H x R G H x = x H -1 dom F dom G F H x R G H x
62 38 61 eqtrd F V G V Fun H F H V G H V F H R f G H = x H -1 dom F dom G F H x R G H x
63 17 34 62 3eqtr4d F V G V Fun H F H V G H V F R f G H = F H R f G H