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	$$⊢T=G\mathrm{toNrmGrp}N$$
	tngds.2	$$⊢\underset{\dot{}}{-}={-}_G$$
Assertion	tngds	$$⊢N\in V\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(T\right)$$

Proof

Step	Hyp	Ref	Expression
1		tngbas.t	$$⊢T=G\mathrm{toNrmGrp}N$$
2		tngds.2	$$⊢\underset{\dot{}}{-}={-}_G$$
3		dsid	$$⊢\mathrm{dist}=\mathrm{Slot}\mathrm{dist}\left(\mathrm{ndx}\right)$$
4		9re	$$⊢9\in ℝ$$
5		1nn	$$⊢1\in \mathbb{N}$$
6		2nn0	$$⊢2\in {\mathbb{N}}_0$$
7		9nn0	$$⊢9\in {\mathbb{N}}_0$$
8		9lt10	$$⊢9<10$$
9	5 6 7 8	declti	$$⊢9<12$$
10	4 9	gtneii	$$⊢12\ne 9$$
11		dsndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)=12$$
12		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
13	11 12	neeq12i	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\leftrightarrow 12\ne 9$$
14	10 13	mpbir	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
15	3 14	setsnid	$$⊢\mathrm{dist}\left(G\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),N\circ \underset{\dot{}}{-}⟩\right)=\mathrm{dist}\left(\left(G\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),N\circ \underset{\dot{}}{-}⟩\right)\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(N\circ \underset{\dot{}}{-}\right)⟩\right)$$
16	2	fvexi	$$⊢\underset{\dot{}}{-}\in \mathrm{V}$$
17		coexg	$$⊢\left(N\in V\wedge \underset{\dot{}}{-}\in \mathrm{V}\right)\to N\circ \underset{\dot{}}{-}\in \mathrm{V}$$
18	16 17	mpan2	$$⊢N\in V\to N\circ \underset{\dot{}}{-}\in \mathrm{V}$$
19	3	setsid	$$⊢\left(G\in \mathrm{V}\wedge N\circ \underset{\dot{}}{-}\in \mathrm{V}\right)\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(G\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),N\circ \underset{\dot{}}{-}⟩\right)$$
20	18 19	sylan2	$$⊢\left(G\in \mathrm{V}\wedge N\in V\right)\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(G\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),N\circ \underset{\dot{}}{-}⟩\right)$$
21		eqid	$$⊢N\circ \underset{\dot{}}{-}=N\circ \underset{\dot{}}{-}$$
22		eqid	$$⊢\mathrm{MetOpen}\left(N\circ \underset{\dot{}}{-}\right)=\mathrm{MetOpen}\left(N\circ \underset{\dot{}}{-}\right)$$
23	1 2 21 22	tngval	$$⊢\left(G\in \mathrm{V}\wedge N\in V\right)\to T=\left(G\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),N\circ \underset{\dot{}}{-}⟩\right)\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(N\circ \underset{\dot{}}{-}\right)⟩$$
24	23	fveq2d	$$⊢\left(G\in \mathrm{V}\wedge N\in V\right)\to \mathrm{dist}\left(T\right)=\mathrm{dist}\left(\left(G\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),N\circ \underset{\dot{}}{-}⟩\right)\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(N\circ \underset{\dot{}}{-}\right)⟩\right)$$
25	15 20 24	3eqtr4a	$$⊢\left(G\in \mathrm{V}\wedge N\in V\right)\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(T\right)$$
26		co02	$$⊢N\circ \varnothing =\varnothing$$
27		df-ds	$$⊢\mathrm{dist}=\mathrm{Slot}12$$
28	27	str0	$$⊢\varnothing =\mathrm{dist}\left(\varnothing \right)$$
29	26 28	eqtri	$$⊢N\circ \varnothing =\mathrm{dist}\left(\varnothing \right)$$
30		fvprc	$$⊢\neg G\in \mathrm{V}\to {-}_G=\varnothing$$
31	2 30	syl5eq	$$⊢\neg G\in \mathrm{V}\to \underset{\dot{}}{-}=\varnothing$$
32	31	coeq2d	$$⊢\neg G\in \mathrm{V}\to N\circ \underset{\dot{}}{-}=N\circ \varnothing$$
33		reldmtng	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{toNrmGrp}$$
34	33	ovprc1	$$⊢\neg G\in \mathrm{V}\to G\mathrm{toNrmGrp}N=\varnothing$$
35	1 34	syl5eq	$$⊢\neg G\in \mathrm{V}\to T=\varnothing$$
36	35	fveq2d	$$⊢\neg G\in \mathrm{V}\to \mathrm{dist}\left(T\right)=\mathrm{dist}\left(\varnothing \right)$$
37	29 32 36	3eqtr4a	$$⊢\neg G\in \mathrm{V}\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(T\right)$$
38	37	adantr	$$⊢\left(\neg G\in \mathrm{V}\wedge N\in V\right)\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(T\right)$$
39	25 38	pm2.61ian	$$⊢N\in V\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(T\right)$$