Step | Hyp | Ref
| Expression |
1 | | ofco.3 |
. . . 4
⊢ (φ → 𝐻:𝐷⟶𝐶) |
2 | 1 | ffvelrnda 5245 |
. . 3
⊢ ((φ ∧ x ∈ 𝐷) → (𝐻‘x) ∈ 𝐶) |
3 | 1 | feqmptd 5169 |
. . 3
⊢ (φ → 𝐻 = (x
∈ 𝐷 ↦ (𝐻‘x))) |
4 | | ofco.1 |
. . . 4
⊢ (φ → 𝐹 Fn A) |
5 | | ofco.2 |
. . . 4
⊢ (φ → 𝐺 Fn B) |
6 | | ofco.4 |
. . . 4
⊢ (φ → A ∈ 𝑉) |
7 | | ofco.5 |
. . . 4
⊢ (φ → B ∈ 𝑊) |
8 | | ofco.7 |
. . . 4
⊢ (A ∩ B) =
𝐶 |
9 | | eqidd 2038 |
. . . 4
⊢ ((φ ∧ y ∈ A) → (𝐹‘y) = (𝐹‘y)) |
10 | | eqidd 2038 |
. . . 4
⊢ ((φ ∧ y ∈ B) → (𝐺‘y) = (𝐺‘y)) |
11 | 4, 5, 6, 7, 8, 9, 10 | offval 5661 |
. . 3
⊢ (φ → (𝐹 ∘𝑓 𝑅𝐺) = (y
∈ 𝐶 ↦ ((𝐹‘y)𝑅(𝐺‘y)))) |
12 | | fveq2 5121 |
. . . 4
⊢ (y = (𝐻‘x) → (𝐹‘y) = (𝐹‘(𝐻‘x))) |
13 | | fveq2 5121 |
. . . 4
⊢ (y = (𝐻‘x) → (𝐺‘y) = (𝐺‘(𝐻‘x))) |
14 | 12, 13 | oveq12d 5473 |
. . 3
⊢ (y = (𝐻‘x) → ((𝐹‘y)𝑅(𝐺‘y)) = ((𝐹‘(𝐻‘x))𝑅(𝐺‘(𝐻‘x)))) |
15 | 2, 3, 11, 14 | fmptco 5273 |
. 2
⊢ (φ → ((𝐹 ∘𝑓 𝑅𝐺) ∘ 𝐻) = (x
∈ 𝐷 ↦ ((𝐹‘(𝐻‘x))𝑅(𝐺‘(𝐻‘x))))) |
16 | | inss1 3151 |
. . . . . 6
⊢ (A ∩ B)
⊆ A |
17 | 8, 16 | eqsstr3i 2970 |
. . . . 5
⊢ 𝐶 ⊆ A |
18 | | fss 4997 |
. . . . 5
⊢ ((𝐻:𝐷⟶𝐶 ∧ 𝐶 ⊆ A) → 𝐻:𝐷⟶A) |
19 | 1, 17, 18 | sylancl 392 |
. . . 4
⊢ (φ → 𝐻:𝐷⟶A) |
20 | | fnfco 5008 |
. . . 4
⊢ ((𝐹 Fn A ∧ 𝐻:𝐷⟶A) → (𝐹 ∘ 𝐻) Fn 𝐷) |
21 | 4, 19, 20 | syl2anc 391 |
. . 3
⊢ (φ → (𝐹 ∘ 𝐻) Fn 𝐷) |
22 | | inss2 3152 |
. . . . . 6
⊢ (A ∩ B)
⊆ B |
23 | 8, 22 | eqsstr3i 2970 |
. . . . 5
⊢ 𝐶 ⊆ B |
24 | | fss 4997 |
. . . . 5
⊢ ((𝐻:𝐷⟶𝐶 ∧ 𝐶 ⊆ B) → 𝐻:𝐷⟶B) |
25 | 1, 23, 24 | sylancl 392 |
. . . 4
⊢ (φ → 𝐻:𝐷⟶B) |
26 | | fnfco 5008 |
. . . 4
⊢ ((𝐺 Fn B ∧ 𝐻:𝐷⟶B) → (𝐺 ∘ 𝐻) Fn 𝐷) |
27 | 5, 25, 26 | syl2anc 391 |
. . 3
⊢ (φ → (𝐺 ∘ 𝐻) Fn 𝐷) |
28 | | ofco.6 |
. . 3
⊢ (φ → 𝐷 ∈ 𝑋) |
29 | | inidm 3140 |
. . 3
⊢ (𝐷 ∩ 𝐷) = 𝐷 |
30 | | ffn 4989 |
. . . . 5
⊢ (𝐻:𝐷⟶𝐶 → 𝐻 Fn 𝐷) |
31 | 1, 30 | syl 14 |
. . . 4
⊢ (φ → 𝐻 Fn 𝐷) |
32 | | fvco2 5185 |
. . . 4
⊢ ((𝐻 Fn 𝐷 ∧ x ∈ 𝐷) → ((𝐹 ∘ 𝐻)‘x) = (𝐹‘(𝐻‘x))) |
33 | 31, 32 | sylan 267 |
. . 3
⊢ ((φ ∧ x ∈ 𝐷) → ((𝐹 ∘ 𝐻)‘x) = (𝐹‘(𝐻‘x))) |
34 | | fvco2 5185 |
. . . 4
⊢ ((𝐻 Fn 𝐷 ∧ x ∈ 𝐷) → ((𝐺 ∘ 𝐻)‘x) = (𝐺‘(𝐻‘x))) |
35 | 31, 34 | sylan 267 |
. . 3
⊢ ((φ ∧ x ∈ 𝐷) → ((𝐺 ∘ 𝐻)‘x) = (𝐺‘(𝐻‘x))) |
36 | 21, 27, 28, 28, 29, 33, 35 | offval 5661 |
. 2
⊢ (φ → ((𝐹 ∘ 𝐻) ∘𝑓 𝑅(𝐺 ∘ 𝐻)) = (x
∈ 𝐷 ↦ ((𝐹‘(𝐻‘x))𝑅(𝐺‘(𝐻‘x))))) |
37 | 15, 36 | eqtr4d 2072 |
1
⊢ (φ → ((𝐹 ∘𝑓 𝑅𝐺) ∘ 𝐻) = ((𝐹 ∘ 𝐻) ∘𝑓 𝑅(𝐺 ∘ 𝐻))) |