Theorem tngnm

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

	Ref	Expression
Hypotheses	tngnm.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
	tngnm.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	tngnm.a	⊢ 𝐴 ∈ V
Assertion	tngnm	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑁 = ( norm ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		tngnm.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2		tngnm.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
3		tngnm.a	⊢ 𝐴 ∈ V
4		simpr	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑁 : 𝑋 ⟶ 𝐴 )
5	4	feqmptd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑁 ‘ 𝑥 ) ) )
6		eqid	⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
7	2 6	grpsubf	⊢ ( 𝐺 ∈ Grp → ( -g ‘ 𝐺 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
8	7	ad2antrr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( -g ‘ 𝐺 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
9		simpr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
10		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
11	2 10	grpidcl	⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
12	11	ad2antrr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
13	9 12	opelxpd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ∈ ( 𝑋 × 𝑋 ) )
14		fvco3	⊢ ( ( ( -g ‘ 𝐺 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ) = ( 𝑁 ‘ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ) ) )
15	8 13 14	syl2anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ) = ( 𝑁 ‘ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ) ) )
16		df-ov	⊢ ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) = ( ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ )
17		df-ov	⊢ ( 𝑥 ( -g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ )
18	17	fveq2i	⊢ ( 𝑁 ‘ ( 𝑥 ( -g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) = ( 𝑁 ‘ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ) )
19	15 16 18	3eqtr4g	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) = ( 𝑁 ‘ ( 𝑥 ( -g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) )
20	2 10 6	grpsubid1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( -g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = 𝑥 )
21	20	adantlr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( -g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = 𝑥 )
22	21	fveq2d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑥 ( -g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) = ( 𝑁 ‘ 𝑥 ) )
23	19 22	eqtr2d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑥 ) = ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) )
24	23	mpteq2dva	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑁 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) ) )
25	2	fvexi	⊢ 𝑋 ∈ V
26		fex2	⊢ ( ( 𝑁 : 𝑋 ⟶ 𝐴 ∧ 𝑋 ∈ V ∧ 𝐴 ∈ V ) → 𝑁 ∈ V )
27	25 3 26	mp3an23	⊢ ( 𝑁 : 𝑋 ⟶ 𝐴 → 𝑁 ∈ V )
28	27	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑁 ∈ V )
29	1 2	tngbas	⊢ ( 𝑁 ∈ V → 𝑋 = ( Base ‘ 𝑇 ) )
30	28 29	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑋 = ( Base ‘ 𝑇 ) )
31	1 6	tngds	⊢ ( 𝑁 ∈ V → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( dist ‘ 𝑇 ) )
32	28 31	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( dist ‘ 𝑇 ) )
33		eqidd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑥 = 𝑥 )
34	1 10	tng0	⊢ ( 𝑁 ∈ V → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝑇 ) )
35	28 34	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝑇 ) )
36	32 33 35	oveq123d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) = ( 𝑥 ( dist ‘ 𝑇 ) ( 0g ‘ 𝑇 ) ) )
37	30 36	mpteq12dv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝑇 ) ↦ ( 𝑥 ( dist ‘ 𝑇 ) ( 0g ‘ 𝑇 ) ) ) )
38		eqid	⊢ ( norm ‘ 𝑇 ) = ( norm ‘ 𝑇 )
39		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
40		eqid	⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
41		eqid	⊢ ( dist ‘ 𝑇 ) = ( dist ‘ 𝑇 )
42	38 39 40 41	nmfval	⊢ ( norm ‘ 𝑇 ) = ( 𝑥 ∈ ( Base ‘ 𝑇 ) ↦ ( 𝑥 ( dist ‘ 𝑇 ) ( 0g ‘ 𝑇 ) ) )
43	37 42	eqtr4di	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) ) = ( norm ‘ 𝑇 ) )
44	5 24 43	3eqtrd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑁 = ( norm ‘ 𝑇 ) )