| Step | Hyp | Ref
| Expression |
| 1 | | coass 6285 |
. . . 4
⊢
(((1st ‘𝐾) ∘ (1st ‘𝐻)) ∘ (1st
‘𝐺)) =
((1st ‘𝐾)
∘ ((1st ‘𝐻) ∘ (1st ‘𝐺))) |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 3 | | cofuass.h |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ (𝐷 Func 𝐸)) |
| 4 | | cofuass.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝐸 Func 𝐹)) |
| 5 | 2, 3, 4 | cofu1st 17928 |
. . . . 5
⊢ (𝜑 → (1st
‘(𝐾
∘func 𝐻)) = ((1st ‘𝐾) ∘ (1st
‘𝐻))) |
| 6 | 5 | coeq1d 5872 |
. . . 4
⊢ (𝜑 → ((1st
‘(𝐾
∘func 𝐻)) ∘ (1st ‘𝐺)) = (((1st
‘𝐾) ∘
(1st ‘𝐻))
∘ (1st ‘𝐺))) |
| 7 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 8 | | cofuass.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) |
| 9 | 7, 8, 3 | cofu1st 17928 |
. . . . 5
⊢ (𝜑 → (1st
‘(𝐻
∘func 𝐺)) = ((1st ‘𝐻) ∘ (1st
‘𝐺))) |
| 10 | 9 | coeq2d 5873 |
. . . 4
⊢ (𝜑 → ((1st
‘𝐾) ∘
(1st ‘(𝐻
∘func 𝐺))) = ((1st ‘𝐾) ∘ ((1st
‘𝐻) ∘
(1st ‘𝐺)))) |
| 11 | 1, 6, 10 | 3eqtr4a 2803 |
. . 3
⊢ (𝜑 → ((1st
‘(𝐾
∘func 𝐻)) ∘ (1st ‘𝐺)) = ((1st
‘𝐾) ∘
(1st ‘(𝐻
∘func 𝐺)))) |
| 12 | | coass 6285 |
. . . . 5
⊢
(((((1st ‘𝐻)‘((1st ‘𝐺)‘𝑥))(2nd ‘𝐾)((1st ‘𝐻)‘((1st ‘𝐺)‘𝑦))) ∘ (((1st ‘𝐺)‘𝑥)(2nd ‘𝐻)((1st ‘𝐺)‘𝑦))) ∘ (𝑥(2nd ‘𝐺)𝑦)) = ((((1st ‘𝐻)‘((1st
‘𝐺)‘𝑥))(2nd ‘𝐾)((1st ‘𝐻)‘((1st
‘𝐺)‘𝑦))) ∘ ((((1st
‘𝐺)‘𝑥)(2nd ‘𝐻)((1st ‘𝐺)‘𝑦)) ∘ (𝑥(2nd ‘𝐺)𝑦))) |
| 13 | 3 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝐻 ∈ (𝐷 Func 𝐸)) |
| 14 | 4 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝐾 ∈ (𝐸 Func 𝐹)) |
| 15 | | relfunc 17907 |
. . . . . . . . . . 11
⊢ Rel
(𝐶 Func 𝐷) |
| 16 | | 1st2ndbr 8067 |
. . . . . . . . . . 11
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
| 17 | 15, 8, 16 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
| 18 | 17 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (1st ‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
| 19 | 7, 2, 18 | funcf1 17911 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (1st ‘𝐺):(Base‘𝐶)⟶(Base‘𝐷)) |
| 20 | | simp2 1138 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
| 21 | 19, 20 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐷)) |
| 22 | | simp3 1139 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶)) |
| 23 | 19, 22 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑦) ∈ (Base‘𝐷)) |
| 24 | 2, 13, 14, 21, 23 | cofu2nd 17930 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (((1st ‘𝐺)‘𝑥)(2nd ‘(𝐾 ∘func 𝐻))((1st ‘𝐺)‘𝑦)) = ((((1st ‘𝐻)‘((1st
‘𝐺)‘𝑥))(2nd ‘𝐾)((1st ‘𝐻)‘((1st
‘𝐺)‘𝑦))) ∘ (((1st
‘𝐺)‘𝑥)(2nd ‘𝐻)((1st ‘𝐺)‘𝑦)))) |
| 25 | 24 | coeq1d 5872 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → ((((1st ‘𝐺)‘𝑥)(2nd ‘(𝐾 ∘func 𝐻))((1st ‘𝐺)‘𝑦)) ∘ (𝑥(2nd ‘𝐺)𝑦)) = (((((1st ‘𝐻)‘((1st
‘𝐺)‘𝑥))(2nd ‘𝐾)((1st ‘𝐻)‘((1st
‘𝐺)‘𝑦))) ∘ (((1st
‘𝐺)‘𝑥)(2nd ‘𝐻)((1st ‘𝐺)‘𝑦))) ∘ (𝑥(2nd ‘𝐺)𝑦))) |
| 26 | 8 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐶 Func 𝐷)) |
| 27 | 7, 26, 13, 20 | cofu1 17929 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → ((1st ‘(𝐻 ∘func
𝐺))‘𝑥) = ((1st
‘𝐻)‘((1st ‘𝐺)‘𝑥))) |
| 28 | 7, 26, 13, 22 | cofu1 17929 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → ((1st ‘(𝐻 ∘func
𝐺))‘𝑦) = ((1st
‘𝐻)‘((1st ‘𝐺)‘𝑦))) |
| 29 | 27, 28 | oveq12d 7449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (((1st ‘(𝐻 ∘func
𝐺))‘𝑥)(2nd ‘𝐾)((1st ‘(𝐻 ∘func
𝐺))‘𝑦)) = (((1st
‘𝐻)‘((1st ‘𝐺)‘𝑥))(2nd ‘𝐾)((1st ‘𝐻)‘((1st ‘𝐺)‘𝑦)))) |
| 30 | 7, 26, 13, 20, 22 | cofu2nd 17930 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(2nd ‘(𝐻 ∘func 𝐺))𝑦) = ((((1st ‘𝐺)‘𝑥)(2nd ‘𝐻)((1st ‘𝐺)‘𝑦)) ∘ (𝑥(2nd ‘𝐺)𝑦))) |
| 31 | 29, 30 | coeq12d 5875 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → ((((1st ‘(𝐻 ∘func
𝐺))‘𝑥)(2nd ‘𝐾)((1st ‘(𝐻 ∘func
𝐺))‘𝑦)) ∘ (𝑥(2nd ‘(𝐻 ∘func 𝐺))𝑦)) = ((((1st ‘𝐻)‘((1st
‘𝐺)‘𝑥))(2nd ‘𝐾)((1st ‘𝐻)‘((1st
‘𝐺)‘𝑦))) ∘ ((((1st
‘𝐺)‘𝑥)(2nd ‘𝐻)((1st ‘𝐺)‘𝑦)) ∘ (𝑥(2nd ‘𝐺)𝑦)))) |
| 32 | 12, 25, 31 | 3eqtr4a 2803 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → ((((1st ‘𝐺)‘𝑥)(2nd ‘(𝐾 ∘func 𝐻))((1st ‘𝐺)‘𝑦)) ∘ (𝑥(2nd ‘𝐺)𝑦)) = ((((1st ‘(𝐻 ∘func
𝐺))‘𝑥)(2nd ‘𝐾)((1st ‘(𝐻 ∘func
𝐺))‘𝑦)) ∘ (𝑥(2nd ‘(𝐻 ∘func 𝐺))𝑦))) |
| 33 | 32 | mpoeq3dva 7510 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐺)‘𝑥)(2nd ‘(𝐾 ∘func 𝐻))((1st ‘𝐺)‘𝑦)) ∘ (𝑥(2nd ‘𝐺)𝑦))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘(𝐻 ∘func
𝐺))‘𝑥)(2nd ‘𝐾)((1st ‘(𝐻 ∘func
𝐺))‘𝑦)) ∘ (𝑥(2nd ‘(𝐻 ∘func 𝐺))𝑦)))) |
| 34 | 11, 33 | opeq12d 4881 |
. 2
⊢ (𝜑 → 〈((1st
‘(𝐾
∘func 𝐻)) ∘ (1st ‘𝐺)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐺)‘𝑥)(2nd ‘(𝐾 ∘func 𝐻))((1st ‘𝐺)‘𝑦)) ∘ (𝑥(2nd ‘𝐺)𝑦)))〉 = 〈((1st
‘𝐾) ∘
(1st ‘(𝐻
∘func 𝐺))), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘(𝐻 ∘func
𝐺))‘𝑥)(2nd ‘𝐾)((1st ‘(𝐻 ∘func
𝐺))‘𝑦)) ∘ (𝑥(2nd ‘(𝐻 ∘func 𝐺))𝑦)))〉) |
| 35 | 3, 4 | cofucl 17933 |
. . 3
⊢ (𝜑 → (𝐾 ∘func 𝐻) ∈ (𝐷 Func 𝐹)) |
| 36 | 7, 8, 35 | cofuval 17927 |
. 2
⊢ (𝜑 → ((𝐾 ∘func 𝐻) ∘func
𝐺) = 〈((1st
‘(𝐾
∘func 𝐻)) ∘ (1st ‘𝐺)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐺)‘𝑥)(2nd ‘(𝐾 ∘func 𝐻))((1st ‘𝐺)‘𝑦)) ∘ (𝑥(2nd ‘𝐺)𝑦)))〉) |
| 37 | 8, 3 | cofucl 17933 |
. . 3
⊢ (𝜑 → (𝐻 ∘func 𝐺) ∈ (𝐶 Func 𝐸)) |
| 38 | 7, 37, 4 | cofuval 17927 |
. 2
⊢ (𝜑 → (𝐾 ∘func (𝐻 ∘func
𝐺)) =
〈((1st ‘𝐾) ∘ (1st ‘(𝐻 ∘func
𝐺))), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘(𝐻 ∘func
𝐺))‘𝑥)(2nd ‘𝐾)((1st ‘(𝐻 ∘func
𝐺))‘𝑦)) ∘ (𝑥(2nd ‘(𝐻 ∘func 𝐺))𝑦)))〉) |
| 39 | 34, 36, 38 | 3eqtr4d 2787 |
1
⊢ (𝜑 → ((𝐾 ∘func 𝐻) ∘func
𝐺) = (𝐾 ∘func (𝐻 ∘func
𝐺))) |