| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 2 | | eqid 2737 |
. . . . 5
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 3 | | eqid 2737 |
. . . . 5
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 4 | | eqid 2737 |
. . . . 5
⊢
(Mono‘𝐶) =
(Mono‘𝐶) |
| 5 | | grptcmon.c |
. . . . . 6
⊢ (𝜑 → 𝐶 = (MndToCat‘𝐺)) |
| 6 | | grptcmon.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 7 | 6 | grpmndd 18964 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Mnd) |
| 8 | 5, 7 | mndtccat 49185 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 9 | | grptcmon.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 10 | | grptcmon.b |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
| 11 | 9, 10 | eleqtrd 2843 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) |
| 12 | | grptcmon.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 13 | 12, 10 | eleqtrd 2843 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) |
| 14 | 1, 2, 3, 4, 8, 11,
13 | ismon2 17778 |
. . . 4
⊢ (𝜑 → (𝑓 ∈ (𝑋(Mono‘𝐶)𝑌) ↔ (𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)((𝑓(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝑓(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)))) |
| 15 | 5 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → 𝐶 = (MndToCat‘𝐺)) |
| 16 | 7 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → 𝐺 ∈ Mnd) |
| 17 | 10 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → 𝐵 = (Base‘𝐶)) |
| 18 | | simpr1 1195 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → 𝑧 ∈ (Base‘𝐶)) |
| 19 | 18, 17 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → 𝑧 ∈ 𝐵) |
| 20 | 9 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → 𝑋 ∈ 𝐵) |
| 21 | 12 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → 𝑌 ∈ 𝐵) |
| 22 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → (comp‘𝐶) = (comp‘𝐶)) |
| 23 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → (〈𝑧, 𝑋〉(comp‘𝐶)𝑌) = (〈𝑧, 𝑋〉(comp‘𝐶)𝑌)) |
| 24 | 15, 16, 17, 19, 20, 21, 22, 23 | mndtcco2 49183 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → (𝑓(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝑓(+g‘𝐺)𝑔)) |
| 25 | 15, 16, 17, 19, 20, 21, 22, 23 | mndtcco2 49183 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → (𝑓(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) = (𝑓(+g‘𝐺)ℎ)) |
| 26 | 24, 25 | eqeq12d 2753 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → ((𝑓(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝑓(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) ↔ (𝑓(+g‘𝐺)𝑔) = (𝑓(+g‘𝐺)ℎ))) |
| 27 | 6 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → 𝐺 ∈ Grp) |
| 28 | | simpr2 1196 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) |
| 29 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → (Hom ‘𝐶) = (Hom ‘𝐶)) |
| 30 | 15, 16, 17, 19, 20, 29 | mndtchom 49181 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → (𝑧(Hom ‘𝐶)𝑋) = (Base‘𝐺)) |
| 31 | 28, 30 | eleqtrd 2843 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → 𝑔 ∈ (Base‘𝐺)) |
| 32 | | simpr3 1197 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)) |
| 33 | 32, 30 | eleqtrd 2843 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → ℎ ∈ (Base‘𝐺)) |
| 34 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
| 35 | 15, 16, 17, 20, 21, 29 | mndtchom 49181 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → (𝑋(Hom ‘𝐶)𝑌) = (Base‘𝐺)) |
| 36 | 34, 35 | eleqtrd 2843 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → 𝑓 ∈ (Base‘𝐺)) |
| 37 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 38 | | eqid 2737 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 39 | 37, 38 | grplcan 19018 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑔 ∈ (Base‘𝐺) ∧ ℎ ∈ (Base‘𝐺) ∧ 𝑓 ∈ (Base‘𝐺))) → ((𝑓(+g‘𝐺)𝑔) = (𝑓(+g‘𝐺)ℎ) ↔ 𝑔 = ℎ)) |
| 40 | 27, 31, 33, 36, 39 | syl13anc 1374 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → ((𝑓(+g‘𝐺)𝑔) = (𝑓(+g‘𝐺)ℎ) ↔ 𝑔 = ℎ)) |
| 41 | 26, 40 | bitrd 279 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → ((𝑓(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝑓(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) ↔ 𝑔 = ℎ)) |
| 42 | 41 | biimpd 229 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → ((𝑓(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝑓(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)) |
| 43 | 42 | ralrimivvva 3205 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌)) → ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)((𝑓(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝑓(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)) |
| 44 | 14, 43 | mpbiran3d 48717 |
. . 3
⊢ (𝜑 → (𝑓 ∈ (𝑋(Mono‘𝐶)𝑌) ↔ 𝑓 ∈ (𝑋(Hom ‘𝐶)𝑌))) |
| 45 | 44 | eqrdv 2735 |
. 2
⊢ (𝜑 → (𝑋(Mono‘𝐶)𝑌) = (𝑋(Hom ‘𝐶)𝑌)) |
| 46 | | grptcmon.m |
. . 3
⊢ (𝜑 → 𝑀 = (Mono‘𝐶)) |
| 47 | 46 | oveqd 7448 |
. 2
⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑋(Mono‘𝐶)𝑌)) |
| 48 | | grptcmon.h |
. . 3
⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) |
| 49 | 48 | oveqd 7448 |
. 2
⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋(Hom ‘𝐶)𝑌)) |
| 50 | 45, 47, 49 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑋𝐻𝑌)) |