| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ofco.3 | . . . 4
⊢ (𝜑 → 𝐻:𝐷⟶𝐶) | 
| 2 | 1 | ffvelcdmda 7104 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐻‘𝑥) ∈ 𝐶) | 
| 3 | 1 | feqmptd 6977 | . . 3
⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐷 ↦ (𝐻‘𝑥))) | 
| 4 |  | ofco.1 | . . . 4
⊢ (𝜑 → 𝐹 Fn 𝐴) | 
| 5 |  | ofco.2 | . . . 4
⊢ (𝜑 → 𝐺 Fn 𝐵) | 
| 6 |  | ofco.4 | . . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 7 |  | ofco.5 | . . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑊) | 
| 8 |  | ofco.7 | . . . 4
⊢ (𝐴 ∩ 𝐵) = 𝐶 | 
| 9 |  | eqidd 2738 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) = (𝐹‘𝑦)) | 
| 10 |  | eqidd 2738 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝐺‘𝑦) = (𝐺‘𝑦)) | 
| 11 | 4, 5, 6, 7, 8, 9, 10 | offval 7706 | . . 3
⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑦 ∈ 𝐶 ↦ ((𝐹‘𝑦)𝑅(𝐺‘𝑦)))) | 
| 12 |  | fveq2 6906 | . . . 4
⊢ (𝑦 = (𝐻‘𝑥) → (𝐹‘𝑦) = (𝐹‘(𝐻‘𝑥))) | 
| 13 |  | fveq2 6906 | . . . 4
⊢ (𝑦 = (𝐻‘𝑥) → (𝐺‘𝑦) = (𝐺‘(𝐻‘𝑥))) | 
| 14 | 12, 13 | oveq12d 7449 | . . 3
⊢ (𝑦 = (𝐻‘𝑥) → ((𝐹‘𝑦)𝑅(𝐺‘𝑦)) = ((𝐹‘(𝐻‘𝑥))𝑅(𝐺‘(𝐻‘𝑥)))) | 
| 15 | 2, 3, 11, 14 | fmptco 7149 | . 2
⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) ∘ 𝐻) = (𝑥 ∈ 𝐷 ↦ ((𝐹‘(𝐻‘𝑥))𝑅(𝐺‘(𝐻‘𝑥))))) | 
| 16 |  | inss1 4237 | . . . . . 6
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | 
| 17 | 8, 16 | eqsstrri 4031 | . . . . 5
⊢ 𝐶 ⊆ 𝐴 | 
| 18 |  | fss 6752 | . . . . 5
⊢ ((𝐻:𝐷⟶𝐶 ∧ 𝐶 ⊆ 𝐴) → 𝐻:𝐷⟶𝐴) | 
| 19 | 1, 17, 18 | sylancl 586 | . . . 4
⊢ (𝜑 → 𝐻:𝐷⟶𝐴) | 
| 20 |  | fnfco 6773 | . . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐻:𝐷⟶𝐴) → (𝐹 ∘ 𝐻) Fn 𝐷) | 
| 21 | 4, 19, 20 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐹 ∘ 𝐻) Fn 𝐷) | 
| 22 |  | inss2 4238 | . . . . . 6
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 | 
| 23 | 8, 22 | eqsstrri 4031 | . . . . 5
⊢ 𝐶 ⊆ 𝐵 | 
| 24 |  | fss 6752 | . . . . 5
⊢ ((𝐻:𝐷⟶𝐶 ∧ 𝐶 ⊆ 𝐵) → 𝐻:𝐷⟶𝐵) | 
| 25 | 1, 23, 24 | sylancl 586 | . . . 4
⊢ (𝜑 → 𝐻:𝐷⟶𝐵) | 
| 26 |  | fnfco 6773 | . . . 4
⊢ ((𝐺 Fn 𝐵 ∧ 𝐻:𝐷⟶𝐵) → (𝐺 ∘ 𝐻) Fn 𝐷) | 
| 27 | 5, 25, 26 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐺 ∘ 𝐻) Fn 𝐷) | 
| 28 |  | ofco.6 | . . 3
⊢ (𝜑 → 𝐷 ∈ 𝑋) | 
| 29 |  | inidm 4227 | . . 3
⊢ (𝐷 ∩ 𝐷) = 𝐷 | 
| 30 | 1 | ffnd 6737 | . . . 4
⊢ (𝜑 → 𝐻 Fn 𝐷) | 
| 31 |  | fvco2 7006 | . . . 4
⊢ ((𝐻 Fn 𝐷 ∧ 𝑥 ∈ 𝐷) → ((𝐹 ∘ 𝐻)‘𝑥) = (𝐹‘(𝐻‘𝑥))) | 
| 32 | 30, 31 | sylan 580 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐹 ∘ 𝐻)‘𝑥) = (𝐹‘(𝐻‘𝑥))) | 
| 33 |  | fvco2 7006 | . . . 4
⊢ ((𝐻 Fn 𝐷 ∧ 𝑥 ∈ 𝐷) → ((𝐺 ∘ 𝐻)‘𝑥) = (𝐺‘(𝐻‘𝑥))) | 
| 34 | 30, 33 | sylan 580 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 ∘ 𝐻)‘𝑥) = (𝐺‘(𝐻‘𝑥))) | 
| 35 | 21, 27, 28, 28, 29, 32, 34 | offval 7706 | . 2
⊢ (𝜑 → ((𝐹 ∘ 𝐻) ∘f 𝑅(𝐺 ∘ 𝐻)) = (𝑥 ∈ 𝐷 ↦ ((𝐹‘(𝐻‘𝑥))𝑅(𝐺‘(𝐻‘𝑥))))) | 
| 36 | 15, 35 | eqtr4d 2780 | 1
⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) ∘ 𝐻) = ((𝐹 ∘ 𝐻) ∘f 𝑅(𝐺 ∘ 𝐻))) |