Proof of Theorem rcaninv
| Step | Hyp | Ref
| Expression |
| 1 | | rcaninv.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
| 2 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 3 | | eqid 2737 |
. . . . . 6
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 4 | | rcaninv.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 5 | | rcaninv.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 6 | | rcaninv.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 7 | | eqid 2737 |
. . . . . . . 8
⊢
(Iso‘𝐶) =
(Iso‘𝐶) |
| 8 | 1, 2, 7, 4, 5, 6 | isohom 17820 |
. . . . . . 7
⊢ (𝜑 → (𝑌(Iso‘𝐶)𝑋) ⊆ (𝑌(Hom ‘𝐶)𝑋)) |
| 9 | | rcaninv.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝑌(Iso‘𝐶)𝑋)) |
| 10 | 8, 9 | sseldd 3984 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋)) |
| 11 | 1, 2, 7, 4, 6, 5 | isohom 17820 |
. . . . . . 7
⊢ (𝜑 → (𝑋(Iso‘𝐶)𝑌) ⊆ (𝑋(Hom ‘𝐶)𝑌)) |
| 12 | | rcaninv.n |
. . . . . . . . 9
⊢ 𝑁 = (Inv‘𝐶) |
| 13 | 1, 12, 4, 5, 6, 7 | invf 17812 |
. . . . . . . 8
⊢ (𝜑 → (𝑌𝑁𝑋):(𝑌(Iso‘𝐶)𝑋)⟶(𝑋(Iso‘𝐶)𝑌)) |
| 14 | 13, 9 | ffvelcdmd 7105 |
. . . . . . 7
⊢ (𝜑 → ((𝑌𝑁𝑋)‘𝐹) ∈ (𝑋(Iso‘𝐶)𝑌)) |
| 15 | 11, 14 | sseldd 3984 |
. . . . . 6
⊢ (𝜑 → ((𝑌𝑁𝑋)‘𝐹) ∈ (𝑋(Hom ‘𝐶)𝑌)) |
| 16 | | rcaninv.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
| 17 | | rcaninv.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑍)) |
| 18 | 1, 2, 3, 4, 5, 6, 5, 10, 15, 16, 17 | catass 17729 |
. . . . 5
⊢ (𝜑 → ((𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑍)((𝑌𝑁𝑋)‘𝐹))(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹) = (𝐺(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)(((𝑌𝑁𝑋)‘𝐹)(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐹))) |
| 19 | | eqid 2737 |
. . . . . . . 8
⊢
(Id‘𝐶) =
(Id‘𝐶) |
| 20 | | eqid 2737 |
. . . . . . . 8
⊢
(〈𝑌, 𝑋〉(comp‘𝐶)𝑌) = (〈𝑌, 𝑋〉(comp‘𝐶)𝑌) |
| 21 | 1, 7, 12, 4, 5, 6,
9, 19, 20 | invcoisoid 17836 |
. . . . . . 7
⊢ (𝜑 → (((𝑌𝑁𝑋)‘𝐹)(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐹) = ((Id‘𝐶)‘𝑌)) |
| 22 | 21 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → ((Id‘𝐶)‘𝑌) = (((𝑌𝑁𝑋)‘𝐹)(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐹)) |
| 23 | 22 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (𝐺(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)((Id‘𝐶)‘𝑌)) = (𝐺(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)(((𝑌𝑁𝑋)‘𝐹)(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐹))) |
| 24 | 1, 2, 19, 4, 5, 3,
16, 17 | catrid 17727 |
. . . . 5
⊢ (𝜑 → (𝐺(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)((Id‘𝐶)‘𝑌)) = 𝐺) |
| 25 | 18, 23, 24 | 3eqtr2rd 2784 |
. . . 4
⊢ (𝜑 → 𝐺 = ((𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑍)((𝑌𝑁𝑋)‘𝐹))(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹)) |
| 26 | 25 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) → 𝐺 = ((𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑍)((𝑌𝑁𝑋)‘𝐹))(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹)) |
| 27 | | rcaninv.o |
. . . . . . . . 9
⊢ ⚬ =
(〈𝑋, 𝑌〉(comp‘𝐶)𝑍) |
| 28 | 27 | eqcomi 2746 |
. . . . . . . 8
⊢
(〈𝑋, 𝑌〉(comp‘𝐶)𝑍) = ⚬ |
| 29 | 28 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (〈𝑋, 𝑌〉(comp‘𝐶)𝑍) = ⚬ ) |
| 30 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → 𝐺 = 𝐺) |
| 31 | | rcaninv.1 |
. . . . . . . . 9
⊢ 𝑅 = ((𝑌𝑁𝑋)‘𝐹) |
| 32 | 31 | eqcomi 2746 |
. . . . . . . 8
⊢ ((𝑌𝑁𝑋)‘𝐹) = 𝑅 |
| 33 | 32 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((𝑌𝑁𝑋)‘𝐹) = 𝑅) |
| 34 | 29, 30, 33 | oveq123d 7452 |
. . . . . 6
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑍)((𝑌𝑁𝑋)‘𝐹)) = (𝐺 ⚬ 𝑅)) |
| 35 | 34 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) → (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑍)((𝑌𝑁𝑋)‘𝐹)) = (𝐺 ⚬ 𝑅)) |
| 36 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) → (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) |
| 37 | 35, 36 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) → (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑍)((𝑌𝑁𝑋)‘𝐹)) = (𝐻 ⚬ 𝑅)) |
| 38 | 37 | oveq1d 7446 |
. . 3
⊢ ((𝜑 ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) → ((𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑍)((𝑌𝑁𝑋)‘𝐹))(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹) = ((𝐻 ⚬ 𝑅)(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹)) |
| 39 | 27 | oveqi 7444 |
. . . . . . 7
⊢ (𝐻 ⚬ 𝑅) = (𝐻(〈𝑋, 𝑌〉(comp‘𝐶)𝑍)𝑅) |
| 40 | 39 | oveq1i 7441 |
. . . . . 6
⊢ ((𝐻 ⚬ 𝑅)(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹) = ((𝐻(〈𝑋, 𝑌〉(comp‘𝐶)𝑍)𝑅)(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹) |
| 41 | 40 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝐻 ⚬ 𝑅)(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹) = ((𝐻(〈𝑋, 𝑌〉(comp‘𝐶)𝑍)𝑅)(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹)) |
| 42 | 31, 15 | eqeltrid 2845 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
| 43 | | rcaninv.h |
. . . . . . 7
⊢ (𝜑 → 𝐻 ∈ (𝑌(Hom ‘𝐶)𝑍)) |
| 44 | 1, 2, 3, 4, 5, 6, 5, 10, 42, 16, 43 | catass 17729 |
. . . . . 6
⊢ (𝜑 → ((𝐻(〈𝑋, 𝑌〉(comp‘𝐶)𝑍)𝑅)(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹) = (𝐻(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)(𝑅(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐹))) |
| 45 | 31 | oveq1i 7441 |
. . . . . . . 8
⊢ (𝑅(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐹) = (((𝑌𝑁𝑋)‘𝐹)(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐹) |
| 46 | 45 | oveq2i 7442 |
. . . . . . 7
⊢ (𝐻(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)(𝑅(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐹)) = (𝐻(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)(((𝑌𝑁𝑋)‘𝐹)(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐹)) |
| 47 | 46 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐻(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)(𝑅(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐹)) = (𝐻(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)(((𝑌𝑁𝑋)‘𝐹)(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐹))) |
| 48 | 21 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (𝐻(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)(((𝑌𝑁𝑋)‘𝐹)(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐹)) = (𝐻(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)((Id‘𝐶)‘𝑌))) |
| 49 | 44, 47, 48 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → ((𝐻(〈𝑋, 𝑌〉(comp‘𝐶)𝑍)𝑅)(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹) = (𝐻(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)((Id‘𝐶)‘𝑌))) |
| 50 | 1, 2, 19, 4, 5, 3,
16, 43 | catrid 17727 |
. . . . 5
⊢ (𝜑 → (𝐻(〈𝑌, 𝑌〉(comp‘𝐶)𝑍)((Id‘𝐶)‘𝑌)) = 𝐻) |
| 51 | 41, 49, 50 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → ((𝐻 ⚬ 𝑅)(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹) = 𝐻) |
| 52 | 51 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) → ((𝐻 ⚬ 𝑅)(〈𝑌, 𝑋〉(comp‘𝐶)𝑍)𝐹) = 𝐻) |
| 53 | 26, 38, 52 | 3eqtrd 2781 |
. 2
⊢ ((𝜑 ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) → 𝐺 = 𝐻) |
| 54 | 53 | ex 412 |
1
⊢ (𝜑 → ((𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅) → 𝐺 = 𝐻)) |