Metamath Proof Explorer

Theorem ressxms

Description: The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion ressxms ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( 𝐾 β†Ύs 𝐴 ) ∈ ∞MetSp )

Proof

Step Hyp Ref Expression
1 eqid ⊒ ( Base β€˜ 𝐾 ) = ( Base β€˜ 𝐾 )
2 eqid ⊒ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) = ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) )
3 1 2 xmsxmet ⊒ ( 𝐾 ∈ ∞MetSp β†’ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ∈ ( ∞Met β€˜ ( Base β€˜ 𝐾 ) ) )
4 3 adantr ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ∈ ( ∞Met β€˜ ( Base β€˜ 𝐾 ) ) )
5 xmetres ⊒ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ∈ ( ∞Met β€˜ ( Base β€˜ 𝐾 ) ) β†’ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) ∈ ( ∞Met β€˜ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) )
6 4 5 syl ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) ∈ ( ∞Met β€˜ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) )
7 resres ⊒ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) = ( ( dist β€˜ 𝐾 ) β†Ύ ( ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ∩ ( 𝐴 Γ— 𝐴 ) ) )
8 inxp ⊒ ( ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ∩ ( 𝐴 Γ— 𝐴 ) ) = ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) )
9 8 reseq2i ⊒ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ∩ ( 𝐴 Γ— 𝐴 ) ) ) = ( ( dist β€˜ 𝐾 ) β†Ύ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) )
10 7 9 eqtri ⊒ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) = ( ( dist β€˜ 𝐾 ) β†Ύ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) )
11 eqid ⊒ ( 𝐾 β†Ύs 𝐴 ) = ( 𝐾 β†Ύs 𝐴 )
12 eqid ⊒ ( dist β€˜ 𝐾 ) = ( dist β€˜ 𝐾 )
13 11 12 ressds ⊒ ( 𝐴 ∈ 𝑉 β†’ ( dist β€˜ 𝐾 ) = ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) )
14 13 adantl ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( dist β€˜ 𝐾 ) = ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) )
15 incom ⊒ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( Base β€˜ 𝐾 ) )
16 11 1 ressbas ⊒ ( 𝐴 ∈ 𝑉 β†’ ( 𝐴 ∩ ( Base β€˜ 𝐾 ) ) = ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) )
17 16 adantl ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( 𝐴 ∩ ( Base β€˜ 𝐾 ) ) = ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) )
18 15 17 eqtrid ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) = ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) )
19 18 sqxpeqd ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) = ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) )
20 14 19 reseq12d ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) ) = ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) )
21 10 20 eqtrid ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) = ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) )
22 18 fveq2d ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ∞Met β€˜ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) = ( ∞Met β€˜ ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) )
23 6 21 22 3eltr3d ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) ∈ ( ∞Met β€˜ ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) )
24 eqid ⊒ ( TopOpen β€˜ 𝐾 ) = ( TopOpen β€˜ 𝐾 )
25 24 1 2 xmstopn ⊒ ( 𝐾 ∈ ∞MetSp β†’ ( TopOpen β€˜ 𝐾 ) = ( MetOpen β€˜ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ) )
26 25 adantr ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( TopOpen β€˜ 𝐾 ) = ( MetOpen β€˜ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ) )
27 26 oveq1d ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( TopOpen β€˜ 𝐾 ) β†Ύt ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) = ( ( MetOpen β€˜ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ) β†Ύt ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) )
28 inss1 ⊒ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) βŠ† ( Base β€˜ 𝐾 )
29 xpss12 ⊒ ( ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) βŠ† ( Base β€˜ 𝐾 ) ∧ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) βŠ† ( Base β€˜ 𝐾 ) ) β†’ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) βŠ† ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) )
30 28 28 29 mp2an ⊒ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) βŠ† ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) )
31 resabs1 ⊒ ( ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) βŠ† ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) β†’ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) ) = ( ( dist β€˜ 𝐾 ) β†Ύ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) ) )
32 30 31 ax-mp ⊒ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) ) = ( ( dist β€˜ 𝐾 ) β†Ύ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) )
33 10 32 eqtr4i ⊒ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) = ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) )
34 eqid ⊒ ( MetOpen β€˜ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ) = ( MetOpen β€˜ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) )
35 eqid ⊒ ( MetOpen β€˜ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) ) = ( MetOpen β€˜ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) )
36 33 34 35 metrest ⊒ ( ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ∈ ( ∞Met β€˜ ( Base β€˜ 𝐾 ) ) ∧ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) βŠ† ( Base β€˜ 𝐾 ) ) β†’ ( ( MetOpen β€˜ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ) β†Ύt ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) = ( MetOpen β€˜ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) ) )
37 4 28 36 sylancl ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( MetOpen β€˜ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ) β†Ύt ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) = ( MetOpen β€˜ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) ) )
38 27 37 eqtrd ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( TopOpen β€˜ 𝐾 ) β†Ύt ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) = ( MetOpen β€˜ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) ) )
39 xmstps ⊒ ( 𝐾 ∈ ∞MetSp β†’ 𝐾 ∈ TopSp )
40 1 24 tpsuni ⊒ ( 𝐾 ∈ TopSp β†’ ( Base β€˜ 𝐾 ) = βˆͺ ( TopOpen β€˜ 𝐾 ) )
41 39 40 syl ⊒ ( 𝐾 ∈ ∞MetSp β†’ ( Base β€˜ 𝐾 ) = βˆͺ ( TopOpen β€˜ 𝐾 ) )
42 41 adantr ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( Base β€˜ 𝐾 ) = βˆͺ ( TopOpen β€˜ 𝐾 ) )
43 42 ineq2d ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( 𝐴 ∩ ( Base β€˜ 𝐾 ) ) = ( 𝐴 ∩ βˆͺ ( TopOpen β€˜ 𝐾 ) ) )
44 15 43 eqtrid ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) = ( 𝐴 ∩ βˆͺ ( TopOpen β€˜ 𝐾 ) ) )
45 44 oveq2d ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( TopOpen β€˜ 𝐾 ) β†Ύt ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) = ( ( TopOpen β€˜ 𝐾 ) β†Ύt ( 𝐴 ∩ βˆͺ ( TopOpen β€˜ 𝐾 ) ) ) )
46 1 24 istps ⊒ ( 𝐾 ∈ TopSp ↔ ( TopOpen β€˜ 𝐾 ) ∈ ( TopOn β€˜ ( Base β€˜ 𝐾 ) ) )
47 39 46 sylib ⊒ ( 𝐾 ∈ ∞MetSp β†’ ( TopOpen β€˜ 𝐾 ) ∈ ( TopOn β€˜ ( Base β€˜ 𝐾 ) ) )
48 eqid ⊒ βˆͺ ( TopOpen β€˜ 𝐾 ) = βˆͺ ( TopOpen β€˜ 𝐾 )
49 48 restin ⊒ ( ( ( TopOpen β€˜ 𝐾 ) ∈ ( TopOn β€˜ ( Base β€˜ 𝐾 ) ) ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( TopOpen β€˜ 𝐾 ) β†Ύt 𝐴 ) = ( ( TopOpen β€˜ 𝐾 ) β†Ύt ( 𝐴 ∩ βˆͺ ( TopOpen β€˜ 𝐾 ) ) ) )
50 47 49 sylan ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( TopOpen β€˜ 𝐾 ) β†Ύt 𝐴 ) = ( ( TopOpen β€˜ 𝐾 ) β†Ύt ( 𝐴 ∩ βˆͺ ( TopOpen β€˜ 𝐾 ) ) ) )
51 45 50 eqtr4d ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( TopOpen β€˜ 𝐾 ) β†Ύt ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) = ( ( TopOpen β€˜ 𝐾 ) β†Ύt 𝐴 ) )
52 21 fveq2d ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( MetOpen β€˜ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) ) = ( MetOpen β€˜ ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) ) )
53 38 51 52 3eqtr3d ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( TopOpen β€˜ 𝐾 ) β†Ύt 𝐴 ) = ( MetOpen β€˜ ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) ) )
54 11 24 resstopn ⊒ ( ( TopOpen β€˜ 𝐾 ) β†Ύt 𝐴 ) = ( TopOpen β€˜ ( 𝐾 β†Ύs 𝐴 ) )
55 eqid ⊒ ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) = ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) )
56 eqid ⊒ ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) = ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) )
57 54 55 56 isxms2 ⊒ ( ( 𝐾 β†Ύs 𝐴 ) ∈ ∞MetSp ↔ ( ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) ∈ ( ∞Met β€˜ ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ∧ ( ( TopOpen β€˜ 𝐾 ) β†Ύt 𝐴 ) = ( MetOpen β€˜ ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) ) ) )
58 23 53 57 sylanbrc ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( 𝐾 β†Ύs 𝐴 ) ∈ ∞MetSp )