Step | Hyp | Ref
| Expression |
1 | | evlfcl.e |
. . . 4
⊢ 𝐸 = (𝐶 evalF 𝐷) |
2 | | evlfcl.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
3 | | evlfcl.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) |
4 | | eqid 2733 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
5 | | eqid 2733 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
6 | | eqid 2733 |
. . . 4
⊢
(comp‘𝐷) =
(comp‘𝐷) |
7 | | evlfcl.n |
. . . 4
⊢ 𝑁 = (𝐶 Nat 𝐷) |
8 | | evlfcl.f |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (Base‘𝐶))) |
9 | 8 | simpld 496 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
10 | | evlfcl.h |
. . . . 5
⊢ (𝜑 → (𝐻 ∈ (𝐶 Func 𝐷) ∧ 𝑍 ∈ (Base‘𝐶))) |
11 | 10 | simpld 496 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ (𝐶 Func 𝐷)) |
12 | 8 | simprd 497 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) |
13 | 10 | simprd 497 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶)) |
14 | | eqid 2733 |
. . . 4
⊢
(⟨𝐹, 𝑋⟩(2nd
‘𝐸)⟨𝐻, 𝑍⟩) = (⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩) |
15 | | evlfcl.q |
. . . . 5
⊢ 𝑄 = (𝐶 FuncCat 𝐷) |
16 | | eqid 2733 |
. . . . 5
⊢
(comp‘𝑄) =
(comp‘𝑄) |
17 | | evlfcl.a |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ (𝐹𝑁𝐺) ∧ 𝐾 ∈ (𝑋(Hom ‘𝐶)𝑌))) |
18 | 17 | simpld 496 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) |
19 | | evlfcl.b |
. . . . . 6
⊢ (𝜑 → (𝐵 ∈ (𝐺𝑁𝐻) ∧ 𝐿 ∈ (𝑌(Hom ‘𝐶)𝑍))) |
20 | 19 | simpld 496 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (𝐺𝑁𝐻)) |
21 | 15, 7, 16, 18, 20 | fuccocl 17858 |
. . . 4
⊢ (𝜑 → (𝐵(⟨𝐹, 𝐺⟩(comp‘𝑄)𝐻)𝐴) ∈ (𝐹𝑁𝐻)) |
22 | | eqid 2733 |
. . . . 5
⊢
(comp‘𝐶) =
(comp‘𝐶) |
23 | | evlfcl.g |
. . . . . 6
⊢ (𝜑 → (𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ (Base‘𝐶))) |
24 | 23 | simprd 497 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) |
25 | 17 | simprd 497 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
26 | 19 | simprd 497 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ (𝑌(Hom ‘𝐶)𝑍)) |
27 | 4, 5, 22, 2, 12, 24, 13, 25, 26 | catcocl 17570 |
. . . 4
⊢ (𝜑 → (𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾) ∈ (𝑋(Hom ‘𝐶)𝑍)) |
28 | 1, 2, 3, 4, 5, 6, 7, 9, 11, 12, 13, 14, 21, 27 | evlf2val 18113 |
. . 3
⊢ (𝜑 → ((𝐵(⟨𝐹, 𝐺⟩(comp‘𝑄)𝐻)𝐴)(⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)(𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾)) = (((𝐵(⟨𝐹, 𝐺⟩(comp‘𝑄)𝐻)𝐴)‘𝑍)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑋(2nd ‘𝐹)𝑍)‘(𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾)))) |
29 | 15, 7, 4, 6, 16, 18, 20, 13 | fuccoval 17857 |
. . . 4
⊢ (𝜑 → ((𝐵(⟨𝐹, 𝐺⟩(comp‘𝑄)𝐻)𝐴)‘𝑍) = ((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑍), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑍))) |
30 | 29 | oveq1d 7373 |
. . 3
⊢ (𝜑 → (((𝐵(⟨𝐹, 𝐺⟩(comp‘𝑄)𝐻)𝐴)‘𝑍)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑋(2nd ‘𝐹)𝑍)‘(𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾))) = (((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑍), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑍))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑋(2nd ‘𝐹)𝑍)‘(𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾)))) |
31 | | relfunc 17753 |
. . . . . . 7
⊢ Rel
(𝐶 Func 𝐷) |
32 | | 1st2ndbr 7975 |
. . . . . . 7
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
33 | 31, 9, 32 | sylancr 588 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
34 | 4, 5, 22, 6, 33, 12, 24, 13, 25, 26 | funcco 17762 |
. . . . 5
⊢ (𝜑 → ((𝑋(2nd ‘𝐹)𝑍)‘(𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾)) = (((𝑌(2nd ‘𝐹)𝑍)‘𝐿)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑍))((𝑋(2nd ‘𝐹)𝑌)‘𝐾))) |
35 | 34 | oveq2d 7374 |
. . . 4
⊢ (𝜑 → (((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑍), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑍))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑋(2nd ‘𝐹)𝑍)‘(𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾))) = (((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑍), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑍))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(((𝑌(2nd ‘𝐹)𝑍)‘𝐿)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑍))((𝑋(2nd ‘𝐹)𝑌)‘𝐾)))) |
36 | 7, 18 | nat1st2nd 17843 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (⟨(1st ‘𝐹), (2nd ‘𝐹)⟩𝑁⟨(1st ‘𝐺), (2nd ‘𝐺)⟩)) |
37 | 7, 36, 4, 5, 6, 24,
13, 26 | nati 17847 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝑍)(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑍))((𝑌(2nd ‘𝐹)𝑍)‘𝐿)) = (((𝑌(2nd ‘𝐺)𝑍)‘𝐿)(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑍))(𝐴‘𝑌))) |
38 | 37 | oveq2d 7374 |
. . . . . . 7
⊢ (𝜑 → ((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝐴‘𝑍)(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑍))((𝑌(2nd ‘𝐹)𝑍)‘𝐿))) = ((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(((𝑌(2nd ‘𝐺)𝑍)‘𝐿)(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑍))(𝐴‘𝑌)))) |
39 | | eqid 2733 |
. . . . . . . 8
⊢
(Base‘𝐷) =
(Base‘𝐷) |
40 | | eqid 2733 |
. . . . . . . 8
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
41 | 4, 39, 33 | funcf1 17757 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) |
42 | 41, 24 | ffvelcdmd 7037 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝐹)‘𝑌) ∈ (Base‘𝐷)) |
43 | 41, 13 | ffvelcdmd 7037 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝐹)‘𝑍) ∈ (Base‘𝐷)) |
44 | 23 | simpld 496 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) |
45 | | 1st2ndbr 7975 |
. . . . . . . . . . 11
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
46 | 31, 44, 45 | sylancr 588 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
47 | 4, 39, 46 | funcf1 17757 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝐺):(Base‘𝐶)⟶(Base‘𝐷)) |
48 | 47, 13 | ffvelcdmd 7037 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝐺)‘𝑍) ∈ (Base‘𝐷)) |
49 | 4, 5, 40, 33, 24, 13 | funcf2 17759 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌(2nd ‘𝐹)𝑍):(𝑌(Hom ‘𝐶)𝑍)⟶(((1st ‘𝐹)‘𝑌)(Hom ‘𝐷)((1st ‘𝐹)‘𝑍))) |
50 | 49, 26 | ffvelcdmd 7037 |
. . . . . . . 8
⊢ (𝜑 → ((𝑌(2nd ‘𝐹)𝑍)‘𝐿) ∈ (((1st ‘𝐹)‘𝑌)(Hom ‘𝐷)((1st ‘𝐹)‘𝑍))) |
51 | 7, 36, 4, 40, 13 | natcl 17845 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘𝑍) ∈ (((1st ‘𝐹)‘𝑍)(Hom ‘𝐷)((1st ‘𝐺)‘𝑍))) |
52 | | 1st2ndbr 7975 |
. . . . . . . . . . 11
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐻 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐻)(𝐶 Func 𝐷)(2nd ‘𝐻)) |
53 | 31, 11, 52 | sylancr 588 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝐻)(𝐶 Func 𝐷)(2nd ‘𝐻)) |
54 | 4, 39, 53 | funcf1 17757 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝐻):(Base‘𝐶)⟶(Base‘𝐷)) |
55 | 54, 13 | ffvelcdmd 7037 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝐻)‘𝑍) ∈ (Base‘𝐷)) |
56 | 7, 20 | nat1st2nd 17843 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ (⟨(1st ‘𝐺), (2nd ‘𝐺)⟩𝑁⟨(1st ‘𝐻), (2nd ‘𝐻)⟩)) |
57 | 7, 56, 4, 40, 13 | natcl 17845 |
. . . . . . . 8
⊢ (𝜑 → (𝐵‘𝑍) ∈ (((1st ‘𝐺)‘𝑍)(Hom ‘𝐷)((1st ‘𝐻)‘𝑍))) |
58 | 39, 40, 6, 3, 42, 43, 48, 50, 51, 55, 57 | catass 17571 |
. . . . . . 7
⊢ (𝜑 → (((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑍), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑍))(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐹)𝑍)‘𝐿)) = ((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝐴‘𝑍)(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑍))((𝑌(2nd ‘𝐹)𝑍)‘𝐿)))) |
59 | 47, 24 | ffvelcdmd 7037 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝐺)‘𝑌) ∈ (Base‘𝐷)) |
60 | 7, 36, 4, 40, 24 | natcl 17845 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘𝑌) ∈ (((1st ‘𝐹)‘𝑌)(Hom ‘𝐷)((1st ‘𝐺)‘𝑌))) |
61 | 4, 5, 40, 46, 24, 13 | funcf2 17759 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌(2nd ‘𝐺)𝑍):(𝑌(Hom ‘𝐶)𝑍)⟶(((1st ‘𝐺)‘𝑌)(Hom ‘𝐷)((1st ‘𝐺)‘𝑍))) |
62 | 61, 26 | ffvelcdmd 7037 |
. . . . . . . 8
⊢ (𝜑 → ((𝑌(2nd ‘𝐺)𝑍)‘𝐿) ∈ (((1st ‘𝐺)‘𝑌)(Hom ‘𝐷)((1st ‘𝐺)‘𝑍))) |
63 | 39, 40, 6, 3, 42, 59, 48, 60, 62, 55, 57 | catass 17571 |
. . . . . . 7
⊢ (𝜑 → (((𝐵‘𝑍)(⟨((1st ‘𝐺)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐺)𝑍)‘𝐿))(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑌)) = ((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(((𝑌(2nd ‘𝐺)𝑍)‘𝐿)(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑍))(𝐴‘𝑌)))) |
64 | 38, 58, 63 | 3eqtr4d 2783 |
. . . . . 6
⊢ (𝜑 → (((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑍), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑍))(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐹)𝑍)‘𝐿)) = (((𝐵‘𝑍)(⟨((1st ‘𝐺)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐺)𝑍)‘𝐿))(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑌))) |
65 | 64 | oveq1d 7373 |
. . . . 5
⊢ (𝜑 → ((((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑍), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑍))(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐹)𝑍)‘𝐿))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑋(2nd ‘𝐹)𝑌)‘𝐾)) = ((((𝐵‘𝑍)(⟨((1st ‘𝐺)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐺)𝑍)‘𝐿))(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑌))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑋(2nd ‘𝐹)𝑌)‘𝐾))) |
66 | 41, 12 | ffvelcdmd 7037 |
. . . . . 6
⊢ (𝜑 → ((1st
‘𝐹)‘𝑋) ∈ (Base‘𝐷)) |
67 | 4, 5, 40, 33, 12, 24 | funcf2 17759 |
. . . . . . 7
⊢ (𝜑 → (𝑋(2nd ‘𝐹)𝑌):(𝑋(Hom ‘𝐶)𝑌)⟶(((1st ‘𝐹)‘𝑋)(Hom ‘𝐷)((1st ‘𝐹)‘𝑌))) |
68 | 67, 25 | ffvelcdmd 7037 |
. . . . . 6
⊢ (𝜑 → ((𝑋(2nd ‘𝐹)𝑌)‘𝐾) ∈ (((1st ‘𝐹)‘𝑋)(Hom ‘𝐷)((1st ‘𝐹)‘𝑌))) |
69 | 39, 40, 6, 3, 43, 48, 55, 51, 57 | catcocl 17570 |
. . . . . 6
⊢ (𝜑 → ((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑍), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑍)) ∈ (((1st ‘𝐹)‘𝑍)(Hom ‘𝐷)((1st ‘𝐻)‘𝑍))) |
70 | 39, 40, 6, 3, 66, 42, 43, 68, 50, 55, 69 | catass 17571 |
. . . . 5
⊢ (𝜑 → ((((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑍), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑍))(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐹)𝑍)‘𝐿))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑋(2nd ‘𝐹)𝑌)‘𝐾)) = (((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑍), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑍))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(((𝑌(2nd ‘𝐹)𝑍)‘𝐿)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑍))((𝑋(2nd ‘𝐹)𝑌)‘𝐾)))) |
71 | 39, 40, 6, 3, 59, 48, 55, 62, 57 | catcocl 17570 |
. . . . . 6
⊢ (𝜑 → ((𝐵‘𝑍)(⟨((1st ‘𝐺)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐺)𝑍)‘𝐿)) ∈ (((1st ‘𝐺)‘𝑌)(Hom ‘𝐷)((1st ‘𝐻)‘𝑍))) |
72 | 39, 40, 6, 3, 66, 42, 59, 68, 60, 55, 71 | catass 17571 |
. . . . 5
⊢ (𝜑 → ((((𝐵‘𝑍)(⟨((1st ‘𝐺)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐺)𝑍)‘𝐿))(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑌))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑋(2nd ‘𝐹)𝑌)‘𝐾)) = (((𝐵‘𝑍)(⟨((1st ‘𝐺)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐺)𝑍)‘𝐿))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝐴‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝐾)))) |
73 | 65, 70, 72 | 3eqtr3d 2781 |
. . . 4
⊢ (𝜑 → (((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑍), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑍))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(((𝑌(2nd ‘𝐹)𝑍)‘𝐿)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑍))((𝑋(2nd ‘𝐹)𝑌)‘𝐾))) = (((𝐵‘𝑍)(⟨((1st ‘𝐺)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐺)𝑍)‘𝐿))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝐴‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝐾)))) |
74 | 35, 73 | eqtrd 2773 |
. . 3
⊢ (𝜑 → (((𝐵‘𝑍)(⟨((1st ‘𝐹)‘𝑍), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))(𝐴‘𝑍))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑋(2nd ‘𝐹)𝑍)‘(𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾))) = (((𝐵‘𝑍)(⟨((1st ‘𝐺)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐺)𝑍)‘𝐿))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝐴‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝐾)))) |
75 | 28, 30, 74 | 3eqtrd 2777 |
. 2
⊢ (𝜑 → ((𝐵(⟨𝐹, 𝐺⟩(comp‘𝑄)𝐻)𝐴)(⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)(𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾)) = (((𝐵‘𝑍)(⟨((1st ‘𝐺)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐺)𝑍)‘𝐿))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝐴‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝐾)))) |
76 | | eqid 2733 |
. . . . 5
⊢ (𝑄 ×c
𝐶) = (𝑄 ×c 𝐶) |
77 | 15 | fucbas 17853 |
. . . . 5
⊢ (𝐶 Func 𝐷) = (Base‘𝑄) |
78 | 15, 7 | fuchom 17854 |
. . . . 5
⊢ 𝑁 = (Hom ‘𝑄) |
79 | | eqid 2733 |
. . . . 5
⊢
(comp‘(𝑄
×c 𝐶)) = (comp‘(𝑄 ×c 𝐶)) |
80 | 76, 77, 4, 78, 5, 9,
12, 44, 24, 16, 22, 79, 11, 13, 18, 25, 20, 26 | xpcco2 18080 |
. . . 4
⊢ (𝜑 → (⟨𝐵, 𝐿⟩(⟨⟨𝐹, 𝑋⟩, ⟨𝐺, 𝑌⟩⟩(comp‘(𝑄 ×c 𝐶))⟨𝐻, 𝑍⟩)⟨𝐴, 𝐾⟩) = ⟨(𝐵(⟨𝐹, 𝐺⟩(comp‘𝑄)𝐻)𝐴), (𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾)⟩) |
81 | 80 | fveq2d 6847 |
. . 3
⊢ (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)‘(⟨𝐵, 𝐿⟩(⟨⟨𝐹, 𝑋⟩, ⟨𝐺, 𝑌⟩⟩(comp‘(𝑄 ×c 𝐶))⟨𝐻, 𝑍⟩)⟨𝐴, 𝐾⟩)) = ((⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)‘⟨(𝐵(⟨𝐹, 𝐺⟩(comp‘𝑄)𝐻)𝐴), (𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾)⟩)) |
82 | | df-ov 7361 |
. . 3
⊢ ((𝐵(⟨𝐹, 𝐺⟩(comp‘𝑄)𝐻)𝐴)(⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)(𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾)) = ((⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)‘⟨(𝐵(⟨𝐹, 𝐺⟩(comp‘𝑄)𝐻)𝐴), (𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾)⟩) |
83 | 81, 82 | eqtr4di 2791 |
. 2
⊢ (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)‘(⟨𝐵, 𝐿⟩(⟨⟨𝐹, 𝑋⟩, ⟨𝐺, 𝑌⟩⟩(comp‘(𝑄 ×c 𝐶))⟨𝐻, 𝑍⟩)⟨𝐴, 𝐾⟩)) = ((𝐵(⟨𝐹, 𝐺⟩(comp‘𝑄)𝐻)𝐴)(⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)(𝐿(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)𝐾))) |
84 | | df-ov 7361 |
. . . . . 6
⊢ (𝐹(1st ‘𝐸)𝑋) = ((1st ‘𝐸)‘⟨𝐹, 𝑋⟩) |
85 | 1, 2, 3, 4, 9, 12 | evlf1 18114 |
. . . . . 6
⊢ (𝜑 → (𝐹(1st ‘𝐸)𝑋) = ((1st ‘𝐹)‘𝑋)) |
86 | 84, 85 | eqtr3id 2787 |
. . . . 5
⊢ (𝜑 → ((1st
‘𝐸)‘⟨𝐹, 𝑋⟩) = ((1st ‘𝐹)‘𝑋)) |
87 | | df-ov 7361 |
. . . . . 6
⊢ (𝐺(1st ‘𝐸)𝑌) = ((1st ‘𝐸)‘⟨𝐺, 𝑌⟩) |
88 | 1, 2, 3, 4, 44, 24 | evlf1 18114 |
. . . . . 6
⊢ (𝜑 → (𝐺(1st ‘𝐸)𝑌) = ((1st ‘𝐺)‘𝑌)) |
89 | 87, 88 | eqtr3id 2787 |
. . . . 5
⊢ (𝜑 → ((1st
‘𝐸)‘⟨𝐺, 𝑌⟩) = ((1st ‘𝐺)‘𝑌)) |
90 | 86, 89 | opeq12d 4839 |
. . . 4
⊢ (𝜑 → ⟨((1st
‘𝐸)‘⟨𝐹, 𝑋⟩), ((1st ‘𝐸)‘⟨𝐺, 𝑌⟩)⟩ = ⟨((1st
‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑌)⟩) |
91 | | df-ov 7361 |
. . . . 5
⊢ (𝐻(1st ‘𝐸)𝑍) = ((1st ‘𝐸)‘⟨𝐻, 𝑍⟩) |
92 | 1, 2, 3, 4, 11, 13 | evlf1 18114 |
. . . . 5
⊢ (𝜑 → (𝐻(1st ‘𝐸)𝑍) = ((1st ‘𝐻)‘𝑍)) |
93 | 91, 92 | eqtr3id 2787 |
. . . 4
⊢ (𝜑 → ((1st
‘𝐸)‘⟨𝐻, 𝑍⟩) = ((1st ‘𝐻)‘𝑍)) |
94 | 90, 93 | oveq12d 7376 |
. . 3
⊢ (𝜑 → (⟨((1st
‘𝐸)‘⟨𝐹, 𝑋⟩), ((1st ‘𝐸)‘⟨𝐺, 𝑌⟩)⟩(comp‘𝐷)((1st ‘𝐸)‘⟨𝐻, 𝑍⟩)) = (⟨((1st
‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))) |
95 | | df-ov 7361 |
. . . 4
⊢ (𝐵(⟨𝐺, 𝑌⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)𝐿) = ((⟨𝐺, 𝑌⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)‘⟨𝐵, 𝐿⟩) |
96 | | eqid 2733 |
. . . . 5
⊢
(⟨𝐺, 𝑌⟩(2nd
‘𝐸)⟨𝐻, 𝑍⟩) = (⟨𝐺, 𝑌⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩) |
97 | 1, 2, 3, 4, 5, 6, 7, 44, 11, 24, 13, 96, 20, 26 | evlf2val 18113 |
. . . 4
⊢ (𝜑 → (𝐵(⟨𝐺, 𝑌⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)𝐿) = ((𝐵‘𝑍)(⟨((1st ‘𝐺)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐺)𝑍)‘𝐿))) |
98 | 95, 97 | eqtr3id 2787 |
. . 3
⊢ (𝜑 → ((⟨𝐺, 𝑌⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)‘⟨𝐵, 𝐿⟩) = ((𝐵‘𝑍)(⟨((1st ‘𝐺)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐺)𝑍)‘𝐿))) |
99 | | df-ov 7361 |
. . . 4
⊢ (𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩)𝐾) = ((⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩)‘⟨𝐴, 𝐾⟩) |
100 | | eqid 2733 |
. . . . 5
⊢
(⟨𝐹, 𝑋⟩(2nd
‘𝐸)⟨𝐺, 𝑌⟩) = (⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩) |
101 | 1, 2, 3, 4, 5, 6, 7, 9, 44, 12, 24, 100, 18, 25 | evlf2val 18113 |
. . . 4
⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩)𝐾) = ((𝐴‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝐾))) |
102 | 99, 101 | eqtr3id 2787 |
. . 3
⊢ (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩)‘⟨𝐴, 𝐾⟩) = ((𝐴‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝐾))) |
103 | 94, 98, 102 | oveq123d 7379 |
. 2
⊢ (𝜑 → (((⟨𝐺, 𝑌⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)‘⟨𝐵, 𝐿⟩)(⟨((1st ‘𝐸)‘⟨𝐹, 𝑋⟩), ((1st ‘𝐸)‘⟨𝐺, 𝑌⟩)⟩(comp‘𝐷)((1st ‘𝐸)‘⟨𝐻, 𝑍⟩))((⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩)‘⟨𝐴, 𝐾⟩)) = (((𝐵‘𝑍)(⟨((1st ‘𝐺)‘𝑌), ((1st ‘𝐺)‘𝑍)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝑌(2nd ‘𝐺)𝑍)‘𝐿))(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐻)‘𝑍))((𝐴‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝐾)))) |
104 | 75, 83, 103 | 3eqtr4d 2783 |
1
⊢ (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)‘(⟨𝐵, 𝐿⟩(⟨⟨𝐹, 𝑋⟩, ⟨𝐺, 𝑌⟩⟩(comp‘(𝑄 ×c 𝐶))⟨𝐻, 𝑍⟩)⟨𝐴, 𝐾⟩)) = (((⟨𝐺, 𝑌⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)‘⟨𝐵, 𝐿⟩)(⟨((1st ‘𝐸)‘⟨𝐹, 𝑋⟩), ((1st ‘𝐸)‘⟨𝐺, 𝑌⟩)⟩(comp‘𝐷)((1st ‘𝐸)‘⟨𝐻, 𝑍⟩))((⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩)‘⟨𝐴, 𝐾⟩))) |