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 e. UnifSp /\ W e. TopSp /\ A e. J ) -> ( W |`s A ) e. UnifSp )

Proof

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