Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(BaseβπΆ) =
(BaseβπΆ) |
2 | | eqid 2733 |
. . . . 5
β’ (Hom
βπΆ) = (Hom
βπΆ) |
3 | | eqid 2733 |
. . . . 5
β’
(compβπΆ) =
(compβπΆ) |
4 | | eqid 2733 |
. . . . 5
β’
(EpiβπΆ) =
(EpiβπΆ) |
5 | | grptcmon.c |
. . . . . 6
β’ (π β πΆ = (MndToCatβπΊ)) |
6 | | grptcmon.g |
. . . . . . 7
β’ (π β πΊ β Grp) |
7 | 6 | grpmndd 18765 |
. . . . . 6
β’ (π β πΊ β Mnd) |
8 | 5, 7 | mndtccat 47200 |
. . . . 5
β’ (π β πΆ β Cat) |
9 | | grptcmon.x |
. . . . . 6
β’ (π β π β π΅) |
10 | | grptcmon.b |
. . . . . 6
β’ (π β π΅ = (BaseβπΆ)) |
11 | 9, 10 | eleqtrd 2836 |
. . . . 5
β’ (π β π β (BaseβπΆ)) |
12 | | grptcmon.y |
. . . . . 6
β’ (π β π β π΅) |
13 | 12, 10 | eleqtrd 2836 |
. . . . 5
β’ (π β π β (BaseβπΆ)) |
14 | 1, 2, 3, 4, 8, 11,
13 | isepi2 17629 |
. . . 4
β’ (π β (π β (π(EpiβπΆ)π) β (π β (π(Hom βπΆ)π) β§ βπ§ β (BaseβπΆ)βπ β (π(Hom βπΆ)π§)ββ β (π(Hom βπΆ)π§)((π(β¨π, πβ©(compβπΆ)π§)π) = (β(β¨π, πβ©(compβπΆ)π§)π) β π = β)))) |
15 | 5 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β πΆ = (MndToCatβπΊ)) |
16 | 7 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β πΊ β Mnd) |
17 | 10 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β π΅ = (BaseβπΆ)) |
18 | 9 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β π β π΅) |
19 | 12 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β π β π΅) |
20 | | simpr1 1195 |
. . . . . . . . . 10
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β π§ β (BaseβπΆ)) |
21 | 20, 17 | eleqtrrd 2837 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β π§ β π΅) |
22 | | eqidd 2734 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β (compβπΆ) = (compβπΆ)) |
23 | | eqidd 2734 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β (β¨π, πβ©(compβπΆ)π§) = (β¨π, πβ©(compβπΆ)π§)) |
24 | 15, 16, 17, 18, 19, 21, 22, 23 | mndtcco2 47198 |
. . . . . . . 8
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β (π(β¨π, πβ©(compβπΆ)π§)π) = (π(+gβπΊ)π)) |
25 | 15, 16, 17, 18, 19, 21, 22, 23 | mndtcco2 47198 |
. . . . . . . 8
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β (β(β¨π, πβ©(compβπΆ)π§)π) = (β(+gβπΊ)π)) |
26 | 24, 25 | eqeq12d 2749 |
. . . . . . 7
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β ((π(β¨π, πβ©(compβπΆ)π§)π) = (β(β¨π, πβ©(compβπΆ)π§)π) β (π(+gβπΊ)π) = (β(+gβπΊ)π))) |
27 | 6 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β πΊ β Grp) |
28 | | simpr2 1196 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β π β (π(Hom βπΆ)π§)) |
29 | | eqidd 2734 |
. . . . . . . . . 10
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β (Hom βπΆ) = (Hom βπΆ)) |
30 | 15, 16, 17, 19, 21, 29 | mndtchom 47196 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β (π(Hom βπΆ)π§) = (BaseβπΊ)) |
31 | 28, 30 | eleqtrd 2836 |
. . . . . . . 8
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β π β (BaseβπΊ)) |
32 | | simpr3 1197 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β β β (π(Hom βπΆ)π§)) |
33 | 32, 30 | eleqtrd 2836 |
. . . . . . . 8
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β β β (BaseβπΊ)) |
34 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β π β (π(Hom βπΆ)π)) |
35 | 15, 16, 17, 18, 19, 29 | mndtchom 47196 |
. . . . . . . . 9
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β (π(Hom βπΆ)π) = (BaseβπΊ)) |
36 | 34, 35 | eleqtrd 2836 |
. . . . . . . 8
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β π β (BaseβπΊ)) |
37 | | eqid 2733 |
. . . . . . . . 9
β’
(BaseβπΊ) =
(BaseβπΊ) |
38 | | eqid 2733 |
. . . . . . . . 9
β’
(+gβπΊ) = (+gβπΊ) |
39 | 37, 38 | grprcan 18789 |
. . . . . . . 8
β’ ((πΊ β Grp β§ (π β (BaseβπΊ) β§ β β (BaseβπΊ) β§ π β (BaseβπΊ))) β ((π(+gβπΊ)π) = (β(+gβπΊ)π) β π = β)) |
40 | 27, 31, 33, 36, 39 | syl13anc 1373 |
. . . . . . 7
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β ((π(+gβπΊ)π) = (β(+gβπΊ)π) β π = β)) |
41 | 26, 40 | bitrd 279 |
. . . . . 6
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β ((π(β¨π, πβ©(compβπΆ)π§)π) = (β(β¨π, πβ©(compβπΆ)π§)π) β π = β)) |
42 | 41 | biimpd 228 |
. . . . 5
β’ (((π β§ π β (π(Hom βπΆ)π)) β§ (π§ β (BaseβπΆ) β§ π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β ((π(β¨π, πβ©(compβπΆ)π§)π) = (β(β¨π, πβ©(compβπΆ)π§)π) β π = β)) |
43 | 42 | ralrimivvva 3197 |
. . . 4
β’ ((π β§ π β (π(Hom βπΆ)π)) β βπ§ β (BaseβπΆ)βπ β (π(Hom βπΆ)π§)ββ β (π(Hom βπΆ)π§)((π(β¨π, πβ©(compβπΆ)π§)π) = (β(β¨π, πβ©(compβπΆ)π§)π) β π = β)) |
44 | 14, 43 | mpbiran3d 46968 |
. . 3
β’ (π β (π β (π(EpiβπΆ)π) β π β (π(Hom βπΆ)π))) |
45 | 44 | eqrdv 2731 |
. 2
β’ (π β (π(EpiβπΆ)π) = (π(Hom βπΆ)π)) |
46 | | grptcepi.e |
. . 3
β’ (π β πΈ = (EpiβπΆ)) |
47 | 46 | oveqd 7375 |
. 2
β’ (π β (ππΈπ) = (π(EpiβπΆ)π)) |
48 | | grptcmon.h |
. . 3
β’ (π β π» = (Hom βπΆ)) |
49 | 48 | oveqd 7375 |
. 2
β’ (π β (ππ»π) = (π(Hom βπΆ)π)) |
50 | 45, 47, 49 | 3eqtr4d 2783 |
1
β’ (π β (ππΈπ) = (ππ»π)) |