Theorem prdsmslem1

Description: Lemma for prdsms . The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypotheses	prdsxms.y	$$⊢Y=S{⨉}_{𝑠}R$$
	prdsxms.s	$$⊢\phi \to S\in W$$
	prdsxms.i	$$⊢\phi \to I\in \mathrm{Fin}$$
	prdsxms.d	$$⊢D=\mathrm{dist}\left(Y\right)$$
	prdsxms.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsms.r	$$⊢\phi \to R:I⟶\mathrm{MetSp}$$
Assertion	prdsmslem1	$$⊢\phi \to D\in \mathrm{Met}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		prdsxms.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsxms.s	$$⊢\phi \to S\in W$$
3		prdsxms.i	$$⊢\phi \to I\in \mathrm{Fin}$$
4		prdsxms.d	$$⊢D=\mathrm{dist}\left(Y\right)$$
5		prdsxms.b	$$⊢B={\mathrm{Base}}_Y$$
6		prdsms.r	$$⊢\phi \to R:I⟶\mathrm{MetSp}$$
7		eqid	$$⊢S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)=S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)$$
8		eqid	$$⊢{\mathrm{Base}}_{\left(S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)\right)}={\mathrm{Base}}_{\left(S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)\right)}$$
9		eqid	$$⊢{\mathrm{Base}}_{R\left(k\right)}={\mathrm{Base}}_{R\left(k\right)}$$
10		eqid	$$⊢{\mathrm{dist}\left(R\left(k\right)\right)\upharpoonright }_{\left({\mathrm{Base}}_{R\left(k\right)}\times {\mathrm{Base}}_{R\left(k\right)}\right)}={\mathrm{dist}\left(R\left(k\right)\right)\upharpoonright }_{\left({\mathrm{Base}}_{R\left(k\right)}\times {\mathrm{Base}}_{R\left(k\right)}\right)}$$
11		eqid	$$⊢\mathrm{dist}\left(S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)\right)=\mathrm{dist}\left(S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)\right)$$
12	6	ffvelrnda	$$⊢\left(\phi \wedge k\in I\right)\to R\left(k\right)\in \mathrm{MetSp}$$
13	9 10	msmet	$$⊢R\left(k\right)\in \mathrm{MetSp}\to {\mathrm{dist}\left(R\left(k\right)\right)\upharpoonright }_{\left({\mathrm{Base}}_{R\left(k\right)}\times {\mathrm{Base}}_{R\left(k\right)}\right)}\in \mathrm{Met}\left({\mathrm{Base}}_{R\left(k\right)}\right)$$
14	12 13	syl	$$⊢\left(\phi \wedge k\in I\right)\to {\mathrm{dist}\left(R\left(k\right)\right)\upharpoonright }_{\left({\mathrm{Base}}_{R\left(k\right)}\times {\mathrm{Base}}_{R\left(k\right)}\right)}\in \mathrm{Met}\left({\mathrm{Base}}_{R\left(k\right)}\right)$$
15	7 8 9 10 11 2 3 12 14	prdsmet	$$⊢\phi \to \mathrm{dist}\left(S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)\right)\in \mathrm{Met}\left({\mathrm{Base}}_{\left(S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)\right)}\right)$$
16	6	feqmptd	$$⊢\phi \to R=\left(k\in I⟼R\left(k\right)\right)$$
17	16	oveq2d	$$⊢\phi \to S{⨉}_{𝑠}R=S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)$$
18	1 17	syl5eq	$$⊢\phi \to Y=S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)$$
19	18	fveq2d	$$⊢\phi \to \mathrm{dist}\left(Y\right)=\mathrm{dist}\left(S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)\right)$$
20	4 19	syl5eq	$$⊢\phi \to D=\mathrm{dist}\left(S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)\right)$$
21	18	fveq2d	$$⊢\phi \to {\mathrm{Base}}_Y={\mathrm{Base}}_{\left(S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)\right)}$$
22	5 21	syl5eq	$$⊢\phi \to B={\mathrm{Base}}_{\left(S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)\right)}$$
23	22	fveq2d	$$⊢\phi \to \mathrm{Met}\left(B\right)=\mathrm{Met}\left({\mathrm{Base}}_{\left(S{⨉}_{𝑠}\left(k\in I⟼R\left(k\right)\right)\right)}\right)$$
24	15 20 23	3eltr4d	$$⊢\phi \to D\in \mathrm{Met}\left(B\right)$$