| Step | Hyp | Ref
| Expression |
| 1 | | homdmcoa.o |
. . 3
⊢ · =
(compa‘𝐶) |
| 2 | | eqid 2737 |
. . 3
⊢
(Arrow‘𝐶) =
(Arrow‘𝐶) |
| 3 | | coaval.x |
. . 3
⊢ ∙ =
(comp‘𝐶) |
| 4 | 1, 2, 3 | coafval 18109 |
. 2
⊢ · =
(𝑔 ∈
(Arrow‘𝐶), 𝑓 ∈ {ℎ ∈ (Arrow‘𝐶) ∣
(coda‘ℎ) = (doma‘𝑔)} ↦
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉 ∙
(coda‘𝑔))(2nd ‘𝑓))〉) |
| 5 | | homdmcoa.h |
. . . . 5
⊢ 𝐻 =
(Homa‘𝐶) |
| 6 | 2, 5 | homarw 18091 |
. . . 4
⊢ (𝑌𝐻𝑍) ⊆ (Arrow‘𝐶) |
| 7 | | homdmcoa.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) |
| 8 | 6, 7 | sselid 3981 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (Arrow‘𝐶)) |
| 9 | | fveqeq2 6915 |
. . . 4
⊢ (ℎ = 𝐹 → ((coda‘ℎ) =
(doma‘𝑔) ↔ (coda‘𝐹) =
(doma‘𝑔))) |
| 10 | 2, 5 | homarw 18091 |
. . . . 5
⊢ (𝑋𝐻𝑌) ⊆ (Arrow‘𝐶) |
| 11 | | homdmcoa.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) |
| 12 | 11 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝐹 ∈ (𝑋𝐻𝑌)) |
| 13 | 10, 12 | sselid 3981 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝐹 ∈ (Arrow‘𝐶)) |
| 14 | 5 | homacd 18086 |
. . . . . 6
⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (coda‘𝐹) = 𝑌) |
| 15 | 12, 14 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (coda‘𝐹) = 𝑌) |
| 16 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
| 17 | 16 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (doma‘𝑔) =
(doma‘𝐺)) |
| 18 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝐺 ∈ (𝑌𝐻𝑍)) |
| 19 | 5 | homadm 18085 |
. . . . . . 7
⊢ (𝐺 ∈ (𝑌𝐻𝑍) → (doma‘𝐺) = 𝑌) |
| 20 | 18, 19 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (doma‘𝐺) = 𝑌) |
| 21 | 17, 20 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (doma‘𝑔) = 𝑌) |
| 22 | 15, 21 | eqtr4d 2780 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (coda‘𝐹) =
(doma‘𝑔)) |
| 23 | 9, 13, 22 | elrabd 3694 |
. . 3
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝐹 ∈ {ℎ ∈ (Arrow‘𝐶) ∣
(coda‘ℎ) = (doma‘𝑔)}) |
| 24 | | otex 5470 |
. . . 4
⊢
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉 ∙
(coda‘𝑔))(2nd ‘𝑓))〉 ∈ V |
| 25 | 24 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉 ∙
(coda‘𝑔))(2nd ‘𝑓))〉 ∈ V) |
| 26 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → 𝑓 = 𝐹) |
| 27 | 26 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
(doma‘𝑓) = (doma‘𝐹)) |
| 28 | 5 | homadm 18085 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (doma‘𝐹) = 𝑋) |
| 29 | 12, 28 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (doma‘𝐹) = 𝑋) |
| 30 | 29 | adantrr 717 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
(doma‘𝐹) = 𝑋) |
| 31 | 27, 30 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
(doma‘𝑓) = 𝑋) |
| 32 | 16 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (coda‘𝑔) =
(coda‘𝐺)) |
| 33 | 5 | homacd 18086 |
. . . . . . 7
⊢ (𝐺 ∈ (𝑌𝐻𝑍) → (coda‘𝐺) = 𝑍) |
| 34 | 18, 33 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (coda‘𝐺) = 𝑍) |
| 35 | 32, 34 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (coda‘𝑔) = 𝑍) |
| 36 | 35 | adantrr 717 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
(coda‘𝑔) = 𝑍) |
| 37 | 21 | adantrr 717 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
(doma‘𝑔) = 𝑌) |
| 38 | 31, 37 | opeq12d 4881 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
〈(doma‘𝑓), (doma‘𝑔)〉 = 〈𝑋, 𝑌〉) |
| 39 | 38, 36 | oveq12d 7449 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
(〈(doma‘𝑓), (doma‘𝑔)〉 ∙
(coda‘𝑔)) = (〈𝑋, 𝑌〉 ∙ 𝑍)) |
| 40 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → 𝑔 = 𝐺) |
| 41 | 40 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2nd ‘𝑔) = (2nd ‘𝐺)) |
| 42 | 26 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2nd ‘𝑓) = (2nd ‘𝐹)) |
| 43 | 39, 41, 42 | oveq123d 7452 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉 ∙
(coda‘𝑔))(2nd ‘𝑓)) = ((2nd ‘𝐺)(〈𝑋, 𝑌〉 ∙ 𝑍)(2nd ‘𝐹))) |
| 44 | 31, 36, 43 | oteq123d 4888 |
. . 3
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) →
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉 ∙
(coda‘𝑔))(2nd ‘𝑓))〉 = 〈𝑋, 𝑍, ((2nd ‘𝐺)(〈𝑋, 𝑌〉 ∙ 𝑍)(2nd ‘𝐹))〉) |
| 45 | 8, 23, 25, 44 | ovmpodv2 7591 |
. 2
⊢ (𝜑 → ( · = (𝑔 ∈ (Arrow‘𝐶), 𝑓 ∈ {ℎ ∈ (Arrow‘𝐶) ∣
(coda‘ℎ) = (doma‘𝑔)} ↦
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉 ∙
(coda‘𝑔))(2nd ‘𝑓))〉) → (𝐺 · 𝐹) = 〈𝑋, 𝑍, ((2nd ‘𝐺)(〈𝑋, 𝑌〉 ∙ 𝑍)(2nd ‘𝐹))〉)) |
| 46 | 4, 45 | mpi 20 |
1
⊢ (𝜑 → (𝐺 · 𝐹) = 〈𝑋, 𝑍, ((2nd ‘𝐺)(〈𝑋, 𝑌〉 ∙ 𝑍)(2nd ‘𝐹))〉) |