Theorem xmspropd

Description: Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	xmspropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	xmspropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	xmspropd.3	$$⊢\phi \to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left(B\times B\right)}={\mathrm{dist}\left(L\right)\upharpoonright }_{\left(B\times B\right)}$$
	xmspropd.4	$$⊢\phi \to \mathrm{TopOpen}\left(K\right)=\mathrm{TopOpen}\left(L\right)$$
Assertion	xmspropd	$$⊢\phi \to \left(K\in \mathrm{\infty MetSp}\leftrightarrow L\in \mathrm{\infty MetSp}\right)$$

Proof

Step	Hyp	Ref	Expression
1		xmspropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		xmspropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		xmspropd.3	$$⊢\phi \to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left(B\times B\right)}={\mathrm{dist}\left(L\right)\upharpoonright }_{\left(B\times B\right)}$$
4		xmspropd.4	$$⊢\phi \to \mathrm{TopOpen}\left(K\right)=\mathrm{TopOpen}\left(L\right)$$
5	1 2	eqtr3d	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
6	5 4	tpspropd	$$⊢\phi \to \left(K\in \mathrm{TopSp}\leftrightarrow L\in \mathrm{TopSp}\right)$$
7	1	sqxpeqd	$$⊢\phi \to B\times B={\mathrm{Base}}_K\times {\mathrm{Base}}_K$$
8	7	reseq2d	$$⊢\phi \to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left(B\times B\right)}={\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}$$
9	3 8	eqtr3d	$$⊢\phi \to {\mathrm{dist}\left(L\right)\upharpoonright }_{\left(B\times B\right)}={\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}$$
10	2	sqxpeqd	$$⊢\phi \to B\times B={\mathrm{Base}}_L\times {\mathrm{Base}}_L$$
11	10	reseq2d	$$⊢\phi \to {\mathrm{dist}\left(L\right)\upharpoonright }_{\left(B\times B\right)}={\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}$$
12	9 11	eqtr3d	$$⊢\phi \to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}={\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}$$
13	12	fveq2d	$$⊢\phi \to \mathrm{MetOpen}\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}\right)$$
14	4 13	eqeq12d	$$⊢\phi \to \left(\mathrm{TopOpen}\left(K\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)\leftrightarrow \mathrm{TopOpen}\left(L\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}\right)\right)$$
15	6 14	anbi12d	$$⊢\phi \to \left(\left(K\in \mathrm{TopSp}\wedge \mathrm{TopOpen}\left(K\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)\right)\leftrightarrow \left(L\in \mathrm{TopSp}\wedge \mathrm{TopOpen}\left(L\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}\right)\right)\right)$$
16		eqid	$$⊢\mathrm{TopOpen}\left(K\right)=\mathrm{TopOpen}\left(K\right)$$
17		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
18		eqid	$$⊢{\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}={\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}$$
19	16 17 18	isxms	$$⊢K\in \mathrm{\infty MetSp}\leftrightarrow \left(K\in \mathrm{TopSp}\wedge \mathrm{TopOpen}\left(K\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)\right)$$
20		eqid	$$⊢\mathrm{TopOpen}\left(L\right)=\mathrm{TopOpen}\left(L\right)$$
21		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
22		eqid	$$⊢{\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}={\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}$$
23	20 21 22	isxms	$$⊢L\in \mathrm{\infty MetSp}\leftrightarrow \left(L\in \mathrm{TopSp}\wedge \mathrm{TopOpen}\left(L\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}\right)\right)$$
24	15 19 23	3bitr4g	$$⊢\phi \to \left(K\in \mathrm{\infty MetSp}\leftrightarrow L\in \mathrm{\infty MetSp}\right)$$