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 ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ 𝐻 ) = ( ( 𝐹 ∘ 𝐻 ) ∘f 𝑅 ( 𝐺 ∘ 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 simpr1 ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → Fun 𝐻 )
2 fvimacnvi ⊢ ( ( Fun 𝐻 ∧ 𝑥 ∈ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ( dom 𝐹 ∩ dom 𝐺 ) )
3 1 2 sylan ⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ( dom 𝐹 ∩ dom 𝐺 ) )
4 1 funfnd ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → 𝐻 Fn dom 𝐻 )
5 dffn5 ⊢ ( 𝐻 Fn dom 𝐻 ↔ 𝐻 = ( 𝑥 ∈ dom 𝐻 ↦ ( 𝐻 ‘ 𝑥 ) ) )
6 4 5 sylib ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → 𝐻 = ( 𝑥 ∈ dom 𝐻 ↦ ( 𝐻 ‘ 𝑥 ) ) )
7 6 reseq1d ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( 𝐻 ↾ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( ( 𝑥 ∈ dom 𝐻 ↦ ( 𝐻 ‘ 𝑥 ) ) ↾ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) )
8 cnvimass ⊢ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ⊆ dom 𝐻
9 resmpt ⊢ ( ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ⊆ dom 𝐻 → ( ( 𝑥 ∈ dom 𝐻 ↦ ( 𝐻 ‘ 𝑥 ) ) ↾ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( 𝑥 ∈ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ↦ ( 𝐻 ‘ 𝑥 ) ) )
10 8 9 ax-mp ⊢ ( ( 𝑥 ∈ dom 𝐻 ↦ ( 𝐻 ‘ 𝑥 ) ) ↾ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( 𝑥 ∈ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ↦ ( 𝐻 ‘ 𝑥 ) )
11 7 10 eqtrdi ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( 𝐻 ↾ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( 𝑥 ∈ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ↦ ( 𝐻 ‘ 𝑥 ) ) )
12 offval3 ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑦 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐺 ‘ 𝑦 ) ) ) )
13 12 adantr ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑦 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐺 ‘ 𝑦 ) ) ) )
14 fveq2 ⊢ ( 𝑦 = ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) )
15 fveq2 ⊢ ( 𝑦 = ( 𝐻 ‘ 𝑥 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) )
16 14 15 oveq12d ⊢ ( 𝑦 = ( 𝐻 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐺 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
17 3 11 13 16 fmptco ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ ( 𝐻 ↾ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) ) = ( 𝑥 ∈ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ↦ ( ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) )
18 ovex ⊢ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ∈ V
19 18 rgenw ⊢ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ∈ V
20 eqid ⊢ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
21 20 fnmpt ⊢ ( ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ∈ V → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) Fn ( dom 𝐹 ∩ dom 𝐺 ) )
22 19 21 mp1i ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) Fn ( dom 𝐹 ∩ dom 𝐺 ) )
23 offval3 ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
24 23 adantr ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
25 24 fneq1d ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) Fn ( dom 𝐹 ∩ dom 𝐺 ) ↔ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) Fn ( dom 𝐹 ∩ dom 𝐺 ) ) )
26 22 25 mpbird ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( 𝐹 ∘f 𝑅 𝐺 ) Fn ( dom 𝐹 ∩ dom 𝐺 ) )
27 26 fndmd ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → dom ( 𝐹 ∘f 𝑅 𝐺 ) = ( dom 𝐹 ∩ dom 𝐺 ) )
28 eqimss ⊢ ( dom ( 𝐹 ∘f 𝑅 𝐺 ) = ( dom 𝐹 ∩ dom 𝐺 ) → dom ( 𝐹 ∘f 𝑅 𝐺 ) ⊆ ( dom 𝐹 ∩ dom 𝐺 ) )
29 cores2 ⊢ ( dom ( 𝐹 ∘f 𝑅 𝐺 ) ⊆ ( dom 𝐹 ∩ dom 𝐺 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ ◡ ( ◡ 𝐻 ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ 𝐻 ) )
30 27 28 29 3syl ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ ◡ ( ◡ 𝐻 ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ 𝐻 ) )
31 funcnvres2 ⊢ ( Fun 𝐻 → ◡ ( ◡ 𝐻 ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝐻 ↾ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) )
32 1 31 syl ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ◡ ( ◡ 𝐻 ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝐻 ↾ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) )
33 32 coeq2d ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ ◡ ( ◡ 𝐻 ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ ( 𝐻 ↾ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) ) )
34 30 33 eqtr3d ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ 𝐻 ) = ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ ( 𝐻 ↾ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) ) )
35 simpr2 ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( 𝐹 ∘ 𝐻 ) ∈ V )
36 simpr3 ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( 𝐺 ∘ 𝐻 ) ∈ V )
37 offval3 ⊢ ( ( ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) → ( ( 𝐹 ∘ 𝐻 ) ∘f 𝑅 ( 𝐺 ∘ 𝐻 ) ) = ( 𝑥 ∈ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ↦ ( ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) ) ) )
38 35 36 37 syl2anc ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( ( 𝐹 ∘ 𝐻 ) ∘f 𝑅 ( 𝐺 ∘ 𝐻 ) ) = ( 𝑥 ∈ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ↦ ( ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) ) ) )
39 dmco ⊢ dom ( 𝐹 ∘ 𝐻 ) = ( ◡ 𝐻 “ dom 𝐹 )
40 dmco ⊢ dom ( 𝐺 ∘ 𝐻 ) = ( ◡ 𝐻 “ dom 𝐺 )
41 39 40 ineq12i ⊢ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) = ( ( ◡ 𝐻 “ dom 𝐹 ) ∩ ( ◡ 𝐻 “ dom 𝐺 ) )
42 inpreima ⊢ ( Fun 𝐻 → ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( ( ◡ 𝐻 “ dom 𝐹 ) ∩ ( ◡ 𝐻 “ dom 𝐺 ) ) )
43 1 42 syl ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( ( ◡ 𝐻 “ dom 𝐹 ) ∩ ( ◡ 𝐻 “ dom 𝐺 ) ) )
44 41 43 eqtr4id ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) = ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) )
45 simplr1 ⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ) → Fun 𝐻 )
46 inss2 ⊢ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ⊆ dom ( 𝐺 ∘ 𝐻 )
47 dmcoss ⊢ dom ( 𝐺 ∘ 𝐻 ) ⊆ dom 𝐻
48 46 47 sstri ⊢ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ⊆ dom 𝐻
49 48 a1i ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ⊆ dom 𝐻 )
50 49 sselda ⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ) → 𝑥 ∈ dom 𝐻 )
51 fvco ⊢ ( ( Fun 𝐻 ∧ 𝑥 ∈ dom 𝐻 ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) )
52 45 50 51 syl2anc ⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) )
53 inss1 ⊢ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ⊆ dom ( 𝐹 ∘ 𝐻 )
54 dmcoss ⊢ dom ( 𝐹 ∘ 𝐻 ) ⊆ dom 𝐻
55 53 54 sstri ⊢ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ⊆ dom 𝐻
56 55 a1i ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ⊆ dom 𝐻 )
57 56 sselda ⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ) → 𝑥 ∈ dom 𝐻 )
58 fvco ⊢ ( ( Fun 𝐻 ∧ 𝑥 ∈ dom 𝐻 ) → ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) )
59 45 57 58 syl2anc ⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ) → ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) )
60 52 59 oveq12d ⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ) → ( ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
61 44 60 mpteq12dva ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( 𝑥 ∈ ( dom ( 𝐹 ∘ 𝐻 ) ∩ dom ( 𝐺 ∘ 𝐻 ) ) ↦ ( ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ↦ ( ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) )
62 38 61 eqtrd ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( ( 𝐹 ∘ 𝐻 ) ∘f 𝑅 ( 𝐺 ∘ 𝐻 ) ) = ( 𝑥 ∈ ( ◡ 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ↦ ( ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) )
63 17 34 62 3eqtr4d ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ∧ ( 𝐺 ∘ 𝐻 ) ∈ V ) ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ 𝐻 ) = ( ( 𝐹 ∘ 𝐻 ) ∘f 𝑅 ( 𝐺 ∘ 𝐻 ) ) )