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 𝑅 ( 𝐺 ∘ 𝐻 ) ) ) |