Proof of Theorem uncf2
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 16874 |
. . . . . 6
⊢ (𝜑 → 𝐹 = ((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))) |
6 | 5 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 → (2nd
‘𝐹) = (2nd
‘((𝐷
evalF 𝐸)
∘func ((𝐺 ∘func (𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷))))) |
7 | 6 | oveqd 6667 |
. . . 4
⊢ (𝜑 → (〈𝑋, 𝑌〉(2nd ‘𝐹)〈𝑍, 𝑊〉) = (〈𝑋, 𝑌〉(2nd ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷))))〈𝑍, 𝑊〉)) |
8 | 7 | oveqd 6667 |
. . 3
⊢ (𝜑 → (𝑅(〈𝑋, 𝑌〉(2nd ‘𝐹)〈𝑍, 𝑊〉)𝑆) = (𝑅(〈𝑋, 𝑌〉(2nd ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷))))〈𝑍, 𝑊〉)𝑆)) |
9 | | df-ov 6653 |
. . . 4
⊢ (𝑅(〈𝑋, 𝑌〉(2nd ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷))))〈𝑍, 𝑊〉)𝑆) = ((〈𝑋, 𝑌〉(2nd ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷))))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉) |
10 | | eqid 2622 |
. . . . . 6
⊢ (𝐶 ×c
𝐷) = (𝐶 ×c 𝐷) |
11 | | uncf1.a |
. . . . . 6
⊢ 𝐴 = (Base‘𝐶) |
12 | | uncf1.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐷) |
13 | 10, 11, 12 | xpcbas 16818 |
. . . . 5
⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷)) |
14 | | eqid 2622 |
. . . . . 6
⊢ ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)) = ((𝐺 ∘func (𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)) |
15 | | eqid 2622 |
. . . . . 6
⊢ ((𝐷 FuncCat 𝐸) ×c 𝐷) = ((𝐷 FuncCat 𝐸) ×c 𝐷) |
16 | | funcrcl 16523 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)) → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
17 | 4, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
18 | 17 | simpld 475 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ Cat) |
19 | | eqid 2622 |
. . . . . . . 8
⊢ (𝐶
1stF 𝐷) = (𝐶 1stF 𝐷) |
20 | 10, 18, 2, 19 | 1stfcl 16837 |
. . . . . . 7
⊢ (𝜑 → (𝐶 1stF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐶)) |
21 | 20, 4 | cofucl 16548 |
. . . . . 6
⊢ (𝜑 → (𝐺 ∘func (𝐶
1stF 𝐷)) ∈ ((𝐶 ×c 𝐷) Func (𝐷 FuncCat 𝐸))) |
22 | | eqid 2622 |
. . . . . . 7
⊢ (𝐶
2ndF 𝐷) = (𝐶 2ndF 𝐷) |
23 | 10, 18, 2, 22 | 2ndfcl 16838 |
. . . . . 6
⊢ (𝜑 → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷)) |
24 | 14, 15, 21, 23 | prfcl 16843 |
. . . . 5
⊢ (𝜑 → ((𝐺 ∘func (𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)) ∈ ((𝐶 ×c 𝐷) Func ((𝐷 FuncCat 𝐸) ×c 𝐷))) |
25 | | eqid 2622 |
. . . . . 6
⊢ (𝐷 evalF 𝐸) = (𝐷 evalF 𝐸) |
26 | | eqid 2622 |
. . . . . 6
⊢ (𝐷 FuncCat 𝐸) = (𝐷 FuncCat 𝐸) |
27 | 25, 26, 2, 3 | evlfcl 16862 |
. . . . 5
⊢ (𝜑 → (𝐷 evalF 𝐸) ∈ (((𝐷 FuncCat 𝐸) ×c 𝐷) Func 𝐸)) |
28 | | uncf1.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
29 | | uncf1.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
30 | | opelxpi 5148 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐴 × 𝐵)) |
31 | 28, 29, 30 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝐴 × 𝐵)) |
32 | | uncf2.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝐴) |
33 | | uncf2.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ 𝐵) |
34 | | opelxpi 5148 |
. . . . . 6
⊢ ((𝑍 ∈ 𝐴 ∧ 𝑊 ∈ 𝐵) → 〈𝑍, 𝑊〉 ∈ (𝐴 × 𝐵)) |
35 | 32, 33, 34 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 〈𝑍, 𝑊〉 ∈ (𝐴 × 𝐵)) |
36 | | eqid 2622 |
. . . . 5
⊢ (Hom
‘(𝐶
×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷)) |
37 | | uncf2.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑍)) |
38 | | uncf2.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ (𝑌𝐽𝑊)) |
39 | | opelxpi 5148 |
. . . . . . 7
⊢ ((𝑅 ∈ (𝑋𝐻𝑍) ∧ 𝑆 ∈ (𝑌𝐽𝑊)) → 〈𝑅, 𝑆〉 ∈ ((𝑋𝐻𝑍) × (𝑌𝐽𝑊))) |
40 | 37, 38, 39 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → 〈𝑅, 𝑆〉 ∈ ((𝑋𝐻𝑍) × (𝑌𝐽𝑊))) |
41 | | uncf2.h |
. . . . . . 7
⊢ 𝐻 = (Hom ‘𝐶) |
42 | | uncf2.j |
. . . . . . 7
⊢ 𝐽 = (Hom ‘𝐷) |
43 | 10, 11, 12, 41, 42, 28, 29, 32, 33, 36 | xpchom2 16826 |
. . . . . 6
⊢ (𝜑 → (〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑍, 𝑊〉) = ((𝑋𝐻𝑍) × (𝑌𝐽𝑊))) |
44 | 40, 43 | eleqtrrd 2704 |
. . . . 5
⊢ (𝜑 → 〈𝑅, 𝑆〉 ∈ (〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑍, 𝑊〉)) |
45 | 13, 24, 27, 31, 35, 36, 44 | cofu2 16546 |
. . . 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 𝐷)))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉))) |
46 | 9, 45 | syl5eq 2668 |
. . 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 𝐷)))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉))) |
47 | 8, 46 | eqtrd 2656 |
. 2
⊢ (𝜑 → (𝑅(〈𝑋, 𝑌〉(2nd ‘𝐹)〈𝑍, 𝑊〉)𝑆) = ((((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))‘〈𝑋, 𝑌〉)(2nd ‘(𝐷 evalF 𝐸))((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑍, 𝑊〉))‘((〈𝑋, 𝑌〉(2nd ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉))) |
48 | 14, 13, 36, 21, 23, 31 | prf1 16840 |
. . . . . 6
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉) = 〈((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑋, 𝑌〉), ((1st ‘(𝐶
2ndF 𝐷))‘〈𝑋, 𝑌〉)〉) |
49 | 13, 20, 4, 31 | cofu1 16544 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑋, 𝑌〉) = ((1st ‘𝐺)‘((1st
‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉))) |
50 | 10, 13, 36, 18, 2, 19, 31 | 1stf1 16832 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉) = (1st ‘〈𝑋, 𝑌〉)) |
51 | | op1stg 7180 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (1st ‘〈𝑋, 𝑌〉) = 𝑋) |
52 | 28, 29, 51 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘〈𝑋, 𝑌〉) = 𝑋) |
53 | 50, 52 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉) = 𝑋) |
54 | 53 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝐺)‘((1st ‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉)) = ((1st ‘𝐺)‘𝑋)) |
55 | 49, 54 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑋, 𝑌〉) = ((1st ‘𝐺)‘𝑋)) |
56 | 10, 13, 36, 18, 2, 22, 31 | 2ndf1 16835 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘〈𝑋, 𝑌〉) = (2nd ‘〈𝑋, 𝑌〉)) |
57 | | op2ndg 7181 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (2nd ‘〈𝑋, 𝑌〉) = 𝑌) |
58 | 28, 29, 57 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘〈𝑋, 𝑌〉) = 𝑌) |
59 | 56, 58 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘〈𝑋, 𝑌〉) = 𝑌) |
60 | 55, 59 | opeq12d 4410 |
. . . . . 6
⊢ (𝜑 → 〈((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑋, 𝑌〉), ((1st ‘(𝐶
2ndF 𝐷))‘〈𝑋, 𝑌〉)〉 = 〈((1st
‘𝐺)‘𝑋), 𝑌〉) |
61 | 48, 60 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉) = 〈((1st
‘𝐺)‘𝑋), 𝑌〉) |
62 | 14, 13, 36, 21, 23, 35 | prf1 16840 |
. . . . . 6
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑍, 𝑊〉) = 〈((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑍, 𝑊〉), ((1st ‘(𝐶
2ndF 𝐷))‘〈𝑍, 𝑊〉)〉) |
63 | 13, 20, 4, 35 | cofu1 16544 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑍, 𝑊〉) = ((1st ‘𝐺)‘((1st
‘(𝐶
1stF 𝐷))‘〈𝑍, 𝑊〉))) |
64 | 10, 13, 36, 18, 2, 19, 35 | 1stf1 16832 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘〈𝑍, 𝑊〉) = (1st ‘〈𝑍, 𝑊〉)) |
65 | | op1stg 7180 |
. . . . . . . . . . 11
⊢ ((𝑍 ∈ 𝐴 ∧ 𝑊 ∈ 𝐵) → (1st ‘〈𝑍, 𝑊〉) = 𝑍) |
66 | 32, 33, 65 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘〈𝑍, 𝑊〉) = 𝑍) |
67 | 64, 66 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘〈𝑍, 𝑊〉) = 𝑍) |
68 | 67 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝐺)‘((1st ‘(𝐶
1stF 𝐷))‘〈𝑍, 𝑊〉)) = ((1st ‘𝐺)‘𝑍)) |
69 | 63, 68 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑍, 𝑊〉) = ((1st ‘𝐺)‘𝑍)) |
70 | 10, 13, 36, 18, 2, 22, 35 | 2ndf1 16835 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘〈𝑍, 𝑊〉) = (2nd ‘〈𝑍, 𝑊〉)) |
71 | | op2ndg 7181 |
. . . . . . . . 9
⊢ ((𝑍 ∈ 𝐴 ∧ 𝑊 ∈ 𝐵) → (2nd ‘〈𝑍, 𝑊〉) = 𝑊) |
72 | 32, 33, 71 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘〈𝑍, 𝑊〉) = 𝑊) |
73 | 70, 72 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘〈𝑍, 𝑊〉) = 𝑊) |
74 | 69, 73 | opeq12d 4410 |
. . . . . 6
⊢ (𝜑 → 〈((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑍, 𝑊〉), ((1st ‘(𝐶
2ndF 𝐷))‘〈𝑍, 𝑊〉)〉 = 〈((1st
‘𝐺)‘𝑍), 𝑊〉) |
75 | 62, 74 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑍, 𝑊〉) = 〈((1st
‘𝐺)‘𝑍), 𝑊〉) |
76 | 61, 75 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → (((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉)(2nd ‘(𝐷 evalF 𝐸))((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑍, 𝑊〉)) = (〈((1st
‘𝐺)‘𝑋), 𝑌〉(2nd ‘(𝐷 evalF 𝐸))〈((1st
‘𝐺)‘𝑍), 𝑊〉)) |
77 | 14, 13, 36, 21, 23, 31, 35, 44 | prf2 16842 |
. . . . 5
⊢ (𝜑 → ((〈𝑋, 𝑌〉(2nd ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉) = 〈((〈𝑋, 𝑌〉(2nd ‘(𝐺 ∘func
(𝐶
1stF 𝐷)))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉), ((〈𝑋, 𝑌〉(2nd ‘(𝐶
2ndF 𝐷))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉)〉) |
78 | 13, 20, 4, 31, 35, 36, 44 | cofu2 16546 |
. . . . . . 7
⊢ (𝜑 → ((〈𝑋, 𝑌〉(2nd ‘(𝐺 ∘func
(𝐶
1stF 𝐷)))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉) = ((((1st ‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉)(2nd ‘𝐺)((1st ‘(𝐶
1stF 𝐷))‘〈𝑍, 𝑊〉))‘((〈𝑋, 𝑌〉(2nd ‘(𝐶
1stF 𝐷))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉))) |
79 | 53, 67 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝜑 → (((1st
‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉)(2nd ‘𝐺)((1st ‘(𝐶
1stF 𝐷))‘〈𝑍, 𝑊〉)) = (𝑋(2nd ‘𝐺)𝑍)) |
80 | 10, 13, 36, 18, 2, 19, 31, 35 | 1stf2 16833 |
. . . . . . . . . 10
⊢ (𝜑 → (〈𝑋, 𝑌〉(2nd ‘(𝐶
1stF 𝐷))〈𝑍, 𝑊〉) = (1st ↾
(〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑍, 𝑊〉))) |
81 | 80 | fveq1d 6193 |
. . . . . . . . 9
⊢ (𝜑 → ((〈𝑋, 𝑌〉(2nd ‘(𝐶
1stF 𝐷))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉) = ((1st ↾
(〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑍, 𝑊〉))‘〈𝑅, 𝑆〉)) |
82 | | fvres 6207 |
. . . . . . . . . 10
⊢
(〈𝑅, 𝑆〉 ∈ (〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑍, 𝑊〉) → ((1st ↾
(〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑍, 𝑊〉))‘〈𝑅, 𝑆〉) = (1st ‘〈𝑅, 𝑆〉)) |
83 | 44, 82 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((1st ↾
(〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑍, 𝑊〉))‘〈𝑅, 𝑆〉) = (1st ‘〈𝑅, 𝑆〉)) |
84 | | op1stg 7180 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ (𝑋𝐻𝑍) ∧ 𝑆 ∈ (𝑌𝐽𝑊)) → (1st ‘〈𝑅, 𝑆〉) = 𝑅) |
85 | 37, 38, 84 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘〈𝑅, 𝑆〉) = 𝑅) |
86 | 81, 83, 85 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝜑 → ((〈𝑋, 𝑌〉(2nd ‘(𝐶
1stF 𝐷))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉) = 𝑅) |
87 | 79, 86 | fveq12d 6197 |
. . . . . . 7
⊢ (𝜑 → ((((1st
‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉)(2nd ‘𝐺)((1st ‘(𝐶
1stF 𝐷))‘〈𝑍, 𝑊〉))‘((〈𝑋, 𝑌〉(2nd ‘(𝐶
1stF 𝐷))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉)) = ((𝑋(2nd ‘𝐺)𝑍)‘𝑅)) |
88 | 78, 87 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → ((〈𝑋, 𝑌〉(2nd ‘(𝐺 ∘func
(𝐶
1stF 𝐷)))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉) = ((𝑋(2nd ‘𝐺)𝑍)‘𝑅)) |
89 | 10, 13, 36, 18, 2, 22, 31, 35 | 2ndf2 16836 |
. . . . . . . 8
⊢ (𝜑 → (〈𝑋, 𝑌〉(2nd ‘(𝐶
2ndF 𝐷))〈𝑍, 𝑊〉) = (2nd ↾
(〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑍, 𝑊〉))) |
90 | 89 | fveq1d 6193 |
. . . . . . 7
⊢ (𝜑 → ((〈𝑋, 𝑌〉(2nd ‘(𝐶
2ndF 𝐷))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉) = ((2nd ↾
(〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑍, 𝑊〉))‘〈𝑅, 𝑆〉)) |
91 | | fvres 6207 |
. . . . . . . 8
⊢
(〈𝑅, 𝑆〉 ∈ (〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑍, 𝑊〉) → ((2nd ↾
(〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑍, 𝑊〉))‘〈𝑅, 𝑆〉) = (2nd ‘〈𝑅, 𝑆〉)) |
92 | 44, 91 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((2nd ↾
(〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑍, 𝑊〉))‘〈𝑅, 𝑆〉) = (2nd ‘〈𝑅, 𝑆〉)) |
93 | | op2ndg 7181 |
. . . . . . . 8
⊢ ((𝑅 ∈ (𝑋𝐻𝑍) ∧ 𝑆 ∈ (𝑌𝐽𝑊)) → (2nd ‘〈𝑅, 𝑆〉) = 𝑆) |
94 | 37, 38, 93 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (2nd
‘〈𝑅, 𝑆〉) = 𝑆) |
95 | 90, 92, 94 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝜑 → ((〈𝑋, 𝑌〉(2nd ‘(𝐶
2ndF 𝐷))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉) = 𝑆) |
96 | 88, 95 | opeq12d 4410 |
. . . . 5
⊢ (𝜑 → 〈((〈𝑋, 𝑌〉(2nd ‘(𝐺 ∘func
(𝐶
1stF 𝐷)))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉), ((〈𝑋, 𝑌〉(2nd ‘(𝐶
2ndF 𝐷))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉)〉 = 〈((𝑋(2nd ‘𝐺)𝑍)‘𝑅), 𝑆〉) |
97 | 77, 96 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → ((〈𝑋, 𝑌〉(2nd ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉) = 〈((𝑋(2nd ‘𝐺)𝑍)‘𝑅), 𝑆〉) |
98 | 76, 97 | fveq12d 6197 |
. . 3
⊢ (𝜑 → ((((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉)(2nd ‘(𝐷 evalF 𝐸))((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑍, 𝑊〉))‘((〈𝑋, 𝑌〉(2nd ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉)) = ((〈((1st
‘𝐺)‘𝑋), 𝑌〉(2nd ‘(𝐷 evalF 𝐸))〈((1st
‘𝐺)‘𝑍), 𝑊〉)‘〈((𝑋(2nd ‘𝐺)𝑍)‘𝑅), 𝑆〉)) |
99 | | df-ov 6653 |
. . 3
⊢ (((𝑋(2nd ‘𝐺)𝑍)‘𝑅)(〈((1st ‘𝐺)‘𝑋), 𝑌〉(2nd ‘(𝐷 evalF 𝐸))〈((1st
‘𝐺)‘𝑍), 𝑊〉)𝑆) = ((〈((1st ‘𝐺)‘𝑋), 𝑌〉(2nd ‘(𝐷 evalF 𝐸))〈((1st
‘𝐺)‘𝑍), 𝑊〉)‘〈((𝑋(2nd ‘𝐺)𝑍)‘𝑅), 𝑆〉) |
100 | 98, 99 | syl6eqr 2674 |
. 2
⊢ (𝜑 → ((((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉)(2nd ‘(𝐷 evalF 𝐸))((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑍, 𝑊〉))‘((〈𝑋, 𝑌〉(2nd ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))〈𝑍, 𝑊〉)‘〈𝑅, 𝑆〉)) = (((𝑋(2nd ‘𝐺)𝑍)‘𝑅)(〈((1st ‘𝐺)‘𝑋), 𝑌〉(2nd ‘(𝐷 evalF 𝐸))〈((1st
‘𝐺)‘𝑍), 𝑊〉)𝑆)) |
101 | | eqid 2622 |
. . 3
⊢
(comp‘𝐸) =
(comp‘𝐸) |
102 | | eqid 2622 |
. . 3
⊢ (𝐷 Nat 𝐸) = (𝐷 Nat 𝐸) |
103 | 26 | fucbas 16620 |
. . . . 5
⊢ (𝐷 Func 𝐸) = (Base‘(𝐷 FuncCat 𝐸)) |
104 | | relfunc 16522 |
. . . . . 6
⊢ Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) |
105 | | 1st2ndbr 7217 |
. . . . . 6
⊢ ((Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) ∧ 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) → (1st ‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
106 | 104, 4, 105 | sylancr 695 |
. . . . 5
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
107 | 11, 103, 106 | funcf1 16526 |
. . . 4
⊢ (𝜑 → (1st
‘𝐺):𝐴⟶(𝐷 Func 𝐸)) |
108 | 107, 28 | ffvelrnd 6360 |
. . 3
⊢ (𝜑 → ((1st
‘𝐺)‘𝑋) ∈ (𝐷 Func 𝐸)) |
109 | 107, 32 | ffvelrnd 6360 |
. . 3
⊢ (𝜑 → ((1st
‘𝐺)‘𝑍) ∈ (𝐷 Func 𝐸)) |
110 | | eqid 2622 |
. . 3
⊢
(〈((1st ‘𝐺)‘𝑋), 𝑌〉(2nd ‘(𝐷 evalF 𝐸))〈((1st
‘𝐺)‘𝑍), 𝑊〉) = (〈((1st
‘𝐺)‘𝑋), 𝑌〉(2nd ‘(𝐷 evalF 𝐸))〈((1st
‘𝐺)‘𝑍), 𝑊〉) |
111 | 26, 102 | fuchom 16621 |
. . . . 5
⊢ (𝐷 Nat 𝐸) = (Hom ‘(𝐷 FuncCat 𝐸)) |
112 | 11, 41, 111, 106, 28, 32 | funcf2 16528 |
. . . 4
⊢ (𝜑 → (𝑋(2nd ‘𝐺)𝑍):(𝑋𝐻𝑍)⟶(((1st ‘𝐺)‘𝑋)(𝐷 Nat 𝐸)((1st ‘𝐺)‘𝑍))) |
113 | 112, 37 | ffvelrnd 6360 |
. . 3
⊢ (𝜑 → ((𝑋(2nd ‘𝐺)𝑍)‘𝑅) ∈ (((1st ‘𝐺)‘𝑋)(𝐷 Nat 𝐸)((1st ‘𝐺)‘𝑍))) |
114 | 25, 2, 3, 12, 42, 101, 102, 108, 109, 29, 33, 110, 113, 38 | evlf2val 16859 |
. 2
⊢ (𝜑 → (((𝑋(2nd ‘𝐺)𝑍)‘𝑅)(〈((1st ‘𝐺)‘𝑋), 𝑌〉(2nd ‘(𝐷 evalF 𝐸))〈((1st
‘𝐺)‘𝑍), 𝑊〉)𝑆) = ((((𝑋(2nd ‘𝐺)𝑍)‘𝑅)‘𝑊)(〈((1st
‘((1st ‘𝐺)‘𝑋))‘𝑌), ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑊)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑍))‘𝑊))((𝑌(2nd ‘((1st
‘𝐺)‘𝑋))𝑊)‘𝑆))) |
115 | 47, 100, 114 | 3eqtrd 2660 |
1
⊢ (𝜑 → (𝑅(〈𝑋, 𝑌〉(2nd ‘𝐹)〈𝑍, 𝑊〉)𝑆) = ((((𝑋(2nd ‘𝐺)𝑍)‘𝑅)‘𝑊)(〈((1st
‘((1st ‘𝐺)‘𝑋))‘𝑌), ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑊)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑍))‘𝑊))((𝑌(2nd ‘((1st
‘𝐺)‘𝑋))𝑊)‘𝑆))) |