Theorem tngds

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

	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		dsndxntsetndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
5	3 4	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)$$
6	2	fvexi	$$⊢\underset{\dot{}}{-}\in \mathrm{V}$$
7		coexg	$$⊢\left(N\in V\wedge \underset{\dot{}}{-}\in \mathrm{V}\right)\to N\circ \underset{\dot{}}{-}\in \mathrm{V}$$
8	6 7	mpan2	$$⊢N\in V\to N\circ \underset{\dot{}}{-}\in \mathrm{V}$$
9	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)$$
10	8 9	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)$$
11		eqid	$$⊢N\circ \underset{\dot{}}{-}=N\circ \underset{\dot{}}{-}$$
12		eqid	$$⊢\mathrm{MetOpen}\left(N\circ \underset{\dot{}}{-}\right)=\mathrm{MetOpen}\left(N\circ \underset{\dot{}}{-}\right)$$
13	1 2 11 12	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)⟩$$
14	13	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)$$
15	5 10 14	3eqtr4a	$$⊢\left(G\in \mathrm{V}\wedge N\in V\right)\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(T\right)$$
16		co02	$$⊢N\circ \varnothing =\varnothing$$
17	3	str0	$$⊢\varnothing =\mathrm{dist}\left(\varnothing \right)$$
18	16 17	eqtri	$$⊢N\circ \varnothing =\mathrm{dist}\left(\varnothing \right)$$
19		fvprc	$$⊢\neg G\in \mathrm{V}\to {-}_G=\varnothing$$
20	2 19	syl5eq	$$⊢\neg G\in \mathrm{V}\to \underset{\dot{}}{-}=\varnothing$$
21	20	coeq2d	$$⊢\neg G\in \mathrm{V}\to N\circ \underset{\dot{}}{-}=N\circ \varnothing$$
22		reldmtng	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{toNrmGrp}$$
23	22	ovprc1	$$⊢\neg G\in \mathrm{V}\to G\mathrm{toNrmGrp}N=\varnothing$$
24	1 23	syl5eq	$$⊢\neg G\in \mathrm{V}\to T=\varnothing$$
25	24	fveq2d	$$⊢\neg G\in \mathrm{V}\to \mathrm{dist}\left(T\right)=\mathrm{dist}\left(\varnothing \right)$$
26	18 21 25	3eqtr4a	$$⊢\neg G\in \mathrm{V}\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(T\right)$$
27	26	adantr	$$⊢\left(\neg G\in \mathrm{V}\wedge N\in V\right)\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(T\right)$$
28	15 27	pm2.61ian	$$⊢N\in V\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(T\right)$$