Metamath Proof Explorer


Theorem ofco

Description: The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014)

Ref Expression
Hypotheses ofco.1 ( 𝜑𝐹 Fn 𝐴 )
ofco.2 ( 𝜑𝐺 Fn 𝐵 )
ofco.3 ( 𝜑𝐻 : 𝐷𝐶 )
ofco.4 ( 𝜑𝐴𝑉 )
ofco.5 ( 𝜑𝐵𝑊 )
ofco.6 ( 𝜑𝐷𝑋 )
ofco.7 ( 𝐴𝐵 ) = 𝐶
Assertion ofco ( 𝜑 → ( ( 𝐹f 𝑅 𝐺 ) ∘ 𝐻 ) = ( ( 𝐹𝐻 ) ∘f 𝑅 ( 𝐺𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 ofco.1 ( 𝜑𝐹 Fn 𝐴 )
2 ofco.2 ( 𝜑𝐺 Fn 𝐵 )
3 ofco.3 ( 𝜑𝐻 : 𝐷𝐶 )
4 ofco.4 ( 𝜑𝐴𝑉 )
5 ofco.5 ( 𝜑𝐵𝑊 )
6 ofco.6 ( 𝜑𝐷𝑋 )
7 ofco.7 ( 𝐴𝐵 ) = 𝐶
8 3 ffvelrnda ( ( 𝜑𝑥𝐷 ) → ( 𝐻𝑥 ) ∈ 𝐶 )
9 3 feqmptd ( 𝜑𝐻 = ( 𝑥𝐷 ↦ ( 𝐻𝑥 ) ) )
10 eqidd ( ( 𝜑𝑦𝐴 ) → ( 𝐹𝑦 ) = ( 𝐹𝑦 ) )
11 eqidd ( ( 𝜑𝑦𝐵 ) → ( 𝐺𝑦 ) = ( 𝐺𝑦 ) )
12 1 2 4 5 7 10 11 offval ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) = ( 𝑦𝐶 ↦ ( ( 𝐹𝑦 ) 𝑅 ( 𝐺𝑦 ) ) ) )
13 fveq2 ( 𝑦 = ( 𝐻𝑥 ) → ( 𝐹𝑦 ) = ( 𝐹 ‘ ( 𝐻𝑥 ) ) )
14 fveq2 ( 𝑦 = ( 𝐻𝑥 ) → ( 𝐺𝑦 ) = ( 𝐺 ‘ ( 𝐻𝑥 ) ) )
15 13 14 oveq12d ( 𝑦 = ( 𝐻𝑥 ) → ( ( 𝐹𝑦 ) 𝑅 ( 𝐺𝑦 ) ) = ( ( 𝐹 ‘ ( 𝐻𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻𝑥 ) ) ) )
16 8 9 12 15 fmptco ( 𝜑 → ( ( 𝐹f 𝑅 𝐺 ) ∘ 𝐻 ) = ( 𝑥𝐷 ↦ ( ( 𝐹 ‘ ( 𝐻𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻𝑥 ) ) ) ) )
17 inss1 ( 𝐴𝐵 ) ⊆ 𝐴
18 7 17 eqsstrri 𝐶𝐴
19 fss ( ( 𝐻 : 𝐷𝐶𝐶𝐴 ) → 𝐻 : 𝐷𝐴 )
20 3 18 19 sylancl ( 𝜑𝐻 : 𝐷𝐴 )
21 fnfco ( ( 𝐹 Fn 𝐴𝐻 : 𝐷𝐴 ) → ( 𝐹𝐻 ) Fn 𝐷 )
22 1 20 21 syl2anc ( 𝜑 → ( 𝐹𝐻 ) Fn 𝐷 )
23 inss2 ( 𝐴𝐵 ) ⊆ 𝐵
24 7 23 eqsstrri 𝐶𝐵
25 fss ( ( 𝐻 : 𝐷𝐶𝐶𝐵 ) → 𝐻 : 𝐷𝐵 )
26 3 24 25 sylancl ( 𝜑𝐻 : 𝐷𝐵 )
27 fnfco ( ( 𝐺 Fn 𝐵𝐻 : 𝐷𝐵 ) → ( 𝐺𝐻 ) Fn 𝐷 )
28 2 26 27 syl2anc ( 𝜑 → ( 𝐺𝐻 ) Fn 𝐷 )
29 inidm ( 𝐷𝐷 ) = 𝐷
30 3 ffnd ( 𝜑𝐻 Fn 𝐷 )
31 fvco2 ( ( 𝐻 Fn 𝐷𝑥𝐷 ) → ( ( 𝐹𝐻 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐻𝑥 ) ) )
32 30 31 sylan ( ( 𝜑𝑥𝐷 ) → ( ( 𝐹𝐻 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐻𝑥 ) ) )
33 fvco2 ( ( 𝐻 Fn 𝐷𝑥𝐷 ) → ( ( 𝐺𝐻 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐻𝑥 ) ) )
34 30 33 sylan ( ( 𝜑𝑥𝐷 ) → ( ( 𝐺𝐻 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐻𝑥 ) ) )
35 22 28 6 6 29 32 34 offval ( 𝜑 → ( ( 𝐹𝐻 ) ∘f 𝑅 ( 𝐺𝐻 ) ) = ( 𝑥𝐷 ↦ ( ( 𝐹 ‘ ( 𝐻𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻𝑥 ) ) ) ) )
36 16 35 eqtr4d ( 𝜑 → ( ( 𝐹f 𝑅 𝐺 ) ∘ 𝐻 ) = ( ( 𝐹𝐻 ) ∘f 𝑅 ( 𝐺𝐻 ) ) )