Theorem resspwsds

Description: Restriction of a power metric. (Contributed by Mario Carneiro, 16-Sep-2015)

	Ref	Expression
Hypotheses	resspwsds.y	$$⊢\phi \to Y=R{\uparrow }_{𝑠}I$$
	resspwsds.h	$$⊢\phi \to H=\left(R{\upharpoonright }_{𝑠}A\right){\uparrow }_{𝑠}I$$
	resspwsds.b	$$⊢B={\mathrm{Base}}_H$$
	resspwsds.d	$$⊢D=\mathrm{dist}\left(Y\right)$$
	resspwsds.e	$$⊢E=\mathrm{dist}\left(H\right)$$
	resspwsds.i	$$⊢\phi \to I\in V$$
	resspwsds.r	$$⊢\phi \to R\in W$$
	resspwsds.a	$$⊢\phi \to A\in X$$
Assertion	resspwsds	$$⊢\phi \to E={D\upharpoonright }_{\left(B\times B\right)}$$

Proof

Step	Hyp	Ref	Expression
1		resspwsds.y	$$⊢\phi \to Y=R{\uparrow }_{𝑠}I$$
2		resspwsds.h	$$⊢\phi \to H=\left(R{\upharpoonright }_{𝑠}A\right){\uparrow }_{𝑠}I$$
3		resspwsds.b	$$⊢B={\mathrm{Base}}_H$$
4		resspwsds.d	$$⊢D=\mathrm{dist}\left(Y\right)$$
5		resspwsds.e	$$⊢E=\mathrm{dist}\left(H\right)$$
6		resspwsds.i	$$⊢\phi \to I\in V$$
7		resspwsds.r	$$⊢\phi \to R\in W$$
8		resspwsds.a	$$⊢\phi \to A\in X$$
9		eqid	$$⊢R{\uparrow }_{𝑠}I=R{\uparrow }_{𝑠}I$$
10		eqid	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(R\right)$$
11	9 10	pwsval	$$⊢\left(R\in W\wedge I\in V\right)\to R{\uparrow }_{𝑠}I=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$
12	7 6 11	syl2anc	$$⊢\phi \to R{\uparrow }_{𝑠}I=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$
13		fconstmpt	$$⊢I\times \left\{R\right\}=\left(x\in I⟼R\right)$$
14	13	oveq2i	$$⊢\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(x\in I⟼R\right)$$
15	12 14	syl6eq	$$⊢\phi \to R{\uparrow }_{𝑠}I=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(x\in I⟼R\right)$$
16	1 15	eqtrd	$$⊢\phi \to Y=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(x\in I⟼R\right)$$
17		ovex	$$⊢R{\upharpoonright }_{𝑠}A\in \mathrm{V}$$
18		eqid	$$⊢\left(R{\upharpoonright }_{𝑠}A\right){\uparrow }_{𝑠}I=\left(R{\upharpoonright }_{𝑠}A\right){\uparrow }_{𝑠}I$$
19		eqid	$$⊢\mathrm{Scalar}\left(R{\upharpoonright }_{𝑠}A\right)=\mathrm{Scalar}\left(R{\upharpoonright }_{𝑠}A\right)$$
20	18 19	pwsval	$$⊢\left(R{\upharpoonright }_{𝑠}A\in \mathrm{V}\wedge I\in V\right)\to \left(R{\upharpoonright }_{𝑠}A\right){\uparrow }_{𝑠}I=\mathrm{Scalar}\left(R{\upharpoonright }_{𝑠}A\right){⨉}_{𝑠}\left(I\times \left\{R{\upharpoonright }_{𝑠}A\right\}\right)$$
21	17 6 20	sylancr	$$⊢\phi \to \left(R{\upharpoonright }_{𝑠}A\right){\uparrow }_{𝑠}I=\mathrm{Scalar}\left(R{\upharpoonright }_{𝑠}A\right){⨉}_{𝑠}\left(I\times \left\{R{\upharpoonright }_{𝑠}A\right\}\right)$$
22		fconstmpt	$$⊢I\times \left\{R{\upharpoonright }_{𝑠}A\right\}=\left(x\in I⟼R{\upharpoonright }_{𝑠}A\right)$$
23	22	oveq2i	$$⊢\mathrm{Scalar}\left(R{\upharpoonright }_{𝑠}A\right){⨉}_{𝑠}\left(I\times \left\{R{\upharpoonright }_{𝑠}A\right\}\right)=\mathrm{Scalar}\left(R{\upharpoonright }_{𝑠}A\right){⨉}_{𝑠}\left(x\in I⟼R{\upharpoonright }_{𝑠}A\right)$$
24	21 23	syl6eq	$$⊢\phi \to \left(R{\upharpoonright }_{𝑠}A\right){\uparrow }_{𝑠}I=\mathrm{Scalar}\left(R{\upharpoonright }_{𝑠}A\right){⨉}_{𝑠}\left(x\in I⟼R{\upharpoonright }_{𝑠}A\right)$$
25	2 24	eqtrd	$$⊢\phi \to H=\mathrm{Scalar}\left(R{\upharpoonright }_{𝑠}A\right){⨉}_{𝑠}\left(x\in I⟼R{\upharpoonright }_{𝑠}A\right)$$
26		fvexd	$$⊢\phi \to \mathrm{Scalar}\left(R\right)\in \mathrm{V}$$
27		fvexd	$$⊢\phi \to \mathrm{Scalar}\left(R{\upharpoonright }_{𝑠}A\right)\in \mathrm{V}$$
28	7	adantr	$$⊢\left(\phi \wedge x\in I\right)\to R\in W$$
29	8	adantr	$$⊢\left(\phi \wedge x\in I\right)\to A\in X$$
30	16 25 3 4 5 26 27 6 28 29	ressprdsds	$$⊢\phi \to E={D\upharpoonright }_{\left(B\times B\right)}$$