Theorem cmspropd

Description: Property deduction for a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	cmspropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	cmspropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	cmspropd.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)}$$
	cmspropd.4	$$⊢\phi \to \mathrm{TopOpen}\left(K\right)=\mathrm{TopOpen}\left(L\right)$$
Assertion	cmspropd	$$⊢\phi \to \left(K\in \mathrm{CMetSp}\leftrightarrow L\in \mathrm{CMetSp}\right)$$

Proof

Step	Hyp	Ref	Expression
1		cmspropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		cmspropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		cmspropd.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		cmspropd.4	$$⊢\phi \to \mathrm{TopOpen}\left(K\right)=\mathrm{TopOpen}\left(L\right)$$
5	1 2 3 4	mspropd	$$⊢\phi \to \left(K\in \mathrm{MetSp}\leftrightarrow L\in \mathrm{MetSp}\right)$$
6	1	sqxpeqd	$$⊢\phi \to B\times B={\mathrm{Base}}_K\times {\mathrm{Base}}_K$$
7	6	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)}$$
8	3 7	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)}$$
9	2	sqxpeqd	$$⊢\phi \to B\times B={\mathrm{Base}}_L\times {\mathrm{Base}}_L$$
10	9	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)}$$
11	8 10	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)}$$
12	1 2	eqtr3d	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
13	12	fveq2d	$$⊢\phi \to \mathrm{CMet}\left({\mathrm{Base}}_K\right)=\mathrm{CMet}\left({\mathrm{Base}}_L\right)$$
14	11 13	eleq12d	$$⊢\phi \to \left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\in \mathrm{CMet}\left({\mathrm{Base}}_K\right)\leftrightarrow {\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}\in \mathrm{CMet}\left({\mathrm{Base}}_L\right)\right)$$
15	5 14	anbi12d	$$⊢\phi \to \left(\left(K\in \mathrm{MetSp}\wedge {\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\in \mathrm{CMet}\left({\mathrm{Base}}_K\right)\right)\leftrightarrow \left(L\in \mathrm{MetSp}\wedge {\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}\in \mathrm{CMet}\left({\mathrm{Base}}_L\right)\right)\right)$$
16		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
17		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)}$$
18	16 17	iscms	$$⊢K\in \mathrm{CMetSp}\leftrightarrow \left(K\in \mathrm{MetSp}\wedge {\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\in \mathrm{CMet}\left({\mathrm{Base}}_K\right)\right)$$
19		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
20		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)}$$
21	19 20	iscms	$$⊢L\in \mathrm{CMetSp}\leftrightarrow \left(L\in \mathrm{MetSp}\wedge {\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}\in \mathrm{CMet}\left({\mathrm{Base}}_L\right)\right)$$
22	15 18 21	3bitr4g	$$⊢\phi \to \left(K\in \mathrm{CMetSp}\leftrightarrow L\in \mathrm{CMetSp}\right)$$