Theorem repwsmet

Description: The supremum metric on RR ^ I is a metric. (Contributed by Jeff Madsen, 15-Sep-2015)

	Ref	Expression
Hypotheses	rrnequiv.y	$$⊢Y=\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right){\uparrow }_{𝑠}I$$
	rrnequiv.d	$$⊢D=\mathrm{dist}\left(Y\right)$$
	rrnequiv.1	$$⊢X={ℝ}^I$$
Assertion	repwsmet	$$⊢I\in \mathrm{Fin}\to D\in \mathrm{Met}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrnequiv.y	$$⊢Y=\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right){\uparrow }_{𝑠}I$$
2		rrnequiv.d	$$⊢D=\mathrm{dist}\left(Y\right)$$
3		rrnequiv.1	$$⊢X={ℝ}^I$$
4		fconstmpt	$$⊢I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}=\left(k\in I⟼{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)$$
5	4	oveq2i	$$⊢\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)=\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(k\in I⟼{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)$$
6		eqid	$$⊢{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)\right)}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)\right)}$$
7		ax-resscn	$$⊢ℝ\subseteq ℂ$$
8		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
9		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
10	8 9	ressbas2	$$⊢ℝ\subseteq ℂ\to ℝ={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)}$$
11	7 10	ax-mp	$$⊢ℝ={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)}$$
12		reex	$$⊢ℝ\in \mathrm{V}$$
13		cnfldds	$$⊢\mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)$$
14	8 13	ressds	$$⊢ℝ\in \mathrm{V}\to \mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)$$
15	12 14	ax-mp	$$⊢\mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)$$
16	15	reseq1i	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)\upharpoonright }_{{ℝ}^2}$$
17		eqid	$$⊢\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)\right)=\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)\right)$$
18		fvexd	$$⊢I\in \mathrm{Fin}\to \mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{V}$$
19		id	$$⊢I\in \mathrm{Fin}\to I\in \mathrm{Fin}$$
20		ovex	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\in \mathrm{V}$$
21	20	a1i	$$⊢\left(I\in \mathrm{Fin}\wedge k\in I\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\in \mathrm{V}$$
22		eqid	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
23	22	remet	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{Met}\left(ℝ\right)$$
24	23	a1i	$$⊢\left(I\in \mathrm{Fin}\wedge k\in I\right)\to {\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{Met}\left(ℝ\right)$$
25	5 6 11 16 17 18 19 21 24	prdsmet	$$⊢I\in \mathrm{Fin}\to \mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)\right)\in \mathrm{Met}\left({\mathrm{Base}}_{\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)\right)}\right)$$
26		eqid	$$⊢\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right)$$
27	8 26	resssca	$$⊢ℝ\in \mathrm{V}\to \mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)$$
28	12 27	ax-mp	$$⊢\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)$$
29	1 28	pwsval	$$⊢\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\in \mathrm{V}\wedge I\in \mathrm{Fin}\right)\to Y=\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)$$
30	20 29	mpan	$$⊢I\in \mathrm{Fin}\to Y=\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)$$
31	30	fveq2d	$$⊢I\in \mathrm{Fin}\to \mathrm{dist}\left(Y\right)=\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)\right)$$
32	2 31	syl5eq	$$⊢I\in \mathrm{Fin}\to D=\mathrm{dist}\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)\right)$$
33	1 11	pwsbas	$$⊢\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\in \mathrm{V}\wedge I\in \mathrm{Fin}\right)\to {ℝ}^I={\mathrm{Base}}_Y$$
34	20 33	mpan	$$⊢I\in \mathrm{Fin}\to {ℝ}^I={\mathrm{Base}}_Y$$
35	30	fveq2d	$$⊢I\in \mathrm{Fin}\to {\mathrm{Base}}_Y={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)\right)}$$
36	34 35	eqtrd	$$⊢I\in \mathrm{Fin}\to {ℝ}^I={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)\right)}$$
37	3 36	syl5eq	$$⊢I\in \mathrm{Fin}\to X={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)\right)}$$
38	37	fveq2d	$$⊢I\in \mathrm{Fin}\to \mathrm{Met}\left(X\right)=\mathrm{Met}\left({\mathrm{Base}}_{\left(\mathrm{Scalar}\left({ℂ}_{\mathrm{fld}}\right){⨉}_{𝑠}\left(I\times \left\{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right\}\right)\right)}\right)$$
39	25 32 38	3eltr4d	$$⊢I\in \mathrm{Fin}\to D\in \mathrm{Met}\left(X\right)$$