Metamath Proof Explorer


Theorem ressuss

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

Ref Expression
Assertion ressuss A V UnifSt W 𝑠 A = UnifSt W 𝑡 A × A

Proof

Step Hyp Ref Expression
1 eqid Base W = Base W
2 eqid UnifSet W = UnifSet W
3 1 2 ussval UnifSet W 𝑡 Base W × Base W = UnifSt W
4 3 oveq1i UnifSet W 𝑡 Base W × Base W 𝑡 A × A = UnifSt W 𝑡 A × A
5 fvex UnifSet W V
6 fvex Base W V
7 6 6 xpex Base W × Base W V
8 sqxpexg A V A × A V
9 restco UnifSet W V Base W × Base W V A × A V UnifSet W 𝑡 Base W × Base W 𝑡 A × A = UnifSet W 𝑡 Base W × Base W A × A
10 5 7 8 9 mp3an12i A V UnifSet W 𝑡 Base W × Base W 𝑡 A × A = UnifSet W 𝑡 Base W × Base W A × A
11 4 10 eqtr3id A V UnifSt W 𝑡 A × A = UnifSet W 𝑡 Base W × Base W A × A
12 inxp Base W × Base W A × A = Base W A × Base W A
13 incom A Base W = Base W A
14 eqid W 𝑠 A = W 𝑠 A
15 14 1 ressbas A V A Base W = Base W 𝑠 A
16 13 15 eqtr3id A V Base W A = Base W 𝑠 A
17 16 sqxpeqd A V Base W A × Base W A = Base W 𝑠 A × Base W 𝑠 A
18 12 17 syl5eq A V Base W × Base W A × A = Base W 𝑠 A × Base W 𝑠 A
19 18 oveq2d A V UnifSet W 𝑡 Base W × Base W A × A = UnifSet W 𝑡 Base W 𝑠 A × Base W 𝑠 A
20 14 2 ressunif A V UnifSet W = UnifSet W 𝑠 A
21 20 oveq1d A V UnifSet W 𝑡 Base W 𝑠 A × Base W 𝑠 A = UnifSet W 𝑠 A 𝑡 Base W 𝑠 A × Base W 𝑠 A
22 eqid Base W 𝑠 A = Base W 𝑠 A
23 eqid UnifSet W 𝑠 A = UnifSet W 𝑠 A
24 22 23 ussval UnifSet W 𝑠 A 𝑡 Base W 𝑠 A × Base W 𝑠 A = UnifSt W 𝑠 A
25 24 a1i A V UnifSet W 𝑠 A 𝑡 Base W 𝑠 A × Base W 𝑠 A = UnifSt W 𝑠 A
26 19 21 25 3eqtrd A V UnifSet W 𝑡 Base W × Base W A × A = UnifSt W 𝑠 A
27 11 26 eqtr2d A V UnifSt W 𝑠 A = UnifSt W 𝑡 A × A