tngtopn

Description: The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	tngbas.t	$⊢ T = G toNrmGrp N$
	tngtset.2	$⊢ D = dist (T)$
	tngtset.3	$⊢ J = MetOpen (D)$
Assertion	tngtopn	$⊢ (G \in V \land N \in W) \to J = TopOpen (T)$

Proof

Step	Hyp	Ref	Expression
1		tngbas.t	$⊢ T = G toNrmGrp N$
2		tngtset.2	$⊢ D = dist (T)$
3		tngtset.3	$⊢ J = MetOpen (D)$
4	1 2 3	tngtset	$⊢ (G \in V \land N \in W) \to J = TopSet (T)$
5		df-mopn	$⊢ MetOpen = (x \in ⋃ ran ∞Met ⟼ topGen (ran ball (x)))$
6	5	dmmptss	$⊢ dom MetOpen \subseteq ⋃ ran ∞Met$
7	6	sseli	$⊢ D \in dom MetOpen \to D \in ⋃ ran ∞Met$
8		eqid	$⊢ -_{G} = -_{G}$
9	1 8	tngds	$⊢ N \in W \to N \circ -_{G} = dist (T)$
10	9 2	eqtr4di	$⊢ N \in W \to N \circ -_{G} = D$
11	10	adantl	$⊢ (G \in V \land N \in W) \to N \circ -_{G} = D$
12	11	dmeqd	$⊢ (G \in V \land N \in W) \to dom (N \circ -_{G}) = dom D$
13		dmcoss	$⊢ dom (N \circ -_{G}) \subseteq dom -_{G}$
14		eqid	$⊢ {Base}_{G} = {Base}_{G}$
15		eqid	$⊢ +_{G} = +_{G}$
16		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
17	14 15 16 8	grpsubfval	$⊢ -_{G} = (x \in {Base}_{G}, y \in {Base}_{G} ⟼ x +_{G} {inv}_{g} (G) (y))$
18		ovex	$⊢ x +_{G} {inv}_{g} (G) (y) \in V$
19	17 18	dmmpo	$⊢ dom -_{G} = {Base}_{G} \times {Base}_{G}$
20	13 19	sseqtri	$⊢ dom (N \circ -_{G}) \subseteq {Base}_{G} \times {Base}_{G}$
21	12 20	eqsstrrdi	$⊢ (G \in V \land N \in W) \to dom D \subseteq {Base}_{G} \times {Base}_{G}$
22	21	adantr	$⊢ ((G \in V \land N \in W) \land D \in ⋃ ran ∞Met) \to dom D \subseteq {Base}_{G} \times {Base}_{G}$
23		dmss	$⊢ dom D \subseteq {Base}_{G} \times {Base}_{G} \to dom dom D \subseteq dom ({Base}_{G} \times {Base}_{G})$
24	22 23	syl	$⊢ ((G \in V \land N \in W) \land D \in ⋃ ran ∞Met) \to dom dom D \subseteq dom ({Base}_{G} \times {Base}_{G})$
25		dmxpid	$⊢ dom ({Base}_{G} \times {Base}_{G}) = {Base}_{G}$
26	24 25	sseqtrdi	$⊢ ((G \in V \land N \in W) \land D \in ⋃ ran ∞Met) \to dom dom D \subseteq {Base}_{G}$
27		simpr	$⊢ ((G \in V \land N \in W) \land D \in ⋃ ran ∞Met) \to D \in ⋃ ran ∞Met$
28		xmetunirn	$⊢ D \in ⋃ ran ∞Met \leftrightarrow D \in ∞Met (dom dom D)$
29	27 28	sylib	$⊢ ((G \in V \land N \in W) \land D \in ⋃ ran ∞Met) \to D \in ∞Met (dom dom D)$
30		eqid	$⊢ MetOpen (D) = MetOpen (D)$
31	30	mopnuni	$⊢ D \in ∞Met (dom dom D) \to dom dom D = ⋃ MetOpen (D)$
32	29 31	syl	$⊢ ((G \in V \land N \in W) \land D \in ⋃ ran ∞Met) \to dom dom D = ⋃ MetOpen (D)$
33	1 14	tngbas	$⊢ N \in W \to {Base}_{G} = {Base}_{T}$
34	33	ad2antlr	$⊢ ((G \in V \land N \in W) \land D \in ⋃ ran ∞Met) \to {Base}_{G} = {Base}_{T}$
35	26 32 34	3sstr3d	$⊢ ((G \in V \land N \in W) \land D \in ⋃ ran ∞Met) \to ⋃ MetOpen (D) \subseteq {Base}_{T}$
36		sspwuni	$⊢ MetOpen (D) \subseteq 𝒫 {Base}_{T} \leftrightarrow ⋃ MetOpen (D) \subseteq {Base}_{T}$
37	35 36	sylibr	$⊢ ((G \in V \land N \in W) \land D \in ⋃ ran ∞Met) \to MetOpen (D) \subseteq 𝒫 {Base}_{T}$
38	37	ex	$⊢ (G \in V \land N \in W) \to (D \in ⋃ ran ∞Met \to MetOpen (D) \subseteq 𝒫 {Base}_{T})$
39	7 38	syl5	$⊢ (G \in V \land N \in W) \to (D \in dom MetOpen \to MetOpen (D) \subseteq 𝒫 {Base}_{T})$
40		ndmfv	$⊢ \neg D \in dom MetOpen \to MetOpen (D) = \emptyset$
41		0ss	$⊢ \emptyset \subseteq 𝒫 {Base}_{T}$
42	40 41	eqsstrdi	$⊢ \neg D \in dom MetOpen \to MetOpen (D) \subseteq 𝒫 {Base}_{T}$
43	39 42	pm2.61d1	$⊢ (G \in V \land N \in W) \to MetOpen (D) \subseteq 𝒫 {Base}_{T}$
44	3 43	eqsstrid	$⊢ (G \in V \land N \in W) \to J \subseteq 𝒫 {Base}_{T}$
45	4 44	eqsstrrd	$⊢ (G \in V \land N \in W) \to TopSet (T) \subseteq 𝒫 {Base}_{T}$
46		eqid	$⊢ {Base}_{T} = {Base}_{T}$
47		eqid	$⊢ TopSet (T) = TopSet (T)$
48	46 47	topnid	$⊢ TopSet (T) \subseteq 𝒫 {Base}_{T} \to TopSet (T) = TopOpen (T)$
49	45 48	syl	$⊢ (G \in V \land N \in W) \to TopSet (T) = TopOpen (T)$
50	4 49	eqtrd	$⊢ (G \in V \land N \in W) \to J = TopOpen (T)$

Metamath Proof Explorer

Theorem tngtopn

Proof