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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐶 )
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 𝑅 ( 𝐺 ∘ 𝐻 ) ) )