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	$⊢ (G \in NrmGrp \land G \in Abel) \to G \in TopGrp$

Proof

Step	Hyp	Ref	Expression
1		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
2	1	adantr	$⊢ (G \in NrmGrp \land G \in Abel) \to G \in Grp$
3		ngpms	$⊢ G \in NrmGrp \to G \in MetSp$
4	3	adantr	$⊢ (G \in NrmGrp \land G \in Abel) \to G \in MetSp$
5		mstps	$⊢ G \in MetSp \to G \in TopSp$
6	4 5	syl	$⊢ (G \in NrmGrp \land G \in Abel) \to G \in TopSp$
7		eqid	$⊢ {Base}_{G} = {Base}_{G}$
8		eqid	$⊢ -_{G} = -_{G}$
9	7 8	grpsubf	$⊢ G \in Grp \to -_{G} : {Base}_{G} \times {Base}_{G} ⟶ {Base}_{G}$
10	2 9	syl	$⊢ (G \in NrmGrp \land G \in Abel) \to -_{G} : {Base}_{G} \times {Base}_{G} ⟶ {Base}_{G}$
11		rphalfcl	$⊢ z \in ℝ^{+} \to \frac{z}{2} \in ℝ^{+}$
12		simplll	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (G \in NrmGrp \land G \in Abel)$
13	12 4	syl	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to G \in MetSp$
14		simpllr	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (x \in {Base}_{G} \land y \in {Base}_{G})$
15	14	simpld	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to x \in {Base}_{G}$
16		simprl	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to u \in {Base}_{G}$
17		eqid	$⊢ dist (G) = dist (G)$
18	7 17	mscl	$⊢ (G \in MetSp \land x \in {Base}_{G} \land u \in {Base}_{G}) \to x dist (G) u \in ℝ$
19	13 15 16 18	syl3anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to x dist (G) u \in ℝ$
20	14	simprd	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to y \in {Base}_{G}$
21		simprr	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to v \in {Base}_{G}$
22	7 17	mscl	$⊢ (G \in MetSp \land y \in {Base}_{G} \land v \in {Base}_{G}) \to y dist (G) v \in ℝ$
23	13 20 21 22	syl3anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to y dist (G) v \in ℝ$
24		rpre	$⊢ z \in ℝ^{+} \to z \in ℝ$
25	24	ad2antlr	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to z \in ℝ$
26		lt2halves	$⊢ (x dist (G) u \in ℝ \land y dist (G) v \in ℝ \land z \in ℝ) \to ((x dist (G) u < \frac{z}{2} \land y dist (G) v < \frac{z}{2}) \to (x dist (G) u) + (y dist (G) v) < z)$
27	19 23 25 26	syl3anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to ((x dist (G) u < \frac{z}{2} \land y dist (G) v < \frac{z}{2}) \to (x dist (G) u) + (y dist (G) v) < z)$
28	12 2	syl	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to G \in Grp$
29	7 8	grpsubcl	$⊢ (G \in Grp \land x \in {Base}_{G} \land y \in {Base}_{G}) \to x -_{G} y \in {Base}_{G}$
30	28 15 20 29	syl3anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to x -_{G} y \in {Base}_{G}$
31	7 8	grpsubcl	$⊢ (G \in Grp \land u \in {Base}_{G} \land v \in {Base}_{G}) \to u -_{G} v \in {Base}_{G}$
32	28 16 21 31	syl3anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to u -_{G} v \in {Base}_{G}$
33	7 8	grpsubcl	$⊢ (G \in Grp \land u \in {Base}_{G} \land y \in {Base}_{G}) \to u -_{G} y \in {Base}_{G}$
34	28 16 20 33	syl3anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to u -_{G} y \in {Base}_{G}$
35	7 17	mstri	$⊢ (G \in MetSp \land (x -_{G} y \in {Base}_{G} \land u -_{G} v \in {Base}_{G} \land u -_{G} y \in {Base}_{G})) \to (x -_{G} y) dist (G) (u -_{G} v) \leq ((x -_{G} y) dist (G) (u -_{G} y)) + ((u -_{G} y) dist (G) (u -_{G} v))$
36	13 30 32 34 35	syl13anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (x -_{G} y) dist (G) (u -_{G} v) \leq ((x -_{G} y) dist (G) (u -_{G} y)) + ((u -_{G} y) dist (G) (u -_{G} v))$
37	12	simpld	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to G \in NrmGrp$
38	7 8 17	ngpsubcan	$⊢ (G \in NrmGrp \land (x \in {Base}_{G} \land u \in {Base}_{G} \land y \in {Base}_{G})) \to (x -_{G} y) dist (G) (u -_{G} y) = x dist (G) u$
39	37 15 16 20 38	syl13anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (x -_{G} y) dist (G) (u -_{G} y) = x dist (G) u$
40		eqid	$⊢ +_{G} = +_{G}$
41		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
42	7 40 41 8	grpsubval	$⊢ (u \in {Base}_{G} \land y \in {Base}_{G}) \to u -_{G} y = u +_{G} {inv}_{g} (G) (y)$
43	16 20 42	syl2anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to u -_{G} y = u +_{G} {inv}_{g} (G) (y)$
44	7 40 41 8	grpsubval	$⊢ (u \in {Base}_{G} \land v \in {Base}_{G}) \to u -_{G} v = u +_{G} {inv}_{g} (G) (v)$
45	44	adantl	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to u -_{G} v = u +_{G} {inv}_{g} (G) (v)$
46	43 45	oveq12d	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (u -_{G} y) dist (G) (u -_{G} v) = (u +_{G} {inv}_{g} (G) (y)) dist (G) (u +_{G} {inv}_{g} (G) (v))$
47	7 41	grpinvcl	$⊢ (G \in Grp \land y \in {Base}_{G}) \to {inv}_{g} (G) (y) \in {Base}_{G}$
48	28 20 47	syl2anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to {inv}_{g} (G) (y) \in {Base}_{G}$
49	7 41	grpinvcl	$⊢ (G \in Grp \land v \in {Base}_{G}) \to {inv}_{g} (G) (v) \in {Base}_{G}$
50	28 21 49	syl2anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to {inv}_{g} (G) (v) \in {Base}_{G}$
51	7 40 17	ngplcan	$⊢ ((G \in NrmGrp \land G \in Abel) \land ({inv}_{g} (G) (y) \in {Base}_{G} \land {inv}_{g} (G) (v) \in {Base}_{G} \land u \in {Base}_{G})) \to (u +_{G} {inv}_{g} (G) (y)) dist (G) (u +_{G} {inv}_{g} (G) (v)) = {inv}_{g} (G) (y) dist (G) {inv}_{g} (G) (v)$
52	12 48 50 16 51	syl13anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (u +_{G} {inv}_{g} (G) (y)) dist (G) (u +_{G} {inv}_{g} (G) (v)) = {inv}_{g} (G) (y) dist (G) {inv}_{g} (G) (v)$
53	7 41 17	ngpinvds	$⊢ ((G \in NrmGrp \land G \in Abel) \land (y \in {Base}_{G} \land v \in {Base}_{G})) \to {inv}_{g} (G) (y) dist (G) {inv}_{g} (G) (v) = y dist (G) v$
54	12 20 21 53	syl12anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to {inv}_{g} (G) (y) dist (G) {inv}_{g} (G) (v) = y dist (G) v$
55	46 52 54	3eqtrd	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (u -_{G} y) dist (G) (u -_{G} v) = y dist (G) v$
56	39 55	oveq12d	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to ((x -_{G} y) dist (G) (u -_{G} y)) + ((u -_{G} y) dist (G) (u -_{G} v)) = (x dist (G) u) + (y dist (G) v)$
57	36 56	breqtrd	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (x -_{G} y) dist (G) (u -_{G} v) \leq (x dist (G) u) + (y dist (G) v)$
58	7 17	mscl	$⊢ (G \in MetSp \land x -_{G} y \in {Base}_{G} \land u -_{G} v \in {Base}_{G}) \to (x -_{G} y) dist (G) (u -_{G} v) \in ℝ$
59	13 30 32 58	syl3anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (x -_{G} y) dist (G) (u -_{G} v) \in ℝ$
60	19 23	readdcld	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (x dist (G) u) + (y dist (G) v) \in ℝ$
61		lelttr	$⊢ ((x -_{G} y) dist (G) (u -_{G} v) \in ℝ \land (x dist (G) u) + (y dist (G) v) \in ℝ \land z \in ℝ) \to (((x -_{G} y) dist (G) (u -_{G} v) \leq (x dist (G) u) + (y dist (G) v) \land (x dist (G) u) + (y dist (G) v) < z) \to (x -_{G} y) dist (G) (u -_{G} v) < z)$
62	59 60 25 61	syl3anc	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (((x -_{G} y) dist (G) (u -_{G} v) \leq (x dist (G) u) + (y dist (G) v) \land (x dist (G) u) + (y dist (G) v) < z) \to (x -_{G} y) dist (G) (u -_{G} v) < z)$
63	57 62	mpand	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to ((x dist (G) u) + (y dist (G) v) < z \to (x -_{G} y) dist (G) (u -_{G} v) < z)$
64	27 63	syld	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to ((x dist (G) u < \frac{z}{2} \land y dist (G) v < \frac{z}{2}) \to (x -_{G} y) dist (G) (u -_{G} v) < z)$
65	15 16	ovresd	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u = x dist (G) u$
66	65	breq1d	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < \frac{z}{2} \leftrightarrow x dist (G) u < \frac{z}{2})$
67	20 21	ovresd	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v = y dist (G) v$
68	67	breq1d	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < \frac{z}{2} \leftrightarrow y dist (G) v < \frac{z}{2})$
69	66 68	anbi12d	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < \frac{z}{2} \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < \frac{z}{2}) \leftrightarrow (x dist (G) u < \frac{z}{2} \land y dist (G) v < \frac{z}{2}))$
70	30 32	ovresd	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) = (x -_{G} y) dist (G) (u -_{G} v)$
71	70	breq1d	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to ((x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z \leftrightarrow (x -_{G} y) dist (G) (u -_{G} v) < z)$
72	64 69 71	3imtr4d	$⊢ ((((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \land (u \in {Base}_{G} \land v \in {Base}_{G})) \to ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < \frac{z}{2} \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < \frac{z}{2}) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z)$
73	72	ralrimivva	$⊢ (((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \to \forall u \in {Base}_{G} \forall v \in {Base}_{G} ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < \frac{z}{2} \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < \frac{z}{2}) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z)$
74		breq2	$⊢ r = \frac{z}{2} \to (x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < r \leftrightarrow x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < \frac{z}{2})$
75		breq2	$⊢ r = \frac{z}{2} \to (y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < r \leftrightarrow y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < \frac{z}{2})$
76	74 75	anbi12d	$⊢ r = \frac{z}{2} \to ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < r \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < r) \leftrightarrow (x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < \frac{z}{2} \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < \frac{z}{2}))$
77	76	imbi1d	$⊢ r = \frac{z}{2} \to (((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < r \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < r) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z) \leftrightarrow ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < \frac{z}{2} \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < \frac{z}{2}) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z))$
78	77	2ralbidv	$⊢ r = \frac{z}{2} \to (\forall u \in {Base}_{G} \forall v \in {Base}_{G} ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < r \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < r) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z) \leftrightarrow \forall u \in {Base}_{G} \forall v \in {Base}_{G} ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < \frac{z}{2} \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < \frac{z}{2}) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z))$
79	78	rspcev	$⊢ (\frac{z}{2} \in ℝ^{+} \land \forall u \in {Base}_{G} \forall v \in {Base}_{G} ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < \frac{z}{2} \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < \frac{z}{2}) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z)) \to \exists r \in ℝ^{+} \forall u \in {Base}_{G} \forall v \in {Base}_{G} ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < r \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < r) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z)$
80	11 73 79	syl2an2	$⊢ (((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in ℝ^{+}) \to \exists r \in ℝ^{+} \forall u \in {Base}_{G} \forall v \in {Base}_{G} ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < r \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < r) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z)$
81	80	ralrimiva	$⊢ ((G \in NrmGrp \land G \in Abel) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to \forall z \in ℝ^{+} \exists r \in ℝ^{+} \forall u \in {Base}_{G} \forall v \in {Base}_{G} ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < r \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < r) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z)$
82	81	ralrimivva	$⊢ (G \in NrmGrp \land G \in Abel) \to \forall x \in {Base}_{G} \forall y \in {Base}_{G} \forall z \in ℝ^{+} \exists r \in ℝ^{+} \forall u \in {Base}_{G} \forall v \in {Base}_{G} ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < r \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < r) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z)$
83		msxms	$⊢ G \in MetSp \to G \in ∞MetSp$
84		eqid	$⊢ {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})} = {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}$
85	7 84	xmsxmet	$⊢ G \in ∞MetSp \to {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})} \in ∞Met ({Base}_{G})$
86	4 83 85	3syl	$⊢ (G \in NrmGrp \land G \in Abel) \to {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})} \in ∞Met ({Base}_{G})$
87		eqid	$⊢ MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) = MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})})$
88	87 87 87	txmetcn	$⊢ ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})} \in ∞Met ({Base}_{G}) \land {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})} \in ∞Met ({Base}_{G}) \land {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})} \in ∞Met ({Base}_{G})) \to (-_{G} \in ((MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) \times_{t} MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})})) Cn MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})})) \leftrightarrow (-_{G} : {Base}_{G} \times {Base}_{G} ⟶ {Base}_{G} \land \forall x \in {Base}_{G} \forall y \in {Base}_{G} \forall z \in ℝ^{+} \exists r \in ℝ^{+} \forall u \in {Base}_{G} \forall v \in {Base}_{G} ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < r \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < r) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z)))$
89	86 86 86 88	syl3anc	$⊢ (G \in NrmGrp \land G \in Abel) \to (-_{G} \in ((MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) \times_{t} MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})})) Cn MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})})) \leftrightarrow (-_{G} : {Base}_{G} \times {Base}_{G} ⟶ {Base}_{G} \land \forall x \in {Base}_{G} \forall y \in {Base}_{G} \forall z \in ℝ^{+} \exists r \in ℝ^{+} \forall u \in {Base}_{G} \forall v \in {Base}_{G} ((x ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) u < r \land y ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) v < r) \to (x -_{G} y) ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) (u -_{G} v) < z)))$
90	10 82 89	mpbir2and	$⊢ (G \in NrmGrp \land G \in Abel) \to -_{G} \in ((MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) \times_{t} MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})})) Cn MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}))$
91		eqid	$⊢ TopOpen (G) = TopOpen (G)$
92	91 7 84	mstopn	$⊢ G \in MetSp \to TopOpen (G) = MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})})$
93	4 92	syl	$⊢ (G \in NrmGrp \land G \in Abel) \to TopOpen (G) = MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})})$
94	93 93	oveq12d	$⊢ (G \in NrmGrp \land G \in Abel) \to TopOpen (G) \times_{t} TopOpen (G) = MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) \times_{t} MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})})$
95	94 93	oveq12d	$⊢ (G \in NrmGrp \land G \in Abel) \to (TopOpen (G) \times_{t} TopOpen (G)) Cn TopOpen (G) = (MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}) \times_{t} MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})})) Cn MetOpen ({dist (G) ↾}_{({Base}_{G} \times {Base}_{G})})$
96	90 95	eleqtrrd	$⊢ (G \in NrmGrp \land G \in Abel) \to -_{G} \in ((TopOpen (G) \times_{t} TopOpen (G)) Cn TopOpen (G))$
97	91 8	istgp2	$⊢ G \in TopGrp \leftrightarrow (G \in Grp \land G \in TopSp \land -_{G} \in ((TopOpen (G) \times_{t} TopOpen (G)) Cn TopOpen (G)))$
98	2 6 96 97	syl3anbrc	$⊢ (G \in NrmGrp \land G \in Abel) \to G \in TopGrp$

Metamath Proof Explorer

Theorem ngptgp

Proof