# 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 ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \left({F}{{R}}_{f}{G}\right)\circ {H}=\left({F}\circ {H}\right){{R}}_{f}\left({G}\circ {H}\right)$

### Proof

Step Hyp Ref Expression
1 simpr1 ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \mathrm{Fun}{H}$
2 fvimacnvi ${⊢}\left(\mathrm{Fun}{H}\wedge {x}\in {{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]\right)\to {H}\left({x}\right)\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)$
3 1 2 sylan ${⊢}\left(\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\wedge {x}\in {{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]\right)\to {H}\left({x}\right)\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)$
4 1 funfnd ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to {H}Fn\mathrm{dom}{H}$
5 dffn5 ${⊢}{H}Fn\mathrm{dom}{H}↔{H}=\left({x}\in \mathrm{dom}{H}⟼{H}\left({x}\right)\right)$
6 4 5 sylib ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to {H}=\left({x}\in \mathrm{dom}{H}⟼{H}\left({x}\right)\right)$
7 6 reseq1d ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to {{H}↾}_{{{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]}={\left({x}\in \mathrm{dom}{H}⟼{H}\left({x}\right)\right)↾}_{{{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]}$
8 cnvimass ${⊢}{{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]\subseteq \mathrm{dom}{H}$
9 resmpt ${⊢}{{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]\subseteq \mathrm{dom}{H}\to {\left({x}\in \mathrm{dom}{H}⟼{H}\left({x}\right)\right)↾}_{{{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]}=\left({x}\in {{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]⟼{H}\left({x}\right)\right)$
10 8 9 ax-mp ${⊢}{\left({x}\in \mathrm{dom}{H}⟼{H}\left({x}\right)\right)↾}_{{{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]}=\left({x}\in {{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]⟼{H}\left({x}\right)\right)$
11 7 10 syl6eq ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to {{H}↾}_{{{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]}=\left({x}\in {{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]⟼{H}\left({x}\right)\right)$
12 offval3 ${⊢}\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\to {F}{{R}}_{f}{G}=\left({y}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)⟼{F}\left({y}\right){R}{G}\left({y}\right)\right)$
13 12 adantr ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to {F}{{R}}_{f}{G}=\left({y}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)⟼{F}\left({y}\right){R}{G}\left({y}\right)\right)$
14 fveq2 ${⊢}{y}={H}\left({x}\right)\to {F}\left({y}\right)={F}\left({H}\left({x}\right)\right)$
15 fveq2 ${⊢}{y}={H}\left({x}\right)\to {G}\left({y}\right)={G}\left({H}\left({x}\right)\right)$
16 14 15 oveq12d ${⊢}{y}={H}\left({x}\right)\to {F}\left({y}\right){R}{G}\left({y}\right)={F}\left({H}\left({x}\right)\right){R}{G}\left({H}\left({x}\right)\right)$
17 3 11 13 16 fmptco ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \left({F}{{R}}_{f}{G}\right)\circ \left({{H}↾}_{{{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]}\right)=\left({x}\in {{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]⟼{F}\left({H}\left({x}\right)\right){R}{G}\left({H}\left({x}\right)\right)\right)$
18 ovex ${⊢}{F}\left({x}\right){R}{G}\left({x}\right)\in \mathrm{V}$
19 18 rgenw ${⊢}\forall {x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){R}{G}\left({x}\right)\in \mathrm{V}$
20 eqid ${⊢}\left({x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)⟼{F}\left({x}\right){R}{G}\left({x}\right)\right)=\left({x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)⟼{F}\left({x}\right){R}{G}\left({x}\right)\right)$
21 20 fnmpt ${⊢}\forall {x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){R}{G}\left({x}\right)\in \mathrm{V}\to \left({x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)⟼{F}\left({x}\right){R}{G}\left({x}\right)\right)Fn\left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)$
22 19 21 mp1i ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \left({x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)⟼{F}\left({x}\right){R}{G}\left({x}\right)\right)Fn\left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)$
23 offval3 ${⊢}\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\to {F}{{R}}_{f}{G}=\left({x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)⟼{F}\left({x}\right){R}{G}\left({x}\right)\right)$
24 23 adantr ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to {F}{{R}}_{f}{G}=\left({x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)⟼{F}\left({x}\right){R}{G}\left({x}\right)\right)$
25 24 fneq1d ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \left(\left({F}{{R}}_{f}{G}\right)Fn\left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)↔\left({x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)⟼{F}\left({x}\right){R}{G}\left({x}\right)\right)Fn\left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)\right)$
26 22 25 mpbird ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \left({F}{{R}}_{f}{G}\right)Fn\left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)$
27 26 fndmd ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \mathrm{dom}\left({F}{{R}}_{f}{G}\right)=\mathrm{dom}{F}\cap \mathrm{dom}{G}$
28 eqimss ${⊢}\mathrm{dom}\left({F}{{R}}_{f}{G}\right)=\mathrm{dom}{F}\cap \mathrm{dom}{G}\to \mathrm{dom}\left({F}{{R}}_{f}{G}\right)\subseteq \mathrm{dom}{F}\cap \mathrm{dom}{G}$
29 cores2 ${⊢}\mathrm{dom}\left({F}{{R}}_{f}{G}\right)\subseteq \mathrm{dom}{F}\cap \mathrm{dom}{G}\to \left({F}{{R}}_{f}{G}\right)\circ {\left({{{H}}^{-1}↾}_{\left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)}\right)}^{-1}=\left({F}{{R}}_{f}{G}\right)\circ {H}$
30 27 28 29 3syl ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \left({F}{{R}}_{f}{G}\right)\circ {\left({{{H}}^{-1}↾}_{\left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)}\right)}^{-1}=\left({F}{{R}}_{f}{G}\right)\circ {H}$
31 funcnvres2 ${⊢}\mathrm{Fun}{H}\to {\left({{{H}}^{-1}↾}_{\left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)}\right)}^{-1}={{H}↾}_{{{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]}$
32 1 31 syl ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to {\left({{{H}}^{-1}↾}_{\left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)}\right)}^{-1}={{H}↾}_{{{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]}$
33 32 coeq2d ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \left({F}{{R}}_{f}{G}\right)\circ {\left({{{H}}^{-1}↾}_{\left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)}\right)}^{-1}=\left({F}{{R}}_{f}{G}\right)\circ \left({{H}↾}_{{{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]}\right)$
34 30 33 eqtr3d ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \left({F}{{R}}_{f}{G}\right)\circ {H}=\left({F}{{R}}_{f}{G}\right)\circ \left({{H}↾}_{{{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]}\right)$
35 simpr2 ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to {F}\circ {H}\in \mathrm{V}$
36 simpr3 ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to {G}\circ {H}\in \mathrm{V}$
37 offval3 ${⊢}\left({F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\to \left({F}\circ {H}\right){{R}}_{f}\left({G}\circ {H}\right)=\left({x}\in \left(\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\right)⟼\left({F}\circ {H}\right)\left({x}\right){R}\left({G}\circ {H}\right)\left({x}\right)\right)$
38 35 36 37 syl2anc ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \left({F}\circ {H}\right){{R}}_{f}\left({G}\circ {H}\right)=\left({x}\in \left(\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\right)⟼\left({F}\circ {H}\right)\left({x}\right){R}\left({G}\circ {H}\right)\left({x}\right)\right)$
39 inpreima ${⊢}\mathrm{Fun}{H}\to {{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]={{H}}^{-1}\left[\mathrm{dom}{F}\right]\cap {{H}}^{-1}\left[\mathrm{dom}{G}\right]$
40 1 39 syl ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to {{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]={{H}}^{-1}\left[\mathrm{dom}{F}\right]\cap {{H}}^{-1}\left[\mathrm{dom}{G}\right]$
41 dmco ${⊢}\mathrm{dom}\left({F}\circ {H}\right)={{H}}^{-1}\left[\mathrm{dom}{F}\right]$
42 dmco ${⊢}\mathrm{dom}\left({G}\circ {H}\right)={{H}}^{-1}\left[\mathrm{dom}{G}\right]$
43 41 42 ineq12i ${⊢}\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)={{H}}^{-1}\left[\mathrm{dom}{F}\right]\cap {{H}}^{-1}\left[\mathrm{dom}{G}\right]$
44 40 43 syl6reqr ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)={{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]$
45 simplr1 ${⊢}\left(\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\wedge {x}\in \left(\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\right)\right)\to \mathrm{Fun}{H}$
46 inss2 ${⊢}\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\subseteq \mathrm{dom}\left({G}\circ {H}\right)$
47 dmcoss ${⊢}\mathrm{dom}\left({G}\circ {H}\right)\subseteq \mathrm{dom}{H}$
48 46 47 sstri ${⊢}\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\subseteq \mathrm{dom}{H}$
49 48 a1i ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\subseteq \mathrm{dom}{H}$
50 49 sselda ${⊢}\left(\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\wedge {x}\in \left(\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\right)\right)\to {x}\in \mathrm{dom}{H}$
51 fvco ${⊢}\left(\mathrm{Fun}{H}\wedge {x}\in \mathrm{dom}{H}\right)\to \left({F}\circ {H}\right)\left({x}\right)={F}\left({H}\left({x}\right)\right)$
52 45 50 51 syl2anc ${⊢}\left(\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\wedge {x}\in \left(\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\right)\right)\to \left({F}\circ {H}\right)\left({x}\right)={F}\left({H}\left({x}\right)\right)$
53 inss1 ${⊢}\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\subseteq \mathrm{dom}\left({F}\circ {H}\right)$
54 dmcoss ${⊢}\mathrm{dom}\left({F}\circ {H}\right)\subseteq \mathrm{dom}{H}$
55 53 54 sstri ${⊢}\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\subseteq \mathrm{dom}{H}$
56 55 a1i ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\subseteq \mathrm{dom}{H}$
57 56 sselda ${⊢}\left(\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\wedge {x}\in \left(\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\right)\right)\to {x}\in \mathrm{dom}{H}$
58 fvco ${⊢}\left(\mathrm{Fun}{H}\wedge {x}\in \mathrm{dom}{H}\right)\to \left({G}\circ {H}\right)\left({x}\right)={G}\left({H}\left({x}\right)\right)$
59 45 57 58 syl2anc ${⊢}\left(\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\wedge {x}\in \left(\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\right)\right)\to \left({G}\circ {H}\right)\left({x}\right)={G}\left({H}\left({x}\right)\right)$
60 52 59 oveq12d ${⊢}\left(\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\wedge {x}\in \left(\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\right)\right)\to \left({F}\circ {H}\right)\left({x}\right){R}\left({G}\circ {H}\right)\left({x}\right)={F}\left({H}\left({x}\right)\right){R}{G}\left({H}\left({x}\right)\right)$
61 44 60 mpteq12dva ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \left({x}\in \left(\mathrm{dom}\left({F}\circ {H}\right)\cap \mathrm{dom}\left({G}\circ {H}\right)\right)⟼\left({F}\circ {H}\right)\left({x}\right){R}\left({G}\circ {H}\right)\left({x}\right)\right)=\left({x}\in {{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]⟼{F}\left({H}\left({x}\right)\right){R}{G}\left({H}\left({x}\right)\right)\right)$
62 38 61 eqtrd ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \left({F}\circ {H}\right){{R}}_{f}\left({G}\circ {H}\right)=\left({x}\in {{H}}^{-1}\left[\mathrm{dom}{F}\cap \mathrm{dom}{G}\right]⟼{F}\left({H}\left({x}\right)\right){R}{G}\left({H}\left({x}\right)\right)\right)$
63 17 34 62 3eqtr4d ${⊢}\left(\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\wedge \left(\mathrm{Fun}{H}\wedge {F}\circ {H}\in \mathrm{V}\wedge {G}\circ {H}\in \mathrm{V}\right)\right)\to \left({F}{{R}}_{f}{G}\right)\circ {H}=\left({F}\circ {H}\right){{R}}_{f}\left({G}\circ {H}\right)$