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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
ressusp.2 ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
Assertion ressusp ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( 𝑊 ↾s 𝐴 ) ∈ UnifSp )

Proof

Step Hyp Ref Expression
1 ressusp.1 ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 ressusp.2 ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3 ressuss ⊢ ( 𝐴 ∈ 𝐽 → ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) ) = ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) )
4 3 3ad2ant3 ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) ) = ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) )
5 simp1 ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → 𝑊 ∈ UnifSp )
6 eqid ⊢ ( UnifSt ‘ 𝑊 ) = ( UnifSt ‘ 𝑊 )
7 1 6 2 isusp ⊢ ( 𝑊 ∈ UnifSp ↔ ( ( UnifSt ‘ 𝑊 ) ∈ ( UnifOn ‘ 𝐵 ) ∧ 𝐽 = ( unifTop ‘ ( UnifSt ‘ 𝑊 ) ) ) )
8 5 7 sylib ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( ( UnifSt ‘ 𝑊 ) ∈ ( UnifOn ‘ 𝐵 ) ∧ 𝐽 = ( unifTop ‘ ( UnifSt ‘ 𝑊 ) ) ) )
9 8 simpld ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( UnifSt ‘ 𝑊 ) ∈ ( UnifOn ‘ 𝐵 ) )
10 simp2 ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → 𝑊 ∈ TopSp )
11 1 2 istps ⊢ ( 𝑊 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
12 10 11 sylib ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
13 simp3 ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → 𝐴 ∈ 𝐽 )
14 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝐴 ∈ 𝐽 ) → 𝐴 ⊆ 𝐵 )
15 12 13 14 syl2anc ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → 𝐴 ⊆ 𝐵 )
16 trust ⊢ ( ( ( UnifSt ‘ 𝑊 ) ∈ ( UnifOn ‘ 𝐵 ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) )
17 9 15 16 syl2anc ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) )
18 4 17 eqeltrd ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) )
19 eqid ⊢ ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s 𝐴 )
20 19 1 ressbas2 ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) )
21 15 20 syl ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → 𝐴 = ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) )
22 21 fveq2d ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( UnifOn ‘ 𝐴 ) = ( UnifOn ‘ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) )
23 18 22 eleqtrd ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) ) ∈ ( UnifOn ‘ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) )
24 8 simprd ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → 𝐽 = ( unifTop ‘ ( UnifSt ‘ 𝑊 ) ) )
25 13 24 eleqtrd ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → 𝐴 ∈ ( unifTop ‘ ( UnifSt ‘ 𝑊 ) ) )
26 restutopopn ⊢ ( ( ( UnifSt ‘ 𝑊 ) ∈ ( UnifOn ‘ 𝐵 ) ∧ 𝐴 ∈ ( unifTop ‘ ( UnifSt ‘ 𝑊 ) ) ) → ( ( unifTop ‘ ( UnifSt ‘ 𝑊 ) ) ↾t 𝐴 ) = ( unifTop ‘ ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) ) )
27 9 25 26 syl2anc ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( ( unifTop ‘ ( UnifSt ‘ 𝑊 ) ) ↾t 𝐴 ) = ( unifTop ‘ ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) ) )
28 24 oveq1d ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( 𝐽 ↾t 𝐴 ) = ( ( unifTop ‘ ( UnifSt ‘ 𝑊 ) ) ↾t 𝐴 ) )
29 4 fveq2d ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( unifTop ‘ ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) ) ) = ( unifTop ‘ ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) ) )
30 27 28 29 3eqtr4d ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( 𝐽 ↾t 𝐴 ) = ( unifTop ‘ ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) ) ) )
31 eqid ⊢ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) = ( Base ‘ ( 𝑊 ↾s 𝐴 ) )
32 eqid ⊢ ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) ) = ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) )
33 19 2 resstopn ⊢ ( 𝐽 ↾t 𝐴 ) = ( TopOpen ‘ ( 𝑊 ↾s 𝐴 ) )
34 31 32 33 isusp ⊢ ( ( 𝑊 ↾s 𝐴 ) ∈ UnifSp ↔ ( ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) ) ∈ ( UnifOn ‘ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ ( 𝐽 ↾t 𝐴 ) = ( unifTop ‘ ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) ) ) ) )
35 23 30 34 sylanbrc ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽 ) → ( 𝑊 ↾s 𝐴 ) ∈ UnifSp )