Theorem ressuss

Description: Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017)

	Ref	Expression
Assertion	ressuss	$$⊢A\in V\to \mathrm{UnifSt}\left(W{\upharpoonright }_{𝑠}A\right)=\mathrm{UnifSt}\left(W\right){\upharpoonright }_{𝑡}\left(A\times A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
2		eqid	$$⊢\mathrm{UnifSet}\left(W\right)=\mathrm{UnifSet}\left(W\right)$$
3	1 2	ussval	$$⊢\mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)=\mathrm{UnifSt}\left(W\right)$$
4	3	oveq1i	$$⊢\left(\mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)\right){\upharpoonright }_{𝑡}\left(A\times A\right)=\mathrm{UnifSt}\left(W\right){\upharpoonright }_{𝑡}\left(A\times A\right)$$
5		fvex	$$⊢\mathrm{UnifSet}\left(W\right)\in \mathrm{V}$$
6		fvex	$$⊢{\mathrm{Base}}_W\in \mathrm{V}$$
7	6 6	xpex	$$⊢{\mathrm{Base}}_W\times {\mathrm{Base}}_W\in \mathrm{V}$$
8		sqxpexg	$$⊢A\in V\to A\times A\in \mathrm{V}$$
9		restco	$$⊢\left(\mathrm{UnifSet}\left(W\right)\in \mathrm{V}\wedge {\mathrm{Base}}_W\times {\mathrm{Base}}_W\in \mathrm{V}\wedge A\times A\in \mathrm{V}\right)\to \left(\mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)\right){\upharpoonright }_{𝑡}\left(A\times A\right)=\mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left(\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)\cap \left(A\times A\right)\right)$$
10	5 7 8 9	mp3an12i	$$⊢A\in V\to \left(\mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)\right){\upharpoonright }_{𝑡}\left(A\times A\right)=\mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left(\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)\cap \left(A\times A\right)\right)$$
11	4 10	eqtr3id	$$⊢A\in V\to \mathrm{UnifSt}\left(W\right){\upharpoonright }_{𝑡}\left(A\times A\right)=\mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left(\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)\cap \left(A\times A\right)\right)$$
12		inxp	$$⊢\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)\cap \left(A\times A\right)=\left({\mathrm{Base}}_W\cap A\right)\times \left({\mathrm{Base}}_W\cap A\right)$$
13		incom	$$⊢A\cap {\mathrm{Base}}_W={\mathrm{Base}}_W\cap A$$
14		eqid	$$⊢W{\upharpoonright }_{𝑠}A=W{\upharpoonright }_{𝑠}A$$
15	14 1	ressbas	$$⊢A\in V\to A\cap {\mathrm{Base}}_W={\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}$$
16	13 15	eqtr3id	$$⊢A\in V\to {\mathrm{Base}}_W\cap A={\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}$$
17	16	sqxpeqd	$$⊢A\in V\to \left({\mathrm{Base}}_W\cap A\right)\times \left({\mathrm{Base}}_W\cap A\right)={\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}$$
18	12 17	syl5eq	$$⊢A\in V\to \left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)\cap \left(A\times A\right)={\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}$$
19	18	oveq2d	$$⊢A\in V\to \mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left(\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)\cap \left(A\times A\right)\right)=\mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\right)$$
20	14 2	ressunif	$$⊢A\in V\to \mathrm{UnifSet}\left(W\right)=\mathrm{UnifSet}\left(W{\upharpoonright }_{𝑠}A\right)$$
21	20	oveq1d	$$⊢A\in V\to \mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\right)=\mathrm{UnifSet}\left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\right)$$
22		eqid	$$⊢{\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}={\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}$$
23		eqid	$$⊢\mathrm{UnifSet}\left(W{\upharpoonright }_{𝑠}A\right)=\mathrm{UnifSet}\left(W{\upharpoonright }_{𝑠}A\right)$$
24	22 23	ussval	$$⊢\mathrm{UnifSet}\left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\right)=\mathrm{UnifSt}\left(W{\upharpoonright }_{𝑠}A\right)$$
25	24	a1i	$$⊢A\in V\to \mathrm{UnifSet}\left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\right)=\mathrm{UnifSt}\left(W{\upharpoonright }_{𝑠}A\right)$$
26	19 21 25	3eqtrd	$$⊢A\in V\to \mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left(\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)\cap \left(A\times A\right)\right)=\mathrm{UnifSt}\left(W{\upharpoonright }_{𝑠}A\right)$$
27	11 26	eqtr2d	$$⊢A\in V\to \mathrm{UnifSt}\left(W{\upharpoonright }_{𝑠}A\right)=\mathrm{UnifSt}\left(W\right){\upharpoonright }_{𝑡}\left(A\times A\right)$$