This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ngptgp

Description: A normed abelian group is a topological group (with the topology induced by the metric induced by the norm). (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion ngptgp ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) → 𝐺 ∈ TopGrp )

Proof

Step Hyp Ref Expression
1 ngpgrp ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
2 1 adantr ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) → 𝐺 ∈ Grp )
3 ngpms ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp )
4 3 adantr ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) → 𝐺 ∈ MetSp )
5 mstps ⊢ ( 𝐺 ∈ MetSp → 𝐺 ∈ TopSp )
6 4 5 syl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) → 𝐺 ∈ TopSp )
7 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
8 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
9 7 8 grpsubf ⊢ ( 𝐺 ∈ Grp → ( -g ‘ 𝐺 ) : ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ⟶ ( Base ‘ 𝐺 ) )
10 2 9 syl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) → ( -g ‘ 𝐺 ) : ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ⟶ ( Base ‘ 𝐺 ) )
11 rphalfcl ⊢ ( 𝑧 ∈ ℝ+ → ( 𝑧 / 2 ) ∈ ℝ+ )
12 simplll ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) )
13 12 4 syl ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → 𝐺 ∈ MetSp )
14 simpllr ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) )
15 14 simpld ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
16 simprl ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑢 ∈ ( Base ‘ 𝐺 ) )
17 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
18 7 17 mscl ⊢ ( ( 𝐺 ∈ MetSp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) ∈ ℝ )
19 13 15 16 18 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) ∈ ℝ )
20 14 simprd ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
21 simprr ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑣 ∈ ( Base ‘ 𝐺 ) )
22 7 17 mscl ⊢ ( ( 𝐺 ∈ MetSp ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ∈ ℝ )
23 13 20 21 22 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ∈ ℝ )
24 rpre ⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ )
25 24 ad2antlr ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑧 ∈ ℝ )
26 lt2halves ⊢ ( ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) ∈ ℝ ∧ ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) < ( 𝑧 / 2 ) ∧ ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) < ( 𝑧 / 2 ) ) → ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) + ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) )
27 19 23 25 26 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) < ( 𝑧 / 2 ) ∧ ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) < ( 𝑧 / 2 ) ) → ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) + ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) )
28 12 2 syl ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → 𝐺 ∈ Grp )
29 7 8 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
30 28 15 20 29 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
31 7 8 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ∈ ( Base ‘ 𝐺 ) )
32 28 16 21 31 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ∈ ( Base ‘ 𝐺 ) )
33 7 8 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
34 28 16 20 33 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
35 7 17 mstri ⊢ ( ( 𝐺 ∈ MetSp ∧ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) ≤ ( ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ) + ( ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) ) )
36 13 30 32 34 35 syl13anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) ≤ ( ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ) + ( ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) ) )
37 12 simpld ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → 𝐺 ∈ NrmGrp )
38 7 8 17 ngpsubcan ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) )
39 37 15 16 20 38 syl13anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) )
40 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
41 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
42 7 40 41 8 grpsubval ⊢ ( ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) = ( 𝑢 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) )
43 16 20 42 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) = ( 𝑢 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) )
44 7 40 41 8 grpsubval ⊢ ( ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) = ( 𝑢 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑣 ) ) )
45 44 adantl ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) = ( 𝑢 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑣 ) ) )
46 43 45 oveq12d ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) = ( ( 𝑢 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( dist ‘ 𝐺 ) ( 𝑢 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑣 ) ) ) )
47 7 41 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
48 28 20 47 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
49 7 41 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ( Base ‘ 𝐺 ) )
50 28 21 49 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ( Base ‘ 𝐺 ) )
51 7 40 17 ngplcan ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ( Base ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑢 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( dist ‘ 𝐺 ) ( 𝑢 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑣 ) ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( dist ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑣 ) ) )
52 12 48 50 16 51 syl13anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑢 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( dist ‘ 𝐺 ) ( 𝑢 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑣 ) ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( dist ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑣 ) ) )
53 7 41 17 ngpinvds ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( dist ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑣 ) ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) )
54 12 20 21 53 syl12anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( dist ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑣 ) ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) )
55 46 52 54 3eqtrd ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) )
56 39 55 oveq12d ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ) + ( ( 𝑢 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) ) = ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) + ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ) )
57 36 56 breqtrd ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) ≤ ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) + ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ) )
58 7 17 mscl ⊢ ( ( 𝐺 ∈ MetSp ∧ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) ∈ ℝ )
59 13 30 32 58 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) ∈ ℝ )
60 19 23 readdcld ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) + ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ) ∈ ℝ )
61 lelttr ⊢ ( ( ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) ∈ ℝ ∧ ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) + ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) ≤ ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) + ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ) ∧ ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) + ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) )
62 59 60 25 61 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) ≤ ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) + ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ) ∧ ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) + ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) )
63 57 62 mpand ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) + ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) ) < 𝑧 → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) )
64 27 63 syld ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) < ( 𝑧 / 2 ) ∧ ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) < ( 𝑧 / 2 ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) )
65 15 16 ovresd ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑢 ) = ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) )
66 65 breq1d ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑢 ) < ( 𝑧 / 2 ) ↔ ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) < ( 𝑧 / 2 ) ) )
67 20 21 ovresd ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑦 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑣 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) )
68 67 breq1d ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑦 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑣 ) < ( 𝑧 / 2 ) ↔ ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) < ( 𝑧 / 2 ) ) )
69 66 68 anbi12d ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( 𝑥 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑢 ) < ( 𝑧 / 2 ) ∧ ( 𝑦 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑣 ) < ( 𝑧 / 2 ) ) ↔ ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑢 ) < ( 𝑧 / 2 ) ∧ ( 𝑦 ( dist ‘ 𝐺 ) 𝑣 ) < ( 𝑧 / 2 ) ) ) )
70 30 32 ovresd ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) = ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) )
71 70 breq1d ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ↔ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( dist ‘ 𝐺 ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) )
72 64 69 71 3imtr4d ⊢ ( ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( 𝑥 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑢 ) < ( 𝑧 / 2 ) ∧ ( 𝑦 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑣 ) < ( 𝑧 / 2 ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) )
73 72 ralrimivva ⊢ ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) → ∀ 𝑢 ∈ ( Base ‘ 𝐺 ) ∀ 𝑣 ∈ ( Base ‘ 𝐺 ) ( ( ( 𝑥 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑢 ) < ( 𝑧 / 2 ) ∧ ( 𝑦 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑣 ) < ( 𝑧 / 2 ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) )
74 breq2 ⊢ ( 𝑟 = ( 𝑧 / 2 ) → ( ( 𝑥 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑢 ) < 𝑟 ↔ ( 𝑥 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑢 ) < ( 𝑧 / 2 ) ) )
75 breq2 ⊢ ( 𝑟 = ( 𝑧 / 2 ) → ( ( 𝑦 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑣 ) < 𝑟 ↔ ( 𝑦 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑣 ) < ( 𝑧 / 2 ) ) )
76 74 75 anbi12d ⊢ ( 𝑟 = ( 𝑧 / 2 ) → ( ( ( 𝑥 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑢 ) < 𝑟 ∧ ( 𝑦 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑣 ) < 𝑟 ) ↔ ( ( 𝑥 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑢 ) < ( 𝑧 / 2 ) ∧ ( 𝑦 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑣 ) < ( 𝑧 / 2 ) ) ) )
77 76 imbi1d ⊢ ( 𝑟 = ( 𝑧 / 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 ⊢ ( 𝑟 = ( 𝑧 / 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 ⊢ ( ( ( 𝑧 / 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 ⊢ ( ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ 𝑧 ∈ ℝ+ ) → ∃ 𝑟 ∈ ℝ+ ∀ 𝑢 ∈ ( Base ‘ 𝐺 ) ∀ 𝑣 ∈ ( Base ‘ 𝐺 ) ( ( ( 𝑥 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑢 ) < 𝑟 ∧ ( 𝑦 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑣 ) < 𝑟 ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) )
81 80 ralrimiva ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑟 ∈ ℝ+ ∀ 𝑢 ∈ ( Base ‘ 𝐺 ) ∀ 𝑣 ∈ ( Base ‘ 𝐺 ) ( ( ( 𝑥 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑢 ) < 𝑟 ∧ ( 𝑦 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑣 ) < 𝑟 ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) )
82 81 ralrimivva ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ℝ+ ∃ 𝑟 ∈ ℝ+ ∀ 𝑢 ∈ ( Base ‘ 𝐺 ) ∀ 𝑣 ∈ ( Base ‘ 𝐺 ) ( ( ( 𝑥 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑢 ) < 𝑟 ∧ ( 𝑦 ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝑣 ) < 𝑟 ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ( 𝑢 ( -g ‘ 𝐺 ) 𝑣 ) ) < 𝑧 ) )
83 msxms ⊢ ( 𝐺 ∈ MetSp → 𝐺 ∈ ∞MetSp )
84 eqid ⊢ ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) = ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
85 7 84 xmsxmet ⊢ ( 𝐺 ∈ ∞MetSp → ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐺 ) ) )
86 4 83 85 3syl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) → ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐺 ) ) )
87 eqid ⊢ ( MetOpen ‘ ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) )
88 87 87 87 txmetcn ⊢ ( ( ( ( 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 ⊢ ( ( 𝐺 ∈ 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 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) → ( -g ‘ 𝐺 ) ∈ ( ( ( MetOpen ‘ ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ) ×t ( MetOpen ‘ ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ) ) Cn ( MetOpen ‘ ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ) ) )
91 eqid ⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
92 91 7 84 mstopn ⊢ ( 𝐺 ∈ MetSp → ( TopOpen ‘ 𝐺 ) = ( MetOpen ‘ ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ) )
93 4 92 syl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) → ( TopOpen ‘ 𝐺 ) = ( MetOpen ‘ ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ) )
94 93 93 oveq12d ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) → ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) = ( ( MetOpen ‘ ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ) ×t ( MetOpen ‘ ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ) ) )
95 94 93 oveq12d ⊢ ( ( 𝐺 ∈ 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 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) → ( -g ‘ 𝐺 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
97 91 8 istgp2 ⊢ ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ ( -g ‘ 𝐺 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ) )
98 2 6 96 97 syl3anbrc ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) → 𝐺 ∈ TopGrp )