Step | Hyp | Ref
| Expression |
1 | | eqid 2739 |
. . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) |
2 | | eqid 2739 |
. . . . 5
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
3 | | eqid 2739 |
. . . . 5
⊢
(comp‘𝐷) =
(comp‘𝐷) |
4 | | fucass.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) |
5 | | fucass.n |
. . . . . . . . . . 11
⊢ 𝑁 = (𝐶 Nat 𝐷) |
6 | 5 | natrcl 17338 |
. . . . . . . . . 10
⊢ (𝑅 ∈ (𝐹𝑁𝐺) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) |
7 | 4, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) |
8 | 7 | simpld 498 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
9 | | funcrcl 17251 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
11 | 10 | simprd 499 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ Cat) |
12 | 11 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat) |
13 | | eqid 2739 |
. . . . . . 7
⊢
(Base‘𝐶) =
(Base‘𝐶) |
14 | | relfunc 17250 |
. . . . . . . 8
⊢ Rel
(𝐶 Func 𝐷) |
15 | | 1st2ndbr 7779 |
. . . . . . . 8
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
16 | 14, 8, 15 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
17 | 13, 1, 16 | funcf1 17254 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) |
18 | 17 | ffvelrnda 6874 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) |
19 | 7 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) |
20 | | 1st2ndbr 7779 |
. . . . . . . 8
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
21 | 14, 19, 20 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
22 | 13, 1, 21 | funcf1 17254 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐺):(Base‘𝐶)⟶(Base‘𝐷)) |
23 | 22 | ffvelrnda 6874 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐷)) |
24 | | fucass.t |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ (𝐻𝑁𝐾)) |
25 | 5 | natrcl 17338 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (𝐻𝑁𝐾) → (𝐻 ∈ (𝐶 Func 𝐷) ∧ 𝐾 ∈ (𝐶 Func 𝐷))) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 ∈ (𝐶 Func 𝐷) ∧ 𝐾 ∈ (𝐶 Func 𝐷))) |
27 | 26 | simpld 498 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ (𝐶 Func 𝐷)) |
28 | | 1st2ndbr 7779 |
. . . . . . . 8
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐻 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐻)(𝐶 Func 𝐷)(2nd ‘𝐻)) |
29 | 14, 27, 28 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝐻)(𝐶 Func 𝐷)(2nd ‘𝐻)) |
30 | 13, 1, 29 | funcf1 17254 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐻):(Base‘𝐶)⟶(Base‘𝐷)) |
31 | 30 | ffvelrnda 6874 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐻)‘𝑥) ∈ (Base‘𝐷)) |
32 | 5, 4 | nat1st2nd 17339 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ (〈(1st ‘𝐹), (2nd ‘𝐹)〉𝑁〈(1st ‘𝐺), (2nd ‘𝐺)〉)) |
33 | 32 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑅 ∈ (〈(1st ‘𝐹), (2nd ‘𝐹)〉𝑁〈(1st ‘𝐺), (2nd ‘𝐺)〉)) |
34 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
35 | 5, 33, 13, 2, 34 | natcl 17341 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑅‘𝑥) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥))) |
36 | | fucass.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) |
37 | 5, 36 | nat1st2nd 17339 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ (〈(1st ‘𝐺), (2nd ‘𝐺)〉𝑁〈(1st ‘𝐻), (2nd ‘𝐻)〉)) |
38 | 37 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑆 ∈ (〈(1st ‘𝐺), (2nd ‘𝐺)〉𝑁〈(1st ‘𝐻), (2nd ‘𝐻)〉)) |
39 | 5, 38, 13, 2, 34 | natcl 17341 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑆‘𝑥) ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐻)‘𝑥))) |
40 | 26 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (𝐶 Func 𝐷)) |
41 | | 1st2ndbr 7779 |
. . . . . . . 8
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐾 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐾)(𝐶 Func 𝐷)(2nd ‘𝐾)) |
42 | 14, 40, 41 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝐾)(𝐶 Func 𝐷)(2nd ‘𝐾)) |
43 | 13, 1, 42 | funcf1 17254 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐾):(Base‘𝐶)⟶(Base‘𝐷)) |
44 | 43 | ffvelrnda 6874 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐾)‘𝑥) ∈ (Base‘𝐷)) |
45 | 5, 24 | nat1st2nd 17339 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (〈(1st ‘𝐻), (2nd ‘𝐻)〉𝑁〈(1st ‘𝐾), (2nd ‘𝐾)〉)) |
46 | 45 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑇 ∈ (〈(1st ‘𝐻), (2nd ‘𝐻)〉𝑁〈(1st ‘𝐾), (2nd ‘𝐾)〉)) |
47 | 5, 46, 13, 2, 34 | natcl 17341 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑇‘𝑥) ∈ (((1st ‘𝐻)‘𝑥)(Hom ‘𝐷)((1st ‘𝐾)‘𝑥))) |
48 | 1, 2, 3, 12, 18, 23, 31, 35, 39, 44, 47 | catass 17073 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (((𝑇‘𝑥)(〈((1st ‘𝐺)‘𝑥), ((1st ‘𝐻)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))(𝑆‘𝑥))(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))(𝑅‘𝑥)) = ((𝑇‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐻)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))((𝑆‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉(comp‘𝐷)((1st ‘𝐻)‘𝑥))(𝑅‘𝑥)))) |
49 | | fucass.q |
. . . . . 6
⊢ 𝑄 = (𝐶 FuncCat 𝐷) |
50 | | fucass.x |
. . . . . 6
⊢ ∙ =
(comp‘𝑄) |
51 | 36 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑆 ∈ (𝐺𝑁𝐻)) |
52 | 24 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑇 ∈ (𝐻𝑁𝐾)) |
53 | 49, 5, 13, 3, 50, 51, 52, 34 | fuccoval 17351 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑇(〈𝐺, 𝐻〉 ∙ 𝐾)𝑆)‘𝑥) = ((𝑇‘𝑥)(〈((1st ‘𝐺)‘𝑥), ((1st ‘𝐻)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))(𝑆‘𝑥))) |
54 | 53 | oveq1d 7198 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (((𝑇(〈𝐺, 𝐻〉 ∙ 𝐾)𝑆)‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))(𝑅‘𝑥)) = (((𝑇‘𝑥)(〈((1st ‘𝐺)‘𝑥), ((1st ‘𝐻)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))(𝑆‘𝑥))(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))(𝑅‘𝑥))) |
55 | 4 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑅 ∈ (𝐹𝑁𝐺)) |
56 | 49, 5, 13, 3, 50, 55, 51, 34 | fuccoval 17351 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅)‘𝑥) = ((𝑆‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉(comp‘𝐷)((1st ‘𝐻)‘𝑥))(𝑅‘𝑥))) |
57 | 56 | oveq2d 7199 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑇‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐻)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))((𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅)‘𝑥)) = ((𝑇‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐻)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))((𝑆‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉(comp‘𝐷)((1st ‘𝐻)‘𝑥))(𝑅‘𝑥)))) |
58 | 48, 54, 57 | 3eqtr4d 2784 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (((𝑇(〈𝐺, 𝐻〉 ∙ 𝐾)𝑆)‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))(𝑅‘𝑥)) = ((𝑇‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐻)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))((𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅)‘𝑥))) |
59 | 58 | mpteq2dva 5135 |
. 2
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ (((𝑇(〈𝐺, 𝐻〉 ∙ 𝐾)𝑆)‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))(𝑅‘𝑥))) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝑇‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐻)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))((𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅)‘𝑥)))) |
60 | 49, 5, 50, 36, 24 | fuccocl 17352 |
. . 3
⊢ (𝜑 → (𝑇(〈𝐺, 𝐻〉 ∙ 𝐾)𝑆) ∈ (𝐺𝑁𝐾)) |
61 | 49, 5, 13, 3, 50, 4, 60 | fucco 17350 |
. 2
⊢ (𝜑 → ((𝑇(〈𝐺, 𝐻〉 ∙ 𝐾)𝑆)(〈𝐹, 𝐺〉 ∙ 𝐾)𝑅) = (𝑥 ∈ (Base‘𝐶) ↦ (((𝑇(〈𝐺, 𝐻〉 ∙ 𝐾)𝑆)‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))(𝑅‘𝑥)))) |
62 | 49, 5, 50, 4, 36 | fuccocl 17352 |
. . 3
⊢ (𝜑 → (𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅) ∈ (𝐹𝑁𝐻)) |
63 | 49, 5, 13, 3, 50, 62, 24 | fucco 17350 |
. 2
⊢ (𝜑 → (𝑇(〈𝐹, 𝐻〉 ∙ 𝐾)(𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅)) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝑇‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐻)‘𝑥)〉(comp‘𝐷)((1st ‘𝐾)‘𝑥))((𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅)‘𝑥)))) |
64 | 59, 61, 63 | 3eqtr4d 2784 |
1
⊢ (𝜑 → ((𝑇(〈𝐺, 𝐻〉 ∙ 𝐾)𝑆)(〈𝐹, 𝐺〉 ∙ 𝐾)𝑅) = (𝑇(〈𝐹, 𝐻〉 ∙ 𝐾)(𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅))) |