Theorem prdsdsval3

Description: Value of the metric in a structure product. (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	prdsbasmpt2.y	$$⊢Y=S{⨉}_{𝑠}\left(x\in I⟼R\right)$$
	prdsbasmpt2.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsbasmpt2.s	$$⊢\phi \to S\in V$$
	prdsbasmpt2.i	$$⊢\phi \to I\in W$$
	prdsbasmpt2.r	$$⊢\phi \to \forall x\in IR\in X$$
	prdsdsval2.f	$$⊢\phi \to F\in B$$
	prdsdsval2.g	$$⊢\phi \to G\in B$$
	prdsdsval3.k	$$⊢K={\mathrm{Base}}_R$$
	prdsdsval3.e	$$⊢E={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(K\times K\right)}$$
	prdsdsval3.d	$$⊢D=\mathrm{dist}\left(Y\right)$$
Assertion	prdsdsval3	$$⊢\phi \to FDG=sup\left(\mathrm{ran}\left(x\in I⟼F\left(x\right)EG\left(x\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt2.y	$$⊢Y=S{⨉}_{𝑠}\left(x\in I⟼R\right)$$
2		prdsbasmpt2.b	$$⊢B={\mathrm{Base}}_Y$$
3		prdsbasmpt2.s	$$⊢\phi \to S\in V$$
4		prdsbasmpt2.i	$$⊢\phi \to I\in W$$
5		prdsbasmpt2.r	$$⊢\phi \to \forall x\in IR\in X$$
6		prdsdsval2.f	$$⊢\phi \to F\in B$$
7		prdsdsval2.g	$$⊢\phi \to G\in B$$
8		prdsdsval3.k	$$⊢K={\mathrm{Base}}_R$$
9		prdsdsval3.e	$$⊢E={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(K\times K\right)}$$
10		prdsdsval3.d	$$⊢D=\mathrm{dist}\left(Y\right)$$
11		eqid	$$⊢\mathrm{dist}\left(R\right)=\mathrm{dist}\left(R\right)$$
12	1 2 3 4 5 6 7 11 10	prdsdsval2	$$⊢\phi \to FDG=sup\left(\mathrm{ran}\left(x\in I⟼F\left(x\right)\mathrm{dist}\left(R\right)G\left(x\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)$$
13		eqidd	$$⊢\phi \to I=I$$
14	1 2 3 4 5 8 6	prdsbascl	$$⊢\phi \to \forall x\in IF\left(x\right)\in K$$
15	1 2 3 4 5 8 7	prdsbascl	$$⊢\phi \to \forall x\in IG\left(x\right)\in K$$
16	9	oveqi	$$⊢F\left(x\right)EG\left(x\right)=F\left(x\right)\left({\mathrm{dist}\left(R\right)\upharpoonright }_{\left(K\times K\right)}\right)G\left(x\right)$$
17		ovres	$$⊢\left(F\left(x\right)\in K\wedge G\left(x\right)\in K\right)\to F\left(x\right)\left({\mathrm{dist}\left(R\right)\upharpoonright }_{\left(K\times K\right)}\right)G\left(x\right)=F\left(x\right)\mathrm{dist}\left(R\right)G\left(x\right)$$
18	16 17	eqtrid	$$⊢\left(F\left(x\right)\in K\wedge G\left(x\right)\in K\right)\to F\left(x\right)EG\left(x\right)=F\left(x\right)\mathrm{dist}\left(R\right)G\left(x\right)$$
19	18	ex	$$⊢F\left(x\right)\in K\to \left(G\left(x\right)\in K\to F\left(x\right)EG\left(x\right)=F\left(x\right)\mathrm{dist}\left(R\right)G\left(x\right)\right)$$
20	19	ral2imi	$$⊢\forall x\in IF\left(x\right)\in K\to \left(\forall x\in IG\left(x\right)\in K\to \forall x\in IF\left(x\right)EG\left(x\right)=F\left(x\right)\mathrm{dist}\left(R\right)G\left(x\right)\right)$$
21	14 15 20	sylc	$$⊢\phi \to \forall x\in IF\left(x\right)EG\left(x\right)=F\left(x\right)\mathrm{dist}\left(R\right)G\left(x\right)$$
22		mpteq12	$$⊢\left(I=I\wedge \forall x\in IF\left(x\right)EG\left(x\right)=F\left(x\right)\mathrm{dist}\left(R\right)G\left(x\right)\right)\to \left(x\in I⟼F\left(x\right)EG\left(x\right)\right)=\left(x\in I⟼F\left(x\right)\mathrm{dist}\left(R\right)G\left(x\right)\right)$$
23	13 21 22	syl2anc	$$⊢\phi \to \left(x\in I⟼F\left(x\right)EG\left(x\right)\right)=\left(x\in I⟼F\left(x\right)\mathrm{dist}\left(R\right)G\left(x\right)\right)$$
24	23	rneqd	$$⊢\phi \to \mathrm{ran}\left(x\in I⟼F\left(x\right)EG\left(x\right)\right)=\mathrm{ran}\left(x\in I⟼F\left(x\right)\mathrm{dist}\left(R\right)G\left(x\right)\right)$$
25	24	uneq1d	$$⊢\phi \to \mathrm{ran}\left(x\in I⟼F\left(x\right)EG\left(x\right)\right)\cup \left\{0\right\}=\mathrm{ran}\left(x\in I⟼F\left(x\right)\mathrm{dist}\left(R\right)G\left(x\right)\right)\cup \left\{0\right\}$$
26	25	supeq1d	$$⊢\phi \to sup\left(\mathrm{ran}\left(x\in I⟼F\left(x\right)EG\left(x\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left(x\in I⟼F\left(x\right)\mathrm{dist}\left(R\right)G\left(x\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)$$
27	12 26	eqtr4d	$$⊢\phi \to FDG=sup\left(\mathrm{ran}\left(x\in I⟼F\left(x\right)EG\left(x\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)$$