Theorem tcphtopn

Description: The topology of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015)

	Ref	Expression
Hypotheses	tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
	tcphtopn.d	$$⊢D=\mathrm{dist}\left(G\right)$$
	tcphtopn.j	$$⊢J=\mathrm{TopOpen}\left(G\right)$$
Assertion	tcphtopn	$$⊢W\in V\to J=\mathrm{MetOpen}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
2		tcphtopn.d	$$⊢D=\mathrm{dist}\left(G\right)$$
3		tcphtopn.j	$$⊢J=\mathrm{TopOpen}\left(G\right)$$
4		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
5	4	tcphex	$$⊢\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)\in \mathrm{V}$$
6		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
7	1 4 6	tcphval	$$⊢G=W\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)$$
8		eqid	$$⊢\mathrm{MetOpen}\left(D\right)=\mathrm{MetOpen}\left(D\right)$$
9	7 2 8	tngtopn	$$⊢\left(W\in V\wedge \left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)\in \mathrm{V}\right)\to \mathrm{MetOpen}\left(D\right)=\mathrm{TopOpen}\left(G\right)$$
10	5 9	mpan2	$$⊢W\in V\to \mathrm{MetOpen}\left(D\right)=\mathrm{TopOpen}\left(G\right)$$
11	3 10	eqtr4id	$$⊢W\in V\to J=\mathrm{MetOpen}\left(D\right)$$