Step | Hyp | Ref
| Expression |
1 | | ngpgrp 24459 |
. . 3
โข (๐บ โ NrmGrp โ ๐บ โ Grp) |
2 | 1 | adantr 480 |
. 2
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ ๐บ โ Grp) |
3 | | ngpms 24460 |
. . . 4
โข (๐บ โ NrmGrp โ ๐บ โ MetSp) |
4 | 3 | adantr 480 |
. . 3
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ ๐บ โ MetSp) |
5 | | mstps 24312 |
. . 3
โข (๐บ โ MetSp โ ๐บ โ TopSp) |
6 | 4, 5 | syl 17 |
. 2
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ ๐บ โ TopSp) |
7 | | eqid 2726 |
. . . . . 6
โข
(Baseโ๐บ) =
(Baseโ๐บ) |
8 | | eqid 2726 |
. . . . . 6
โข
(-gโ๐บ) = (-gโ๐บ) |
9 | 7, 8 | grpsubf 18945 |
. . . . 5
โข (๐บ โ Grp โ
(-gโ๐บ):((Baseโ๐บ) ร (Baseโ๐บ))โถ(Baseโ๐บ)) |
10 | 2, 9 | syl 17 |
. . . 4
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ
(-gโ๐บ):((Baseโ๐บ) ร (Baseโ๐บ))โถ(Baseโ๐บ)) |
11 | | rphalfcl 13004 |
. . . . . . 7
โข (๐ง โ โ+
โ (๐ง / 2) โ
โ+) |
12 | | simplll 772 |
. . . . . . . . . . . . 13
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (๐บ โ NrmGrp โง ๐บ โ Abel)) |
13 | 12, 4 | syl 17 |
. . . . . . . . . . . 12
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ๐บ โ MetSp) |
14 | | simpllr 773 |
. . . . . . . . . . . . 13
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) |
15 | 14 | simpld 494 |
. . . . . . . . . . . 12
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ๐ฅ โ (Baseโ๐บ)) |
16 | | simprl 768 |
. . . . . . . . . . . 12
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ๐ข โ (Baseโ๐บ)) |
17 | | eqid 2726 |
. . . . . . . . . . . . 13
โข
(distโ๐บ) =
(distโ๐บ) |
18 | 7, 17 | mscl 24318 |
. . . . . . . . . . . 12
โข ((๐บ โ MetSp โง ๐ฅ โ (Baseโ๐บ) โง ๐ข โ (Baseโ๐บ)) โ (๐ฅ(distโ๐บ)๐ข) โ โ) |
19 | 13, 15, 16, 18 | syl3anc 1368 |
. . . . . . . . . . 11
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (๐ฅ(distโ๐บ)๐ข) โ โ) |
20 | 14 | simprd 495 |
. . . . . . . . . . . 12
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ๐ฆ โ (Baseโ๐บ)) |
21 | | simprr 770 |
. . . . . . . . . . . 12
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ๐ฃ โ (Baseโ๐บ)) |
22 | 7, 17 | mscl 24318 |
. . . . . . . . . . . 12
โข ((๐บ โ MetSp โง ๐ฆ โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ)) โ (๐ฆ(distโ๐บ)๐ฃ) โ โ) |
23 | 13, 20, 21, 22 | syl3anc 1368 |
. . . . . . . . . . 11
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (๐ฆ(distโ๐บ)๐ฃ) โ โ) |
24 | | rpre 12985 |
. . . . . . . . . . . 12
โข (๐ง โ โ+
โ ๐ง โ
โ) |
25 | 24 | ad2antlr 724 |
. . . . . . . . . . 11
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ๐ง โ โ) |
26 | | lt2halves 12448 |
. . . . . . . . . . 11
โข (((๐ฅ(distโ๐บ)๐ข) โ โ โง (๐ฆ(distโ๐บ)๐ฃ) โ โ โง ๐ง โ โ) โ (((๐ฅ(distโ๐บ)๐ข) < (๐ง / 2) โง (๐ฆ(distโ๐บ)๐ฃ) < (๐ง / 2)) โ ((๐ฅ(distโ๐บ)๐ข) + (๐ฆ(distโ๐บ)๐ฃ)) < ๐ง)) |
27 | 19, 23, 25, 26 | syl3anc 1368 |
. . . . . . . . . 10
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (((๐ฅ(distโ๐บ)๐ข) < (๐ง / 2) โง (๐ฆ(distโ๐บ)๐ฃ) < (๐ง / 2)) โ ((๐ฅ(distโ๐บ)๐ข) + (๐ฆ(distโ๐บ)๐ฃ)) < ๐ง)) |
28 | 12, 2 | syl 17 |
. . . . . . . . . . . . . 14
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ๐บ โ Grp) |
29 | 7, 8 | grpsubcl 18946 |
. . . . . . . . . . . . . 14
โข ((๐บ โ Grp โง ๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ)) โ (๐ฅ(-gโ๐บ)๐ฆ) โ (Baseโ๐บ)) |
30 | 28, 15, 20, 29 | syl3anc 1368 |
. . . . . . . . . . . . 13
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (๐ฅ(-gโ๐บ)๐ฆ) โ (Baseโ๐บ)) |
31 | 7, 8 | grpsubcl 18946 |
. . . . . . . . . . . . . 14
โข ((๐บ โ Grp โง ๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ)) โ (๐ข(-gโ๐บ)๐ฃ) โ (Baseโ๐บ)) |
32 | 28, 16, 21, 31 | syl3anc 1368 |
. . . . . . . . . . . . 13
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (๐ข(-gโ๐บ)๐ฃ) โ (Baseโ๐บ)) |
33 | 7, 8 | grpsubcl 18946 |
. . . . . . . . . . . . . 14
โข ((๐บ โ Grp โง ๐ข โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ)) โ (๐ข(-gโ๐บ)๐ฆ) โ (Baseโ๐บ)) |
34 | 28, 16, 20, 33 | syl3anc 1368 |
. . . . . . . . . . . . 13
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (๐ข(-gโ๐บ)๐ฆ) โ (Baseโ๐บ)) |
35 | 7, 17 | mstri 24326 |
. . . . . . . . . . . . 13
โข ((๐บ โ MetSp โง ((๐ฅ(-gโ๐บ)๐ฆ) โ (Baseโ๐บ) โง (๐ข(-gโ๐บ)๐ฃ) โ (Baseโ๐บ) โง (๐ข(-gโ๐บ)๐ฆ) โ (Baseโ๐บ))) โ ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) โค (((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฆ)) + ((๐ข(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)))) |
36 | 13, 30, 32, 34, 35 | syl13anc 1369 |
. . . . . . . . . . . 12
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) โค (((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฆ)) + ((๐ข(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)))) |
37 | 12 | simpld 494 |
. . . . . . . . . . . . . 14
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ๐บ โ NrmGrp) |
38 | 7, 8, 17 | ngpsubcan 24474 |
. . . . . . . . . . . . . 14
โข ((๐บ โ NrmGrp โง (๐ฅ โ (Baseโ๐บ) โง ๐ข โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โ ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฆ)) = (๐ฅ(distโ๐บ)๐ข)) |
39 | 37, 15, 16, 20, 38 | syl13anc 1369 |
. . . . . . . . . . . . 13
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฆ)) = (๐ฅ(distโ๐บ)๐ข)) |
40 | | eqid 2726 |
. . . . . . . . . . . . . . . . 17
โข
(+gโ๐บ) = (+gโ๐บ) |
41 | | eqid 2726 |
. . . . . . . . . . . . . . . . 17
โข
(invgโ๐บ) = (invgโ๐บ) |
42 | 7, 40, 41, 8 | grpsubval 18913 |
. . . . . . . . . . . . . . . 16
โข ((๐ข โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ)) โ (๐ข(-gโ๐บ)๐ฆ) = (๐ข(+gโ๐บ)((invgโ๐บ)โ๐ฆ))) |
43 | 16, 20, 42 | syl2anc 583 |
. . . . . . . . . . . . . . 15
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (๐ข(-gโ๐บ)๐ฆ) = (๐ข(+gโ๐บ)((invgโ๐บ)โ๐ฆ))) |
44 | 7, 40, 41, 8 | grpsubval 18913 |
. . . . . . . . . . . . . . . 16
โข ((๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ)) โ (๐ข(-gโ๐บ)๐ฃ) = (๐ข(+gโ๐บ)((invgโ๐บ)โ๐ฃ))) |
45 | 44 | adantl 481 |
. . . . . . . . . . . . . . 15
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (๐ข(-gโ๐บ)๐ฃ) = (๐ข(+gโ๐บ)((invgโ๐บ)โ๐ฃ))) |
46 | 43, 45 | oveq12d 7422 |
. . . . . . . . . . . . . 14
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((๐ข(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) = ((๐ข(+gโ๐บ)((invgโ๐บ)โ๐ฆ))(distโ๐บ)(๐ข(+gโ๐บ)((invgโ๐บ)โ๐ฃ)))) |
47 | 7, 41 | grpinvcl 18915 |
. . . . . . . . . . . . . . . 16
โข ((๐บ โ Grp โง ๐ฆ โ (Baseโ๐บ)) โ
((invgโ๐บ)โ๐ฆ) โ (Baseโ๐บ)) |
48 | 28, 20, 47 | syl2anc 583 |
. . . . . . . . . . . . . . 15
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((invgโ๐บ)โ๐ฆ) โ (Baseโ๐บ)) |
49 | 7, 41 | grpinvcl 18915 |
. . . . . . . . . . . . . . . 16
โข ((๐บ โ Grp โง ๐ฃ โ (Baseโ๐บ)) โ
((invgโ๐บ)โ๐ฃ) โ (Baseโ๐บ)) |
50 | 28, 21, 49 | syl2anc 583 |
. . . . . . . . . . . . . . 15
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((invgโ๐บ)โ๐ฃ) โ (Baseโ๐บ)) |
51 | 7, 40, 17 | ngplcan 24471 |
. . . . . . . . . . . . . . 15
โข (((๐บ โ NrmGrp โง ๐บ โ Abel) โง
(((invgโ๐บ)โ๐ฆ) โ (Baseโ๐บ) โง ((invgโ๐บ)โ๐ฃ) โ (Baseโ๐บ) โง ๐ข โ (Baseโ๐บ))) โ ((๐ข(+gโ๐บ)((invgโ๐บ)โ๐ฆ))(distโ๐บ)(๐ข(+gโ๐บ)((invgโ๐บ)โ๐ฃ))) = (((invgโ๐บ)โ๐ฆ)(distโ๐บ)((invgโ๐บ)โ๐ฃ))) |
52 | 12, 48, 50, 16, 51 | syl13anc 1369 |
. . . . . . . . . . . . . 14
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((๐ข(+gโ๐บ)((invgโ๐บ)โ๐ฆ))(distโ๐บ)(๐ข(+gโ๐บ)((invgโ๐บ)โ๐ฃ))) = (((invgโ๐บ)โ๐ฆ)(distโ๐บ)((invgโ๐บ)โ๐ฃ))) |
53 | 7, 41, 17 | ngpinvds 24473 |
. . . . . . . . . . . . . . 15
โข (((๐บ โ NrmGrp โง ๐บ โ Abel) โง (๐ฆ โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (((invgโ๐บ)โ๐ฆ)(distโ๐บ)((invgโ๐บ)โ๐ฃ)) = (๐ฆ(distโ๐บ)๐ฃ)) |
54 | 12, 20, 21, 53 | syl12anc 834 |
. . . . . . . . . . . . . 14
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (((invgโ๐บ)โ๐ฆ)(distโ๐บ)((invgโ๐บ)โ๐ฃ)) = (๐ฆ(distโ๐บ)๐ฃ)) |
55 | 46, 52, 54 | 3eqtrd 2770 |
. . . . . . . . . . . . 13
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((๐ข(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) = (๐ฆ(distโ๐บ)๐ฃ)) |
56 | 39, 55 | oveq12d 7422 |
. . . . . . . . . . . 12
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฆ)) + ((๐ข(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ))) = ((๐ฅ(distโ๐บ)๐ข) + (๐ฆ(distโ๐บ)๐ฃ))) |
57 | 36, 56 | breqtrd 5167 |
. . . . . . . . . . 11
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) โค ((๐ฅ(distโ๐บ)๐ข) + (๐ฆ(distโ๐บ)๐ฃ))) |
58 | 7, 17 | mscl 24318 |
. . . . . . . . . . . . 13
โข ((๐บ โ MetSp โง (๐ฅ(-gโ๐บ)๐ฆ) โ (Baseโ๐บ) โง (๐ข(-gโ๐บ)๐ฃ) โ (Baseโ๐บ)) โ ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) โ โ) |
59 | 13, 30, 32, 58 | syl3anc 1368 |
. . . . . . . . . . . 12
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) โ โ) |
60 | 19, 23 | readdcld 11244 |
. . . . . . . . . . . 12
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((๐ฅ(distโ๐บ)๐ข) + (๐ฆ(distโ๐บ)๐ฃ)) โ โ) |
61 | | lelttr 11305 |
. . . . . . . . . . . 12
โข ((((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) โ โ โง ((๐ฅ(distโ๐บ)๐ข) + (๐ฆ(distโ๐บ)๐ฃ)) โ โ โง ๐ง โ โ) โ ((((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) โค ((๐ฅ(distโ๐บ)๐ข) + (๐ฆ(distโ๐บ)๐ฃ)) โง ((๐ฅ(distโ๐บ)๐ข) + (๐ฆ(distโ๐บ)๐ฃ)) < ๐ง) โ ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)) |
62 | 59, 60, 25, 61 | syl3anc 1368 |
. . . . . . . . . . 11
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) โค ((๐ฅ(distโ๐บ)๐ข) + (๐ฆ(distโ๐บ)๐ฃ)) โง ((๐ฅ(distโ๐บ)๐ข) + (๐ฆ(distโ๐บ)๐ฃ)) < ๐ง) โ ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)) |
63 | 57, 62 | mpand 692 |
. . . . . . . . . 10
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (((๐ฅ(distโ๐บ)๐ข) + (๐ฆ(distโ๐บ)๐ฃ)) < ๐ง โ ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)) |
64 | 27, 63 | syld 47 |
. . . . . . . . 9
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (((๐ฅ(distโ๐บ)๐ข) < (๐ง / 2) โง (๐ฆ(distโ๐บ)๐ฃ) < (๐ง / 2)) โ ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)) |
65 | 15, 16 | ovresd 7570 |
. . . . . . . . . . 11
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) = (๐ฅ(distโ๐บ)๐ข)) |
66 | 65 | breq1d 5151 |
. . . . . . . . . 10
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < (๐ง / 2) โ (๐ฅ(distโ๐บ)๐ข) < (๐ง / 2))) |
67 | 20, 21 | ovresd 7570 |
. . . . . . . . . . 11
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) = (๐ฆ(distโ๐บ)๐ฃ)) |
68 | 67 | breq1d 5151 |
. . . . . . . . . 10
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < (๐ง / 2) โ (๐ฆ(distโ๐บ)๐ฃ) < (๐ง / 2))) |
69 | 66, 68 | anbi12d 630 |
. . . . . . . . 9
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < (๐ง / 2) โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < (๐ง / 2)) โ ((๐ฅ(distโ๐บ)๐ข) < (๐ง / 2) โง (๐ฆ(distโ๐บ)๐ฃ) < (๐ง / 2)))) |
70 | 30, 32 | ovresd 7570 |
. . . . . . . . . 10
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) = ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ))) |
71 | 70 | breq1d 5151 |
. . . . . . . . 9
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง โ ((๐ฅ(-gโ๐บ)๐ฆ)(distโ๐บ)(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)) |
72 | 64, 69, 71 | 3imtr4d 294 |
. . . . . . . 8
โข
(((((๐บ โ NrmGrp
โง ๐บ โ Abel) โง
(๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โง (๐ข โ (Baseโ๐บ) โง ๐ฃ โ (Baseโ๐บ))) โ (((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < (๐ง / 2) โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < (๐ง / 2)) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)) |
73 | 72 | ralrimivva 3194 |
. . . . . . 7
โข ((((๐บ โ NrmGrp โง ๐บ โ Abel) โง (๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โ
โ๐ข โ
(Baseโ๐บ)โ๐ฃ โ (Baseโ๐บ)(((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < (๐ง / 2) โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < (๐ง / 2)) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)) |
74 | | breq2 5145 |
. . . . . . . . . . 11
โข (๐ = (๐ง / 2) โ ((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < ๐ โ (๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < (๐ง / 2))) |
75 | | breq2 5145 |
. . . . . . . . . . 11
โข (๐ = (๐ง / 2) โ ((๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < ๐ โ (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < (๐ง / 2))) |
76 | 74, 75 | anbi12d 630 |
. . . . . . . . . 10
โข (๐ = (๐ง / 2) โ (((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < ๐ โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < ๐) โ ((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < (๐ง / 2) โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < (๐ง / 2)))) |
77 | 76 | imbi1d 341 |
. . . . . . . . 9
โข (๐ = (๐ง / 2) โ ((((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < ๐ โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < ๐) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง) โ (((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < (๐ง / 2) โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < (๐ง / 2)) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง))) |
78 | 77 | 2ralbidv 3212 |
. . . . . . . 8
โข (๐ = (๐ง / 2) โ (โ๐ข โ (Baseโ๐บ)โ๐ฃ โ (Baseโ๐บ)(((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < ๐ โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < ๐) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง) โ โ๐ข โ (Baseโ๐บ)โ๐ฃ โ (Baseโ๐บ)(((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < (๐ง / 2) โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < (๐ง / 2)) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง))) |
79 | 78 | rspcev 3606 |
. . . . . . 7
โข (((๐ง / 2) โ โ+
โง โ๐ข โ
(Baseโ๐บ)โ๐ฃ โ (Baseโ๐บ)(((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < (๐ง / 2) โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < (๐ง / 2)) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)) โ โ๐ โ โ+ โ๐ข โ (Baseโ๐บ)โ๐ฃ โ (Baseโ๐บ)(((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < ๐ โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < ๐) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)) |
80 | 11, 73, 79 | syl2an2 683 |
. . . . . 6
โข ((((๐บ โ NrmGrp โง ๐บ โ Abel) โง (๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โง ๐ง โ โ+) โ
โ๐ โ
โ+ โ๐ข โ (Baseโ๐บ)โ๐ฃ โ (Baseโ๐บ)(((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < ๐ โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < ๐) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)) |
81 | 80 | ralrimiva 3140 |
. . . . 5
โข (((๐บ โ NrmGrp โง ๐บ โ Abel) โง (๐ฅ โ (Baseโ๐บ) โง ๐ฆ โ (Baseโ๐บ))) โ โ๐ง โ โ+ โ๐ โ โ+
โ๐ข โ
(Baseโ๐บ)โ๐ฃ โ (Baseโ๐บ)(((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < ๐ โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < ๐) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)) |
82 | 81 | ralrimivva 3194 |
. . . 4
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ
โ๐ฅ โ
(Baseโ๐บ)โ๐ฆ โ (Baseโ๐บ)โ๐ง โ โ+ โ๐ โ โ+
โ๐ข โ
(Baseโ๐บ)โ๐ฃ โ (Baseโ๐บ)(((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < ๐ โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < ๐) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)) |
83 | | msxms 24311 |
. . . . . 6
โข (๐บ โ MetSp โ ๐บ โ
โMetSp) |
84 | | eqid 2726 |
. . . . . . 7
โข
((distโ๐บ)
โพ ((Baseโ๐บ)
ร (Baseโ๐บ))) =
((distโ๐บ) โพ
((Baseโ๐บ) ร
(Baseโ๐บ))) |
85 | 7, 84 | xmsxmet 24313 |
. . . . . 6
โข (๐บ โ โMetSp โ
((distโ๐บ) โพ
((Baseโ๐บ) ร
(Baseโ๐บ))) โ
(โMetโ(Baseโ๐บ))) |
86 | 4, 83, 85 | 3syl 18 |
. . . . 5
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ
((distโ๐บ) โพ
((Baseโ๐บ) ร
(Baseโ๐บ))) โ
(โMetโ(Baseโ๐บ))) |
87 | | eqid 2726 |
. . . . . 6
โข
(MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))) = (MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))) |
88 | 87, 87, 87 | txmetcn 24408 |
. . . . 5
โข
((((distโ๐บ)
โพ ((Baseโ๐บ)
ร (Baseโ๐บ)))
โ (โMetโ(Baseโ๐บ)) โง ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ))) โ
(โMetโ(Baseโ๐บ)) โง ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ))) โ
(โMetโ(Baseโ๐บ))) โ ((-gโ๐บ) โ
(((MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))) รt
(MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ))))) Cn (MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ))))) โ
((-gโ๐บ):((Baseโ๐บ) ร (Baseโ๐บ))โถ(Baseโ๐บ) โง โ๐ฅ โ (Baseโ๐บ)โ๐ฆ โ (Baseโ๐บ)โ๐ง โ โ+ โ๐ โ โ+
โ๐ข โ
(Baseโ๐บ)โ๐ฃ โ (Baseโ๐บ)(((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < ๐ โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < ๐) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)))) |
89 | 86, 86, 86, 88 | syl3anc 1368 |
. . . 4
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ
((-gโ๐บ)
โ (((MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))) รt
(MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ))))) Cn (MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ))))) โ
((-gโ๐บ):((Baseโ๐บ) ร (Baseโ๐บ))โถ(Baseโ๐บ) โง โ๐ฅ โ (Baseโ๐บ)โ๐ฆ โ (Baseโ๐บ)โ๐ง โ โ+ โ๐ โ โ+
โ๐ข โ
(Baseโ๐บ)โ๐ฃ โ (Baseโ๐บ)(((๐ฅ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ข) < ๐ โง (๐ฆ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))๐ฃ) < ๐) โ ((๐ฅ(-gโ๐บ)๐ฆ)((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))(๐ข(-gโ๐บ)๐ฃ)) < ๐ง)))) |
90 | 10, 82, 89 | mpbir2and 710 |
. . 3
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ
(-gโ๐บ)
โ (((MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))) รt
(MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ))))) Cn (MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))))) |
91 | | eqid 2726 |
. . . . . . 7
โข
(TopOpenโ๐บ) =
(TopOpenโ๐บ) |
92 | 91, 7, 84 | mstopn 24309 |
. . . . . 6
โข (๐บ โ MetSp โ
(TopOpenโ๐บ) =
(MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ))))) |
93 | 4, 92 | syl 17 |
. . . . 5
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ
(TopOpenโ๐บ) =
(MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ))))) |
94 | 93, 93 | oveq12d 7422 |
. . . 4
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ
((TopOpenโ๐บ)
รt (TopOpenโ๐บ)) = ((MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))) รt
(MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))))) |
95 | 94, 93 | oveq12d 7422 |
. . 3
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ
(((TopOpenโ๐บ)
รt (TopOpenโ๐บ)) Cn (TopOpenโ๐บ)) = (((MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))) รt
(MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ))))) Cn (MetOpenโ((distโ๐บ) โพ ((Baseโ๐บ) ร (Baseโ๐บ)))))) |
96 | 90, 95 | eleqtrrd 2830 |
. 2
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ
(-gโ๐บ)
โ (((TopOpenโ๐บ)
รt (TopOpenโ๐บ)) Cn (TopOpenโ๐บ))) |
97 | 91, 8 | istgp2 23946 |
. 2
โข (๐บ โ TopGrp โ (๐บ โ Grp โง ๐บ โ TopSp โง
(-gโ๐บ)
โ (((TopOpenโ๐บ)
รt (TopOpenโ๐บ)) Cn (TopOpenโ๐บ)))) |
98 | 2, 6, 96, 97 | syl3anbrc 1340 |
1
โข ((๐บ โ NrmGrp โง ๐บ โ Abel) โ ๐บ โ TopGrp) |