Step | Hyp | Ref
| Expression |
1 | | tgpgrp 23573 |
. . 3
β’ (πΊ β TopGrp β πΊ β Grp) |
2 | | tgptps 23575 |
. . 3
β’ (πΊ β TopGrp β πΊ β TopSp) |
3 | | tgpsubcn.2 |
. . . 4
β’ π½ = (TopOpenβπΊ) |
4 | | tgpsubcn.3 |
. . . 4
β’ β =
(-gβπΊ) |
5 | 3, 4 | tgpsubcn 23585 |
. . 3
β’ (πΊ β TopGrp β β β
((π½ Γt
π½) Cn π½)) |
6 | 1, 2, 5 | 3jca 1128 |
. 2
β’ (πΊ β TopGrp β (πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½))) |
7 | | simp1 1136 |
. . 3
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β πΊ β Grp) |
8 | | grpmnd 18822 |
. . . . 5
β’ (πΊ β Grp β πΊ β Mnd) |
9 | 8 | 3ad2ant1 1133 |
. . . 4
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β πΊ β Mnd) |
10 | | simp2 1137 |
. . . 4
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β πΊ β TopSp) |
11 | | eqid 2732 |
. . . . . . . 8
β’
(BaseβπΊ) =
(BaseβπΊ) |
12 | | eqid 2732 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
13 | | eqid 2732 |
. . . . . . . 8
β’
(invgβπΊ) = (invgβπΊ) |
14 | 7 | 3ad2ant1 1133 |
. . . . . . . 8
β’ (((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β§ π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β πΊ β Grp) |
15 | | simp2 1137 |
. . . . . . . 8
β’ (((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β§ π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β π₯ β (BaseβπΊ)) |
16 | | simp3 1138 |
. . . . . . . 8
β’ (((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β§ π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β π¦ β (BaseβπΊ)) |
17 | 11, 12, 4, 13, 14, 15, 16 | grpsubinv 18892 |
. . . . . . 7
β’ (((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β§ π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β (π₯ β
((invgβπΊ)βπ¦)) = (π₯(+gβπΊ)π¦)) |
18 | 17 | mpoeq3dva 7482 |
. . . . . 6
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (π₯ β (BaseβπΊ), π¦ β (BaseβπΊ) β¦ (π₯ β
((invgβπΊ)βπ¦))) = (π₯ β (BaseβπΊ), π¦ β (BaseβπΊ) β¦ (π₯(+gβπΊ)π¦))) |
19 | | eqid 2732 |
. . . . . . 7
β’
(+πβπΊ) = (+πβπΊ) |
20 | 11, 12, 19 | plusffval 18563 |
. . . . . 6
β’
(+πβπΊ) = (π₯ β (BaseβπΊ), π¦ β (BaseβπΊ) β¦ (π₯(+gβπΊ)π¦)) |
21 | 18, 20 | eqtr4di 2790 |
. . . . 5
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (π₯ β (BaseβπΊ), π¦ β (BaseβπΊ) β¦ (π₯ β
((invgβπΊ)βπ¦))) = (+πβπΊ)) |
22 | 11, 3 | istps 22427 |
. . . . . . 7
β’ (πΊ β TopSp β π½ β
(TopOnβ(BaseβπΊ))) |
23 | 10, 22 | sylib 217 |
. . . . . 6
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β π½ β (TopOnβ(BaseβπΊ))) |
24 | 23, 23 | cnmpt1st 23163 |
. . . . . 6
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (π₯ β (BaseβπΊ), π¦ β (BaseβπΊ) β¦ π₯) β ((π½ Γt π½) Cn π½)) |
25 | 23, 23 | cnmpt2nd 23164 |
. . . . . . 7
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (π₯ β (BaseβπΊ), π¦ β (BaseβπΊ) β¦ π¦) β ((π½ Γt π½) Cn π½)) |
26 | 11, 13 | grpinvf 18867 |
. . . . . . . . . . 11
β’ (πΊ β Grp β
(invgβπΊ):(BaseβπΊ)βΆ(BaseβπΊ)) |
27 | 26 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (invgβπΊ):(BaseβπΊ)βΆ(BaseβπΊ)) |
28 | 27 | feqmptd 6957 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (invgβπΊ) = (π₯ β (BaseβπΊ) β¦ ((invgβπΊ)βπ₯))) |
29 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(0gβπΊ) = (0gβπΊ) |
30 | 11, 4, 13, 29 | grpinvval2 18902 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ π₯ β (BaseβπΊ)) β
((invgβπΊ)βπ₯) = ((0gβπΊ) β π₯)) |
31 | 7, 30 | sylan 580 |
. . . . . . . . . 10
β’ (((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β§ π₯ β (BaseβπΊ)) β ((invgβπΊ)βπ₯) = ((0gβπΊ) β π₯)) |
32 | 31 | mpteq2dva 5247 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (π₯ β (BaseβπΊ) β¦ ((invgβπΊ)βπ₯)) = (π₯ β (BaseβπΊ) β¦ ((0gβπΊ) β π₯))) |
33 | 28, 32 | eqtrd 2772 |
. . . . . . . 8
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (invgβπΊ) = (π₯ β (BaseβπΊ) β¦ ((0gβπΊ) β π₯))) |
34 | 11, 29 | grpidcl 18846 |
. . . . . . . . . . 11
β’ (πΊ β Grp β
(0gβπΊ)
β (BaseβπΊ)) |
35 | 34 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (0gβπΊ) β (BaseβπΊ)) |
36 | 23, 23, 35 | cnmptc 23157 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (π₯ β (BaseβπΊ) β¦ (0gβπΊ)) β (π½ Cn π½)) |
37 | 23 | cnmptid 23156 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (π₯ β (BaseβπΊ) β¦ π₯) β (π½ Cn π½)) |
38 | | simp3 1138 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β β β ((π½ Γt π½) Cn π½)) |
39 | 23, 36, 37, 38 | cnmpt12f 23161 |
. . . . . . . 8
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (π₯ β (BaseβπΊ) β¦ ((0gβπΊ) β π₯)) β (π½ Cn π½)) |
40 | 33, 39 | eqeltrd 2833 |
. . . . . . 7
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (invgβπΊ) β (π½ Cn π½)) |
41 | 23, 23, 25, 40 | cnmpt21f 23167 |
. . . . . 6
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (π₯ β (BaseβπΊ), π¦ β (BaseβπΊ) β¦ ((invgβπΊ)βπ¦)) β ((π½ Γt π½) Cn π½)) |
42 | 23, 23, 24, 41, 38 | cnmpt22f 23170 |
. . . . 5
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (π₯ β (BaseβπΊ), π¦ β (BaseβπΊ) β¦ (π₯ β
((invgβπΊ)βπ¦))) β ((π½ Γt π½) Cn π½)) |
43 | 21, 42 | eqeltrrd 2834 |
. . . 4
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β (+πβπΊ) β ((π½ Γt π½) Cn π½)) |
44 | 19, 3 | istmd 23569 |
. . . 4
β’ (πΊ β TopMnd β (πΊ β Mnd β§ πΊ β TopSp β§
(+πβπΊ) β ((π½ Γt π½) Cn π½))) |
45 | 9, 10, 43, 44 | syl3anbrc 1343 |
. . 3
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β πΊ β TopMnd) |
46 | 3, 13 | istgp 23572 |
. . 3
β’ (πΊ β TopGrp β (πΊ β Grp β§ πΊ β TopMnd β§
(invgβπΊ)
β (π½ Cn π½))) |
47 | 7, 45, 40, 46 | syl3anbrc 1343 |
. 2
β’ ((πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½)) β πΊ β TopGrp) |
48 | 6, 47 | impbii 208 |
1
β’ (πΊ β TopGrp β (πΊ β Grp β§ πΊ β TopSp β§ β β
((π½ Γt
π½) Cn π½))) |