Theorem tngds

Description: The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015)

	Ref	Expression
Hypotheses	tngbas.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
	tngds.2	⊢ − = ( -g ‘ 𝐺 )
Assertion	tngds	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		tngbas.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2		tngds.2	⊢ − = ( -g ‘ 𝐺 )
3		dsid	⊢ dist = Slot ( dist ‘ ndx )
4		9re	⊢ 9 ∈ ℝ
5		1nn	⊢ 1 ∈ ℕ
6		2nn0	⊢ 2 ∈ ℕ0
7		9nn0	⊢ 9 ∈ ℕ0
8		9lt10	⊢ 9 < ; 1 0
9	5 6 7 8	declti	⊢ 9 < ; 1 2
10	4 9	gtneii	⊢ ; 1 2 ≠ 9
11		dsndx	⊢ ( dist ‘ ndx ) = ; 1 2
12		tsetndx	⊢ ( TopSet ‘ ndx ) = 9
13	11 12	neeq12i	⊢ ( ( dist ‘ ndx ) ≠ ( TopSet ‘ ndx ) ↔ ; 1 2 ≠ 9 )
14	10 13	mpbir	⊢ ( dist ‘ ndx ) ≠ ( TopSet ‘ ndx )
15	3 14	setsnid	⊢ ( dist ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) ) = ( dist ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ − ) ) ⟩ ) )
16	2	fvexi	⊢ − ∈ V
17		coexg	⊢ ( ( 𝑁 ∈ 𝑉 ∧ − ∈ V ) → ( 𝑁 ∘ − ) ∈ V )
18	16 17	mpan2	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∘ − ) ∈ V )
19	3	setsid	⊢ ( ( 𝐺 ∈ V ∧ ( 𝑁 ∘ − ) ∈ V ) → ( 𝑁 ∘ − ) = ( dist ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) ) )
20	18 19	sylan2	⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∘ − ) = ( dist ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) ) )
21		eqid	⊢ ( 𝑁 ∘ − ) = ( 𝑁 ∘ − )
22		eqid	⊢ ( MetOpen ‘ ( 𝑁 ∘ − ) ) = ( MetOpen ‘ ( 𝑁 ∘ − ) )
23	1 2 21 22	tngval	⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → 𝑇 = ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ − ) ) ⟩ ) )
24	23	fveq2d	⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( dist ‘ 𝑇 ) = ( dist ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ − ) ) ⟩ ) ) )
25	15 20 24	3eqtr4a	⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )
26		co02	⊢ ( 𝑁 ∘ ∅ ) = ∅
27		df-ds	⊢ dist = Slot ; 1 2
28	27	str0	⊢ ∅ = ( dist ‘ ∅ )
29	26 28	eqtri	⊢ ( 𝑁 ∘ ∅ ) = ( dist ‘ ∅ )
30		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( -g ‘ 𝐺 ) = ∅ )
31	2 30	syl5eq	⊢ ( ¬ 𝐺 ∈ V → − = ∅ )
32	31	coeq2d	⊢ ( ¬ 𝐺 ∈ V → ( 𝑁 ∘ − ) = ( 𝑁 ∘ ∅ ) )
33		reldmtng	⊢ Rel dom toNrmGrp
34	33	ovprc1	⊢ ( ¬ 𝐺 ∈ V → ( 𝐺 toNrmGrp 𝑁 ) = ∅ )
35	1 34	syl5eq	⊢ ( ¬ 𝐺 ∈ V → 𝑇 = ∅ )
36	35	fveq2d	⊢ ( ¬ 𝐺 ∈ V → ( dist ‘ 𝑇 ) = ( dist ‘ ∅ ) )
37	29 32 36	3eqtr4a	⊢ ( ¬ 𝐺 ∈ V → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )
38	37	adantr	⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )
39	25 38	pm2.61ian	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )