tngnm

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

	Ref	Expression
Hypotheses	tngnm.t	$⊢ T = G toNrmGrp N$
	tngnm.x	$⊢ X = {Base}_{G}$
	tngnm.a	$⊢ A \in V$
Assertion	tngnm	$⊢ (G \in Grp \land N : X ⟶ A) \to N = norm (T)$

Proof

Step	Hyp	Ref	Expression
1		tngnm.t	$⊢ T = G toNrmGrp N$
2		tngnm.x	$⊢ X = {Base}_{G}$
3		tngnm.a	$⊢ A \in V$
4		simpr	$⊢ (G \in Grp \land N : X ⟶ A) \to N : X ⟶ A$
5	4	feqmptd	$⊢ (G \in Grp \land N : X ⟶ A) \to N = (x \in X ⟼ N (x))$
6		eqid	$⊢ -_{G} = -_{G}$
7	2 6	grpsubf	$⊢ G \in Grp \to -_{G} : X \times X ⟶ X$
8	7	ad2antrr	$⊢ ((G \in Grp \land N : X ⟶ A) \land x \in X) \to -_{G} : X \times X ⟶ X$
9		simpr	$⊢ ((G \in Grp \land N : X ⟶ A) \land x \in X) \to x \in X$
10		eqid	$⊢ 0_{G} = 0_{G}$
11	2 10	grpidcl	$⊢ G \in Grp \to 0_{G} \in X$
12	11	ad2antrr	$⊢ ((G \in Grp \land N : X ⟶ A) \land x \in X) \to 0_{G} \in X$
13	9 12	opelxpd	$⊢ ((G \in Grp \land N : X ⟶ A) \land x \in X) \to ⟨x, 0_{G}⟩ \in (X \times X)$
14		fvco3	$⊢ (-_{G} : X \times X ⟶ X \land ⟨x, 0_{G}⟩ \in (X \times X)) \to (N \circ -_{G}) (⟨x, 0_{G}⟩) = N (-_{G} (⟨x, 0_{G}⟩))$
15	8 13 14	syl2anc	$⊢ ((G \in Grp \land N : X ⟶ A) \land x \in X) \to (N \circ -_{G}) (⟨x, 0_{G}⟩) = N (-_{G} (⟨x, 0_{G}⟩))$
16		df-ov	$⊢ x (N \circ -_{G}) 0_{G} = (N \circ -_{G}) (⟨x, 0_{G}⟩)$
17		df-ov	$⊢ x -_{G} 0_{G} = -_{G} (⟨x, 0_{G}⟩)$
18	17	fveq2i	$⊢ N (x -_{G} 0_{G}) = N (-_{G} (⟨x, 0_{G}⟩))$
19	15 16 18	3eqtr4g	$⊢ ((G \in Grp \land N : X ⟶ A) \land x \in X) \to x (N \circ -_{G}) 0_{G} = N (x -_{G} 0_{G})$
20	2 10 6	grpsubid1	$⊢ (G \in Grp \land x \in X) \to x -_{G} 0_{G} = x$
21	20	adantlr	$⊢ ((G \in Grp \land N : X ⟶ A) \land x \in X) \to x -_{G} 0_{G} = x$
22	21	fveq2d	$⊢ ((G \in Grp \land N : X ⟶ A) \land x \in X) \to N (x -_{G} 0_{G}) = N (x)$
23	19 22	eqtr2d	$⊢ ((G \in Grp \land N : X ⟶ A) \land x \in X) \to N (x) = x (N \circ -_{G}) 0_{G}$
24	23	mpteq2dva	$⊢ (G \in Grp \land N : X ⟶ A) \to (x \in X ⟼ N (x)) = (x \in X ⟼ x (N \circ -_{G}) 0_{G})$
25	2	fvexi	$⊢ X \in V$
26		fex2	$⊢ (N : X ⟶ A \land X \in V \land A \in V) \to N \in V$
27	25 3 26	mp3an23	$⊢ N : X ⟶ A \to N \in V$
28	27	adantl	$⊢ (G \in Grp \land N : X ⟶ A) \to N \in V$
29	1 2	tngbas	$⊢ N \in V \to X = {Base}_{T}$
30	28 29	syl	$⊢ (G \in Grp \land N : X ⟶ A) \to X = {Base}_{T}$
31	1 6	tngds	$⊢ N \in V \to N \circ -_{G} = dist (T)$
32	28 31	syl	$⊢ (G \in Grp \land N : X ⟶ A) \to N \circ -_{G} = dist (T)$
33		eqidd	$⊢ (G \in Grp \land N : X ⟶ A) \to x = x$
34	1 10	tng0	$⊢ N \in V \to 0_{G} = 0_{T}$
35	28 34	syl	$⊢ (G \in Grp \land N : X ⟶ A) \to 0_{G} = 0_{T}$
36	32 33 35	oveq123d	$⊢ (G \in Grp \land N : X ⟶ A) \to x (N \circ -_{G}) 0_{G} = x dist (T) 0_{T}$
37	30 36	mpteq12dv	$⊢ (G \in Grp \land N : X ⟶ A) \to (x \in X ⟼ x (N \circ -_{G}) 0_{G}) = (x \in {Base}_{T} ⟼ x dist (T) 0_{T})$
38		eqid	$⊢ norm (T) = norm (T)$
39		eqid	$⊢ {Base}_{T} = {Base}_{T}$
40		eqid	$⊢ 0_{T} = 0_{T}$
41		eqid	$⊢ dist (T) = dist (T)$
42	38 39 40 41	nmfval	$⊢ norm (T) = (x \in {Base}_{T} ⟼ x dist (T) 0_{T})$
43	37 42	syl6eqr	$⊢ (G \in Grp \land N : X ⟶ A) \to (x \in X ⟼ x (N \circ -_{G}) 0_{G}) = norm (T)$
44	5 24 43	3eqtrd	$⊢ (G \in Grp \land N : X ⟶ A) \to N = norm (T)$

Metamath Proof Explorer

Theorem tngnm

Proof