Step | Hyp | Ref
| Expression |
1 | | uncfval.g |
. . . . . . 7
⊢ 𝐹 = (⟨“𝐶𝐷𝐸”⟩ uncurryF
𝐺) |
2 | | uncfval.c |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ Cat) |
3 | | uncfval.d |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ Cat) |
4 | | uncfval.f |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) |
5 | 1, 2, 3, 4 | uncfval 18128 |
. . . . . 6
⊢ (𝜑 → 𝐹 = ((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))) |
6 | 5 | fveq2d 6847 |
. . . . 5
⊢ (𝜑 → (2nd
‘𝐹) = (2nd
‘((𝐷
evalF 𝐸)
∘func ((𝐺 ∘func (𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷))))) |
7 | 6 | oveqd 7375 |
. . . 4
⊢ (𝜑 → (⟨𝑋, 𝑌⟩(2nd ‘𝐹)⟨𝑍, 𝑊⟩) = (⟨𝑋, 𝑌⟩(2nd ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷))))⟨𝑍, 𝑊⟩)) |
8 | 7 | oveqd 7375 |
. . 3
⊢ (𝜑 → (𝑅(⟨𝑋, 𝑌⟩(2nd ‘𝐹)⟨𝑍, 𝑊⟩)𝑆) = (𝑅(⟨𝑋, 𝑌⟩(2nd ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷))))⟨𝑍, 𝑊⟩)𝑆)) |
9 | | df-ov 7361 |
. . . 4
⊢ (𝑅(⟨𝑋, 𝑌⟩(2nd ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷))))⟨𝑍, 𝑊⟩)𝑆) = ((⟨𝑋, 𝑌⟩(2nd ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷))))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩) |
10 | | eqid 2733 |
. . . . . 6
⊢ (𝐶 ×c
𝐷) = (𝐶 ×c 𝐷) |
11 | | uncf1.a |
. . . . . 6
⊢ 𝐴 = (Base‘𝐶) |
12 | | uncf1.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐷) |
13 | 10, 11, 12 | xpcbas 18071 |
. . . . 5
⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷)) |
14 | | eqid 2733 |
. . . . . 6
⊢ ((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)) = ((𝐺 ∘func (𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)) |
15 | | eqid 2733 |
. . . . . 6
⊢ ((𝐷 FuncCat 𝐸) ×c 𝐷) = ((𝐷 FuncCat 𝐸) ×c 𝐷) |
16 | | funcrcl 17754 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)) → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
17 | 4, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
18 | 17 | simpld 496 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ Cat) |
19 | | eqid 2733 |
. . . . . . . 8
⊢ (𝐶
1stF 𝐷) = (𝐶 1stF 𝐷) |
20 | 10, 18, 2, 19 | 1stfcl 18090 |
. . . . . . 7
⊢ (𝜑 → (𝐶 1stF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐶)) |
21 | 20, 4 | cofucl 17779 |
. . . . . 6
⊢ (𝜑 → (𝐺 ∘func (𝐶
1stF 𝐷)) ∈ ((𝐶 ×c 𝐷) Func (𝐷 FuncCat 𝐸))) |
22 | | eqid 2733 |
. . . . . . 7
⊢ (𝐶
2ndF 𝐷) = (𝐶 2ndF 𝐷) |
23 | 10, 18, 2, 22 | 2ndfcl 18091 |
. . . . . 6
⊢ (𝜑 → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷)) |
24 | 14, 15, 21, 23 | prfcl 18096 |
. . . . 5
⊢ (𝜑 → ((𝐺 ∘func (𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)) ∈ ((𝐶 ×c 𝐷) Func ((𝐷 FuncCat 𝐸) ×c 𝐷))) |
25 | | eqid 2733 |
. . . . . 6
⊢ (𝐷 evalF 𝐸) = (𝐷 evalF 𝐸) |
26 | | eqid 2733 |
. . . . . 6
⊢ (𝐷 FuncCat 𝐸) = (𝐷 FuncCat 𝐸) |
27 | 25, 26, 2, 3 | evlfcl 18116 |
. . . . 5
⊢ (𝜑 → (𝐷 evalF 𝐸) ∈ (((𝐷 FuncCat 𝐸) ×c 𝐷) Func 𝐸)) |
28 | | uncf1.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
29 | | uncf1.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
30 | 28, 29 | opelxpd 5672 |
. . . . 5
⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐴 × 𝐵)) |
31 | | uncf2.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝐴) |
32 | | uncf2.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ 𝐵) |
33 | 31, 32 | opelxpd 5672 |
. . . . 5
⊢ (𝜑 → ⟨𝑍, 𝑊⟩ ∈ (𝐴 × 𝐵)) |
34 | | eqid 2733 |
. . . . 5
⊢ (Hom
‘(𝐶
×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷)) |
35 | | uncf2.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑍)) |
36 | | uncf2.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ (𝑌𝐽𝑊)) |
37 | 35, 36 | opelxpd 5672 |
. . . . . 6
⊢ (𝜑 → ⟨𝑅, 𝑆⟩ ∈ ((𝑋𝐻𝑍) × (𝑌𝐽𝑊))) |
38 | | uncf2.h |
. . . . . . 7
⊢ 𝐻 = (Hom ‘𝐶) |
39 | | uncf2.j |
. . . . . . 7
⊢ 𝐽 = (Hom ‘𝐷) |
40 | 10, 11, 12, 38, 39, 28, 29, 31, 32, 34 | xpchom2 18079 |
. . . . . 6
⊢ (𝜑 → (⟨𝑋, 𝑌⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑍, 𝑊⟩) = ((𝑋𝐻𝑍) × (𝑌𝐽𝑊))) |
41 | 37, 40 | eleqtrrd 2837 |
. . . . 5
⊢ (𝜑 → ⟨𝑅, 𝑆⟩ ∈ (⟨𝑋, 𝑌⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑍, 𝑊⟩)) |
42 | 13, 24, 27, 30, 33, 34, 41 | cofu2 17777 |
. . . 4
⊢ (𝜑 → ((⟨𝑋, 𝑌⟩(2nd ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷))))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩) = ((((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))‘⟨𝑋, 𝑌⟩)(2nd ‘(𝐷 evalF 𝐸))((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑍, 𝑊⟩))‘((⟨𝑋, 𝑌⟩(2nd ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩))) |
43 | 9, 42 | eqtrid 2785 |
. . 3
⊢ (𝜑 → (𝑅(⟨𝑋, 𝑌⟩(2nd ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷))))⟨𝑍, 𝑊⟩)𝑆) = ((((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))‘⟨𝑋, 𝑌⟩)(2nd ‘(𝐷 evalF 𝐸))((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑍, 𝑊⟩))‘((⟨𝑋, 𝑌⟩(2nd ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩))) |
44 | 8, 43 | eqtrd 2773 |
. 2
⊢ (𝜑 → (𝑅(⟨𝑋, 𝑌⟩(2nd ‘𝐹)⟨𝑍, 𝑊⟩)𝑆) = ((((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))‘⟨𝑋, 𝑌⟩)(2nd ‘(𝐷 evalF 𝐸))((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑍, 𝑊⟩))‘((⟨𝑋, 𝑌⟩(2nd ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩))) |
45 | 14, 13, 34, 21, 23, 30 | prf1 18093 |
. . . . . 6
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑋, 𝑌⟩) = ⟨((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘⟨𝑋, 𝑌⟩), ((1st ‘(𝐶
2ndF 𝐷))‘⟨𝑋, 𝑌⟩)⟩) |
46 | 13, 20, 4, 30 | cofu1 17775 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘⟨𝑋, 𝑌⟩) = ((1st ‘𝐺)‘((1st
‘(𝐶
1stF 𝐷))‘⟨𝑋, 𝑌⟩))) |
47 | 10, 13, 34, 18, 2, 19, 30 | 1stf1 18085 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘⟨𝑋, 𝑌⟩) = (1st ‘⟨𝑋, 𝑌⟩)) |
48 | | op1stg 7934 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋) |
49 | 28, 29, 48 | syl2anc 585 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘⟨𝑋, 𝑌⟩) = 𝑋) |
50 | 47, 49 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘⟨𝑋, 𝑌⟩) = 𝑋) |
51 | 50 | fveq2d 6847 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝐺)‘((1st ‘(𝐶
1stF 𝐷))‘⟨𝑋, 𝑌⟩)) = ((1st ‘𝐺)‘𝑋)) |
52 | 46, 51 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘⟨𝑋, 𝑌⟩) = ((1st ‘𝐺)‘𝑋)) |
53 | 10, 13, 34, 18, 2, 22, 30 | 2ndf1 18088 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘⟨𝑋, 𝑌⟩) = (2nd ‘⟨𝑋, 𝑌⟩)) |
54 | | op2ndg 7935 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌) |
55 | 28, 29, 54 | syl2anc 585 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘⟨𝑋, 𝑌⟩) = 𝑌) |
56 | 53, 55 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘⟨𝑋, 𝑌⟩) = 𝑌) |
57 | 52, 56 | opeq12d 4839 |
. . . . . 6
⊢ (𝜑 → ⟨((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘⟨𝑋, 𝑌⟩), ((1st ‘(𝐶
2ndF 𝐷))‘⟨𝑋, 𝑌⟩)⟩ = ⟨((1st
‘𝐺)‘𝑋), 𝑌⟩) |
58 | 45, 57 | eqtrd 2773 |
. . . . 5
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑋, 𝑌⟩) = ⟨((1st
‘𝐺)‘𝑋), 𝑌⟩) |
59 | 14, 13, 34, 21, 23, 33 | prf1 18093 |
. . . . . 6
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑍, 𝑊⟩) = ⟨((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘⟨𝑍, 𝑊⟩), ((1st ‘(𝐶
2ndF 𝐷))‘⟨𝑍, 𝑊⟩)⟩) |
60 | 13, 20, 4, 33 | cofu1 17775 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘⟨𝑍, 𝑊⟩) = ((1st ‘𝐺)‘((1st
‘(𝐶
1stF 𝐷))‘⟨𝑍, 𝑊⟩))) |
61 | 10, 13, 34, 18, 2, 19, 33 | 1stf1 18085 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘⟨𝑍, 𝑊⟩) = (1st ‘⟨𝑍, 𝑊⟩)) |
62 | | op1stg 7934 |
. . . . . . . . . . 11
⊢ ((𝑍 ∈ 𝐴 ∧ 𝑊 ∈ 𝐵) → (1st ‘⟨𝑍, 𝑊⟩) = 𝑍) |
63 | 31, 32, 62 | syl2anc 585 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘⟨𝑍, 𝑊⟩) = 𝑍) |
64 | 61, 63 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘⟨𝑍, 𝑊⟩) = 𝑍) |
65 | 64 | fveq2d 6847 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝐺)‘((1st ‘(𝐶
1stF 𝐷))‘⟨𝑍, 𝑊⟩)) = ((1st ‘𝐺)‘𝑍)) |
66 | 60, 65 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘⟨𝑍, 𝑊⟩) = ((1st ‘𝐺)‘𝑍)) |
67 | 10, 13, 34, 18, 2, 22, 33 | 2ndf1 18088 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘⟨𝑍, 𝑊⟩) = (2nd ‘⟨𝑍, 𝑊⟩)) |
68 | | op2ndg 7935 |
. . . . . . . . 9
⊢ ((𝑍 ∈ 𝐴 ∧ 𝑊 ∈ 𝐵) → (2nd ‘⟨𝑍, 𝑊⟩) = 𝑊) |
69 | 31, 32, 68 | syl2anc 585 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘⟨𝑍, 𝑊⟩) = 𝑊) |
70 | 67, 69 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘⟨𝑍, 𝑊⟩) = 𝑊) |
71 | 66, 70 | opeq12d 4839 |
. . . . . 6
⊢ (𝜑 → ⟨((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘⟨𝑍, 𝑊⟩), ((1st ‘(𝐶
2ndF 𝐷))‘⟨𝑍, 𝑊⟩)⟩ = ⟨((1st
‘𝐺)‘𝑍), 𝑊⟩) |
72 | 59, 71 | eqtrd 2773 |
. . . . 5
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑍, 𝑊⟩) = ⟨((1st
‘𝐺)‘𝑍), 𝑊⟩) |
73 | 58, 72 | oveq12d 7376 |
. . . 4
⊢ (𝜑 → (((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑋, 𝑌⟩)(2nd ‘(𝐷 evalF 𝐸))((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑍, 𝑊⟩)) = (⟨((1st
‘𝐺)‘𝑋), 𝑌⟩(2nd ‘(𝐷 evalF 𝐸))⟨((1st
‘𝐺)‘𝑍), 𝑊⟩)) |
74 | 14, 13, 34, 21, 23, 30, 33, 41 | prf2 18095 |
. . . . 5
⊢ (𝜑 → ((⟨𝑋, 𝑌⟩(2nd ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩) = ⟨((⟨𝑋, 𝑌⟩(2nd ‘(𝐺 ∘func
(𝐶
1stF 𝐷)))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩), ((⟨𝑋, 𝑌⟩(2nd ‘(𝐶
2ndF 𝐷))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩)⟩) |
75 | 13, 20, 4, 30, 33, 34, 41 | cofu2 17777 |
. . . . . . 7
⊢ (𝜑 → ((⟨𝑋, 𝑌⟩(2nd ‘(𝐺 ∘func
(𝐶
1stF 𝐷)))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩) = ((((1st ‘(𝐶
1stF 𝐷))‘⟨𝑋, 𝑌⟩)(2nd ‘𝐺)((1st ‘(𝐶
1stF 𝐷))‘⟨𝑍, 𝑊⟩))‘((⟨𝑋, 𝑌⟩(2nd ‘(𝐶
1stF 𝐷))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩))) |
76 | 50, 64 | oveq12d 7376 |
. . . . . . . 8
⊢ (𝜑 → (((1st
‘(𝐶
1stF 𝐷))‘⟨𝑋, 𝑌⟩)(2nd ‘𝐺)((1st ‘(𝐶
1stF 𝐷))‘⟨𝑍, 𝑊⟩)) = (𝑋(2nd ‘𝐺)𝑍)) |
77 | 10, 13, 34, 18, 2, 19, 30, 33 | 1stf2 18086 |
. . . . . . . . . 10
⊢ (𝜑 → (⟨𝑋, 𝑌⟩(2nd ‘(𝐶
1stF 𝐷))⟨𝑍, 𝑊⟩) = (1st ↾
(⟨𝑋, 𝑌⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑍, 𝑊⟩))) |
78 | 77 | fveq1d 6845 |
. . . . . . . . 9
⊢ (𝜑 → ((⟨𝑋, 𝑌⟩(2nd ‘(𝐶
1stF 𝐷))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩) = ((1st ↾
(⟨𝑋, 𝑌⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑍, 𝑊⟩))‘⟨𝑅, 𝑆⟩)) |
79 | 41 | fvresd 6863 |
. . . . . . . . 9
⊢ (𝜑 → ((1st ↾
(⟨𝑋, 𝑌⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑍, 𝑊⟩))‘⟨𝑅, 𝑆⟩) = (1st ‘⟨𝑅, 𝑆⟩)) |
80 | | op1stg 7934 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ (𝑋𝐻𝑍) ∧ 𝑆 ∈ (𝑌𝐽𝑊)) → (1st ‘⟨𝑅, 𝑆⟩) = 𝑅) |
81 | 35, 36, 80 | syl2anc 585 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘⟨𝑅, 𝑆⟩) = 𝑅) |
82 | 78, 79, 81 | 3eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((⟨𝑋, 𝑌⟩(2nd ‘(𝐶
1stF 𝐷))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩) = 𝑅) |
83 | 76, 82 | fveq12d 6850 |
. . . . . . 7
⊢ (𝜑 → ((((1st
‘(𝐶
1stF 𝐷))‘⟨𝑋, 𝑌⟩)(2nd ‘𝐺)((1st ‘(𝐶
1stF 𝐷))‘⟨𝑍, 𝑊⟩))‘((⟨𝑋, 𝑌⟩(2nd ‘(𝐶
1stF 𝐷))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩)) = ((𝑋(2nd ‘𝐺)𝑍)‘𝑅)) |
84 | 75, 83 | eqtrd 2773 |
. . . . . 6
⊢ (𝜑 → ((⟨𝑋, 𝑌⟩(2nd ‘(𝐺 ∘func
(𝐶
1stF 𝐷)))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩) = ((𝑋(2nd ‘𝐺)𝑍)‘𝑅)) |
85 | 10, 13, 34, 18, 2, 22, 30, 33 | 2ndf2 18089 |
. . . . . . . 8
⊢ (𝜑 → (⟨𝑋, 𝑌⟩(2nd ‘(𝐶
2ndF 𝐷))⟨𝑍, 𝑊⟩) = (2nd ↾
(⟨𝑋, 𝑌⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑍, 𝑊⟩))) |
86 | 85 | fveq1d 6845 |
. . . . . . 7
⊢ (𝜑 → ((⟨𝑋, 𝑌⟩(2nd ‘(𝐶
2ndF 𝐷))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩) = ((2nd ↾
(⟨𝑋, 𝑌⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑍, 𝑊⟩))‘⟨𝑅, 𝑆⟩)) |
87 | 41 | fvresd 6863 |
. . . . . . 7
⊢ (𝜑 → ((2nd ↾
(⟨𝑋, 𝑌⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑍, 𝑊⟩))‘⟨𝑅, 𝑆⟩) = (2nd ‘⟨𝑅, 𝑆⟩)) |
88 | | op2ndg 7935 |
. . . . . . . 8
⊢ ((𝑅 ∈ (𝑋𝐻𝑍) ∧ 𝑆 ∈ (𝑌𝐽𝑊)) → (2nd ‘⟨𝑅, 𝑆⟩) = 𝑆) |
89 | 35, 36, 88 | syl2anc 585 |
. . . . . . 7
⊢ (𝜑 → (2nd
‘⟨𝑅, 𝑆⟩) = 𝑆) |
90 | 86, 87, 89 | 3eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((⟨𝑋, 𝑌⟩(2nd ‘(𝐶
2ndF 𝐷))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩) = 𝑆) |
91 | 84, 90 | opeq12d 4839 |
. . . . 5
⊢ (𝜑 → ⟨((⟨𝑋, 𝑌⟩(2nd ‘(𝐺 ∘func
(𝐶
1stF 𝐷)))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩), ((⟨𝑋, 𝑌⟩(2nd ‘(𝐶
2ndF 𝐷))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩)⟩ = ⟨((𝑋(2nd ‘𝐺)𝑍)‘𝑅), 𝑆⟩) |
92 | 74, 91 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → ((⟨𝑋, 𝑌⟩(2nd ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩) = ⟨((𝑋(2nd ‘𝐺)𝑍)‘𝑅), 𝑆⟩) |
93 | 73, 92 | fveq12d 6850 |
. . 3
⊢ (𝜑 → ((((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑋, 𝑌⟩)(2nd ‘(𝐷 evalF 𝐸))((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑍, 𝑊⟩))‘((⟨𝑋, 𝑌⟩(2nd ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩)) = ((⟨((1st
‘𝐺)‘𝑋), 𝑌⟩(2nd ‘(𝐷 evalF 𝐸))⟨((1st
‘𝐺)‘𝑍), 𝑊⟩)‘⟨((𝑋(2nd ‘𝐺)𝑍)‘𝑅), 𝑆⟩)) |
94 | | df-ov 7361 |
. . 3
⊢ (((𝑋(2nd ‘𝐺)𝑍)‘𝑅)(⟨((1st ‘𝐺)‘𝑋), 𝑌⟩(2nd ‘(𝐷 evalF 𝐸))⟨((1st
‘𝐺)‘𝑍), 𝑊⟩)𝑆) = ((⟨((1st ‘𝐺)‘𝑋), 𝑌⟩(2nd ‘(𝐷 evalF 𝐸))⟨((1st
‘𝐺)‘𝑍), 𝑊⟩)‘⟨((𝑋(2nd ‘𝐺)𝑍)‘𝑅), 𝑆⟩) |
95 | 93, 94 | eqtr4di 2791 |
. 2
⊢ (𝜑 → ((((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑋, 𝑌⟩)(2nd ‘(𝐷 evalF 𝐸))((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑍, 𝑊⟩))‘((⟨𝑋, 𝑌⟩(2nd ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))⟨𝑍, 𝑊⟩)‘⟨𝑅, 𝑆⟩)) = (((𝑋(2nd ‘𝐺)𝑍)‘𝑅)(⟨((1st ‘𝐺)‘𝑋), 𝑌⟩(2nd ‘(𝐷 evalF 𝐸))⟨((1st
‘𝐺)‘𝑍), 𝑊⟩)𝑆)) |
96 | | eqid 2733 |
. . 3
⊢
(comp‘𝐸) =
(comp‘𝐸) |
97 | | eqid 2733 |
. . 3
⊢ (𝐷 Nat 𝐸) = (𝐷 Nat 𝐸) |
98 | 26 | fucbas 17853 |
. . . . 5
⊢ (𝐷 Func 𝐸) = (Base‘(𝐷 FuncCat 𝐸)) |
99 | | relfunc 17753 |
. . . . . 6
⊢ Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) |
100 | | 1st2ndbr 7975 |
. . . . . 6
⊢ ((Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) ∧ 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) → (1st ‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
101 | 99, 4, 100 | sylancr 588 |
. . . . 5
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
102 | 11, 98, 101 | funcf1 17757 |
. . . 4
⊢ (𝜑 → (1st
‘𝐺):𝐴⟶(𝐷 Func 𝐸)) |
103 | 102, 28 | ffvelcdmd 7037 |
. . 3
⊢ (𝜑 → ((1st
‘𝐺)‘𝑋) ∈ (𝐷 Func 𝐸)) |
104 | 102, 31 | ffvelcdmd 7037 |
. . 3
⊢ (𝜑 → ((1st
‘𝐺)‘𝑍) ∈ (𝐷 Func 𝐸)) |
105 | | eqid 2733 |
. . 3
⊢
(⟨((1st ‘𝐺)‘𝑋), 𝑌⟩(2nd ‘(𝐷 evalF 𝐸))⟨((1st
‘𝐺)‘𝑍), 𝑊⟩) = (⟨((1st
‘𝐺)‘𝑋), 𝑌⟩(2nd ‘(𝐷 evalF 𝐸))⟨((1st
‘𝐺)‘𝑍), 𝑊⟩) |
106 | 26, 97 | fuchom 17854 |
. . . . 5
⊢ (𝐷 Nat 𝐸) = (Hom ‘(𝐷 FuncCat 𝐸)) |
107 | 11, 38, 106, 101, 28, 31 | funcf2 17759 |
. . . 4
⊢ (𝜑 → (𝑋(2nd ‘𝐺)𝑍):(𝑋𝐻𝑍)⟶(((1st ‘𝐺)‘𝑋)(𝐷 Nat 𝐸)((1st ‘𝐺)‘𝑍))) |
108 | 107, 35 | ffvelcdmd 7037 |
. . 3
⊢ (𝜑 → ((𝑋(2nd ‘𝐺)𝑍)‘𝑅) ∈ (((1st ‘𝐺)‘𝑋)(𝐷 Nat 𝐸)((1st ‘𝐺)‘𝑍))) |
109 | 25, 2, 3, 12, 39, 96, 97, 103, 104, 29, 32, 105, 108, 36 | evlf2val 18113 |
. 2
⊢ (𝜑 → (((𝑋(2nd ‘𝐺)𝑍)‘𝑅)(⟨((1st ‘𝐺)‘𝑋), 𝑌⟩(2nd ‘(𝐷 evalF 𝐸))⟨((1st
‘𝐺)‘𝑍), 𝑊⟩)𝑆) = ((((𝑋(2nd ‘𝐺)𝑍)‘𝑅)‘𝑊)(⟨((1st
‘((1st ‘𝐺)‘𝑋))‘𝑌), ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑊)⟩(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑍))‘𝑊))((𝑌(2nd ‘((1st
‘𝐺)‘𝑋))𝑊)‘𝑆))) |
110 | 44, 95, 109 | 3eqtrd 2777 |
1
⊢ (𝜑 → (𝑅(⟨𝑋, 𝑌⟩(2nd ‘𝐹)⟨𝑍, 𝑊⟩)𝑆) = ((((𝑋(2nd ‘𝐺)𝑍)‘𝑅)‘𝑊)(⟨((1st
‘((1st ‘𝐺)‘𝑋))‘𝑌), ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑊)⟩(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑍))‘𝑊))((𝑌(2nd ‘((1st
‘𝐺)‘𝑋))𝑊)‘𝑆))) |