Theorem prdsxmet

Description: The product metric is an extended metric. Eliminate disjoint variable conditions from prdsxmetlem . (Contributed by Mario Carneiro, 26-Sep-2015)

	Ref	Expression
Hypotheses	prdsdsf.y	$$⊢Y=S{⨉}_{𝑠}\left(x\in I⟼R\right)$$
	prdsdsf.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsdsf.v	$$⊢V={\mathrm{Base}}_R$$
	prdsdsf.e	$$⊢E={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(V\times V\right)}$$
	prdsdsf.d	$$⊢D=\mathrm{dist}\left(Y\right)$$
	prdsdsf.s	$$⊢\phi \to S\in W$$
	prdsdsf.i	$$⊢\phi \to I\in X$$
	prdsdsf.r	$$⊢\left(\phi \wedge x\in I\right)\to R\in Z$$
	prdsdsf.m	$$⊢\left(\phi \wedge x\in I\right)\to E\in \mathrm{\infty Met}\left(V\right)$$
Assertion	prdsxmet	$$⊢\phi \to D\in \mathrm{\infty Met}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		prdsdsf.y	$$⊢Y=S{⨉}_{𝑠}\left(x\in I⟼R\right)$$
2		prdsdsf.b	$$⊢B={\mathrm{Base}}_Y$$
3		prdsdsf.v	$$⊢V={\mathrm{Base}}_R$$
4		prdsdsf.e	$$⊢E={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(V\times V\right)}$$
5		prdsdsf.d	$$⊢D=\mathrm{dist}\left(Y\right)$$
6		prdsdsf.s	$$⊢\phi \to S\in W$$
7		prdsdsf.i	$$⊢\phi \to I\in X$$
8		prdsdsf.r	$$⊢\left(\phi \wedge x\in I\right)\to R\in Z$$
9		prdsdsf.m	$$⊢\left(\phi \wedge x\in I\right)\to E\in \mathrm{\infty Met}\left(V\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}yR$$
11		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌R$$
12		csbeq1a	$$⊢x=y\to R=⦋y/x⦌R$$
13	10 11 12	cbvmpt	$$⊢\left(x\in I⟼R\right)=\left(y\in I⟼⦋y/x⦌R\right)$$
14	13	oveq2i	$$⊢S{⨉}_{𝑠}\left(x\in I⟼R\right)=S{⨉}_{𝑠}\left(y\in I⟼⦋y/x⦌R\right)$$
15	1 14	eqtri	$$⊢Y=S{⨉}_{𝑠}\left(y\in I⟼⦋y/x⦌R\right)$$
16		eqid	$$⊢{\mathrm{Base}}_{⦋y/x⦌R}={\mathrm{Base}}_{⦋y/x⦌R}$$
17		eqid	$$⊢{\mathrm{dist}\left(⦋y/x⦌R\right)\upharpoonright }_{\left({\mathrm{Base}}_{⦋y/x⦌R}\times {\mathrm{Base}}_{⦋y/x⦌R}\right)}={\mathrm{dist}\left(⦋y/x⦌R\right)\upharpoonright }_{\left({\mathrm{Base}}_{⦋y/x⦌R}\times {\mathrm{Base}}_{⦋y/x⦌R}\right)}$$
18	8	elexd	$$⊢\left(\phi \wedge x\in I\right)\to R\in \mathrm{V}$$
19	18	ralrimiva	$$⊢\phi \to \forall x\in IR\in \mathrm{V}$$
20	11	nfel1	$$⊢Ⅎx⦋y/x⦌R\in \mathrm{V}$$
21	12	eleq1d	$$⊢x=y\to \left(R\in \mathrm{V}\leftrightarrow ⦋y/x⦌R\in \mathrm{V}\right)$$
22	20 21	rspc	$$⊢y\in I\to \left(\forall x\in IR\in \mathrm{V}\to ⦋y/x⦌R\in \mathrm{V}\right)$$
23	19 22	mpan9	$$⊢\left(\phi \wedge y\in I\right)\to ⦋y/x⦌R\in \mathrm{V}$$
24	9	ralrimiva	$$⊢\phi \to \forall x\in IE\in \mathrm{\infty Met}\left(V\right)$$
25		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{dist}$$
26	25 11	nffv	$$⊢\underset{\_}{Ⅎ}x\mathrm{dist}\left(⦋y/x⦌R\right)$$
27		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{Base}$$
28	27 11	nffv	$$⊢\underset{\_}{Ⅎ}x{\mathrm{Base}}_{⦋y/x⦌R}$$
29	28 28	nfxp	$$⊢\underset{\_}{Ⅎ}x\left({\mathrm{Base}}_{⦋y/x⦌R}\times {\mathrm{Base}}_{⦋y/x⦌R}\right)$$
30	26 29	nfres	$$⊢\underset{\_}{Ⅎ}x\left({\mathrm{dist}\left(⦋y/x⦌R\right)\upharpoonright }_{\left({\mathrm{Base}}_{⦋y/x⦌R}\times {\mathrm{Base}}_{⦋y/x⦌R}\right)}\right)$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{\infty Met}$$
32	31 28	nffv	$$⊢\underset{\_}{Ⅎ}x\mathrm{\infty Met}\left({\mathrm{Base}}_{⦋y/x⦌R}\right)$$
33	30 32	nfel	$$⊢Ⅎx{\mathrm{dist}\left(⦋y/x⦌R\right)\upharpoonright }_{\left({\mathrm{Base}}_{⦋y/x⦌R}\times {\mathrm{Base}}_{⦋y/x⦌R}\right)}\in \mathrm{\infty Met}\left({\mathrm{Base}}_{⦋y/x⦌R}\right)$$
34	12	fveq2d	$$⊢x=y\to \mathrm{dist}\left(R\right)=\mathrm{dist}\left(⦋y/x⦌R\right)$$
35	12	fveq2d	$$⊢x=y\to {\mathrm{Base}}_R={\mathrm{Base}}_{⦋y/x⦌R}$$
36	3 35	syl5eq	$$⊢x=y\to V={\mathrm{Base}}_{⦋y/x⦌R}$$
37	36	sqxpeqd	$$⊢x=y\to V\times V={\mathrm{Base}}_{⦋y/x⦌R}\times {\mathrm{Base}}_{⦋y/x⦌R}$$
38	34 37	reseq12d	$$⊢x=y\to {\mathrm{dist}\left(R\right)\upharpoonright }_{\left(V\times V\right)}={\mathrm{dist}\left(⦋y/x⦌R\right)\upharpoonright }_{\left({\mathrm{Base}}_{⦋y/x⦌R}\times {\mathrm{Base}}_{⦋y/x⦌R}\right)}$$
39	4 38	syl5eq	$$⊢x=y\to E={\mathrm{dist}\left(⦋y/x⦌R\right)\upharpoonright }_{\left({\mathrm{Base}}_{⦋y/x⦌R}\times {\mathrm{Base}}_{⦋y/x⦌R}\right)}$$
40	36	fveq2d	$$⊢x=y\to \mathrm{\infty Met}\left(V\right)=\mathrm{\infty Met}\left({\mathrm{Base}}_{⦋y/x⦌R}\right)$$
41	39 40	eleq12d	$$⊢x=y\to \left(E\in \mathrm{\infty Met}\left(V\right)\leftrightarrow {\mathrm{dist}\left(⦋y/x⦌R\right)\upharpoonright }_{\left({\mathrm{Base}}_{⦋y/x⦌R}\times {\mathrm{Base}}_{⦋y/x⦌R}\right)}\in \mathrm{\infty Met}\left({\mathrm{Base}}_{⦋y/x⦌R}\right)\right)$$
42	33 41	rspc	$$⊢y\in I\to \left(\forall x\in IE\in \mathrm{\infty Met}\left(V\right)\to {\mathrm{dist}\left(⦋y/x⦌R\right)\upharpoonright }_{\left({\mathrm{Base}}_{⦋y/x⦌R}\times {\mathrm{Base}}_{⦋y/x⦌R}\right)}\in \mathrm{\infty Met}\left({\mathrm{Base}}_{⦋y/x⦌R}\right)\right)$$
43	24 42	mpan9	$$⊢\left(\phi \wedge y\in I\right)\to {\mathrm{dist}\left(⦋y/x⦌R\right)\upharpoonright }_{\left({\mathrm{Base}}_{⦋y/x⦌R}\times {\mathrm{Base}}_{⦋y/x⦌R}\right)}\in \mathrm{\infty Met}\left({\mathrm{Base}}_{⦋y/x⦌R}\right)$$
44	15 2 16 17 5 6 7 23 43	prdsxmetlem	$$⊢\phi \to D\in \mathrm{\infty Met}\left(B\right)$$