Metamath Proof Explorer


Theorem ressusp

Description: The restriction of a uniform topological space to an open set is a uniform space. (Contributed by Thierry Arnoux, 16-Dec-2017)

Ref Expression
Hypotheses ressusp.1 B = Base W
ressusp.2 J = TopOpen W
Assertion ressusp W UnifSp W TopSp A J W 𝑠 A UnifSp

Proof

Step Hyp Ref Expression
1 ressusp.1 B = Base W
2 ressusp.2 J = TopOpen W
3 ressuss A J UnifSt W 𝑠 A = UnifSt W 𝑡 A × A
4 3 3ad2ant3 W UnifSp W TopSp A J UnifSt W 𝑠 A = UnifSt W 𝑡 A × A
5 simp1 W UnifSp W TopSp A J W UnifSp
6 eqid UnifSt W = UnifSt W
7 1 6 2 isusp W UnifSp UnifSt W UnifOn B J = unifTop UnifSt W
8 5 7 sylib W UnifSp W TopSp A J UnifSt W UnifOn B J = unifTop UnifSt W
9 8 simpld W UnifSp W TopSp A J UnifSt W UnifOn B
10 simp2 W UnifSp W TopSp A J W TopSp
11 1 2 istps W TopSp J TopOn B
12 10 11 sylib W UnifSp W TopSp A J J TopOn B
13 simp3 W UnifSp W TopSp A J A J
14 toponss J TopOn B A J A B
15 12 13 14 syl2anc W UnifSp W TopSp A J A B
16 trust UnifSt W UnifOn B A B UnifSt W 𝑡 A × A UnifOn A
17 9 15 16 syl2anc W UnifSp W TopSp A J UnifSt W 𝑡 A × A UnifOn A
18 4 17 eqeltrd W UnifSp W TopSp A J UnifSt W 𝑠 A UnifOn A
19 eqid W 𝑠 A = W 𝑠 A
20 19 1 ressbas2 A B A = Base W 𝑠 A
21 15 20 syl W UnifSp W TopSp A J A = Base W 𝑠 A
22 21 fveq2d W UnifSp W TopSp A J UnifOn A = UnifOn Base W 𝑠 A
23 18 22 eleqtrd W UnifSp W TopSp A J UnifSt W 𝑠 A UnifOn Base W 𝑠 A
24 8 simprd W UnifSp W TopSp A J J = unifTop UnifSt W
25 13 24 eleqtrd W UnifSp W TopSp A J A unifTop UnifSt W
26 restutopopn UnifSt W UnifOn B A unifTop UnifSt W unifTop UnifSt W 𝑡 A = unifTop UnifSt W 𝑡 A × A
27 9 25 26 syl2anc W UnifSp W TopSp A J unifTop UnifSt W 𝑡 A = unifTop UnifSt W 𝑡 A × A
28 24 oveq1d W UnifSp W TopSp A J J 𝑡 A = unifTop UnifSt W 𝑡 A
29 4 fveq2d W UnifSp W TopSp A J unifTop UnifSt W 𝑠 A = unifTop UnifSt W 𝑡 A × A
30 27 28 29 3eqtr4d W UnifSp W TopSp A J J 𝑡 A = unifTop UnifSt W 𝑠 A
31 eqid Base W 𝑠 A = Base W 𝑠 A
32 eqid UnifSt W 𝑠 A = UnifSt W 𝑠 A
33 19 2 resstopn J 𝑡 A = TopOpen W 𝑠 A
34 31 32 33 isusp W 𝑠 A UnifSp UnifSt W 𝑠 A UnifOn Base W 𝑠 A J 𝑡 A = unifTop UnifSt W 𝑠 A
35 23 30 34 sylanbrc W UnifSp W TopSp A J W 𝑠 A UnifSp