Step | Hyp | Ref
| Expression |
1 | | homdmcoa.o |
. . 3
⊢ · =
(compa‘𝐶) |
2 | | eqid 2622 |
. . 3
⊢
(Arrow‘𝐶) =
(Arrow‘𝐶) |
3 | | coaval.x |
. . 3
⊢ ∙ =
(comp‘𝐶) |
4 | 1, 2, 3 | coafval 16714 |
. 2
⊢ · =
(𝑔 ∈
(Arrow‘𝐶), 𝑓 ∈ {ℎ ∈ (Arrow‘𝐶) ∣
(coda‘ℎ) = (doma‘𝑔)} ↦
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉 ∙
(coda‘𝑔))(2nd ‘𝑓))〉) |
5 | | homdmcoa.h |
. . . . 5
⊢ 𝐻 =
(Homa‘𝐶) |
6 | 2, 5 | homarw 16696 |
. . . 4
⊢ (𝑌𝐻𝑍) ⊆ (Arrow‘𝐶) |
7 | | homdmcoa.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) |
8 | 6, 7 | sseldi 3601 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (Arrow‘𝐶)) |
9 | 2, 5 | homarw 16696 |
. . . . 5
⊢ (𝑋𝐻𝑌) ⊆ (Arrow‘𝐶) |
10 | | homdmcoa.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) |
11 | 10 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝐹 ∈ (𝑋𝐻𝑌)) |
12 | 9, 11 | sseldi 3601 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝐹 ∈ (Arrow‘𝐶)) |
13 | 5 | homacd 16691 |
. . . . . 6
⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (coda‘𝐹) = 𝑌) |
14 | 11, 13 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (coda‘𝐹) = 𝑌) |
15 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
16 | 15 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (doma‘𝑔) =
(doma‘𝐺)) |
17 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝐺 ∈ (𝑌𝐻𝑍)) |
18 | 5 | homadm 16690 |
. . . . . . 7
⊢ (𝐺 ∈ (𝑌𝐻𝑍) → (doma‘𝐺) = 𝑌) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (doma‘𝐺) = 𝑌) |
20 | 16, 19 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (doma‘𝑔) = 𝑌) |
21 | 14, 20 | eqtr4d 2659 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (coda‘𝐹) =
(doma‘𝑔)) |
22 | | fveq2 6191 |
. . . . . 6
⊢ (ℎ = 𝐹 → (coda‘ℎ) =
(coda‘𝐹)) |
23 | 22 | eqeq1d 2624 |
. . . . 5
⊢ (ℎ = 𝐹 → ((coda‘ℎ) =
(doma‘𝑔) ↔ (coda‘𝐹) =
(doma‘𝑔))) |
24 | 23 | elrab 3363 |
. . . 4
⊢ (𝐹 ∈ {ℎ ∈ (Arrow‘𝐶) ∣
(coda‘ℎ) = (doma‘𝑔)} ↔ (𝐹 ∈ (Arrow‘𝐶) ∧ (coda‘𝐹) =
(doma‘𝑔))) |
25 | 12, 21, 24 | sylanbrc 698 |
. . 3
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝐹 ∈ {ℎ ∈ (Arrow‘𝐶) ∣
(coda‘ℎ) = (doma‘𝑔)}) |
26 | | otex 4933 |
. . . 4
⊢
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉 ∙
(coda‘𝑔))(2nd ‘𝑓))〉 ∈ V |
27 | 26 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉 ∙
(coda‘𝑔))(2nd ‘𝑓))〉 ∈ V) |
28 | | simprr 796 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → 𝑓 = 𝐹) |
29 | 28 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
(doma‘𝑓) = (doma‘𝐹)) |
30 | 5 | homadm 16690 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (doma‘𝐹) = 𝑋) |
31 | 11, 30 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (doma‘𝐹) = 𝑋) |
32 | 31 | adantrr 753 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
(doma‘𝐹) = 𝑋) |
33 | 29, 32 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
(doma‘𝑓) = 𝑋) |
34 | 15 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (coda‘𝑔) =
(coda‘𝐺)) |
35 | 5 | homacd 16691 |
. . . . . . 7
⊢ (𝐺 ∈ (𝑌𝐻𝑍) → (coda‘𝐺) = 𝑍) |
36 | 17, 35 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (coda‘𝐺) = 𝑍) |
37 | 34, 36 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (coda‘𝑔) = 𝑍) |
38 | 37 | adantrr 753 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
(coda‘𝑔) = 𝑍) |
39 | 20 | adantrr 753 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
(doma‘𝑔) = 𝑌) |
40 | 33, 39 | opeq12d 4410 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
〈(doma‘𝑓), (doma‘𝑔)〉 = 〈𝑋, 𝑌〉) |
41 | 40, 38 | oveq12d 6668 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
(〈(doma‘𝑓), (doma‘𝑔)〉 ∙
(coda‘𝑔)) = (〈𝑋, 𝑌〉 ∙ 𝑍)) |
42 | | simprl 794 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → 𝑔 = 𝐺) |
43 | 42 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2nd ‘𝑔) = (2nd ‘𝐺)) |
44 | 28 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2nd ‘𝑓) = (2nd ‘𝐹)) |
45 | 41, 43, 44 | oveq123d 6671 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉 ∙
(coda‘𝑔))(2nd ‘𝑓)) = ((2nd ‘𝐺)(〈𝑋, 𝑌〉 ∙ 𝑍)(2nd ‘𝐹))) |
46 | 33, 38, 45 | oteq123d 4417 |
. . 3
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉 ∙
(coda‘𝑔))(2nd ‘𝑓))〉 = 〈𝑋, 𝑍, ((2nd ‘𝐺)(〈𝑋, 𝑌〉 ∙ 𝑍)(2nd ‘𝐹))〉) |
47 | 8, 25, 27, 46 | ovmpt2dv2 6794 |
. 2
⊢ (𝜑 → ( · = (𝑔 ∈ (Arrow‘𝐶), 𝑓 ∈ {ℎ ∈ (Arrow‘𝐶) ∣
(coda‘ℎ) = (doma‘𝑔)} ↦
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉 ∙
(coda‘𝑔))(2nd ‘𝑓))〉) → (𝐺 · 𝐹) = 〈𝑋, 𝑍, ((2nd ‘𝐺)(〈𝑋, 𝑌〉 ∙ 𝑍)(2nd ‘𝐹))〉)) |
48 | 4, 47 | mpi 20 |
1
⊢ (𝜑 → (𝐺 · 𝐹) = 〈𝑋, 𝑍, ((2nd ‘𝐺)(〈𝑋, 𝑌〉 ∙ 𝑍)(2nd ‘𝐹))〉) |