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