Metamath Proof Explorer

Theorem ressms

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

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

Proof

Step Hyp Ref Expression
1 msxms ⊒ ( 𝐾 ∈ MetSp β†’ 𝐾 ∈ ∞MetSp )
2 ressxms ⊒ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( 𝐾 β†Ύs 𝐴 ) ∈ ∞MetSp )
3 1 2 sylan ⊒ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( 𝐾 β†Ύs 𝐴 ) ∈ ∞MetSp )
4 eqid ⊒ ( Base β€˜ 𝐾 ) = ( Base β€˜ 𝐾 )
5 eqid ⊒ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) = ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) )
6 4 5 msmet ⊒ ( 𝐾 ∈ MetSp β†’ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ∈ ( Met β€˜ ( Base β€˜ 𝐾 ) ) )
7 6 adantr ⊒ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ∈ ( Met β€˜ ( Base β€˜ 𝐾 ) ) )
8 metres ⊒ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) ∈ ( Met β€˜ ( Base β€˜ 𝐾 ) ) β†’ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) ∈ ( Met β€˜ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) )
9 7 8 syl ⊒ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) ∈ ( Met β€˜ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) )
10 resres ⊒ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) = ( ( dist β€˜ 𝐾 ) β†Ύ ( ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ∩ ( 𝐴 Γ— 𝐴 ) ) )
11 inxp ⊒ ( ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ∩ ( 𝐴 Γ— 𝐴 ) ) = ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) )
12 11 reseq2i ⊒ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ∩ ( 𝐴 Γ— 𝐴 ) ) ) = ( ( dist β€˜ 𝐾 ) β†Ύ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) )
13 10 12 eqtri ⊒ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) = ( ( dist β€˜ 𝐾 ) β†Ύ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) )
14 eqid ⊒ ( 𝐾 β†Ύs 𝐴 ) = ( 𝐾 β†Ύs 𝐴 )
15 eqid ⊒ ( dist β€˜ 𝐾 ) = ( dist β€˜ 𝐾 )
16 14 15 ressds ⊒ ( 𝐴 ∈ 𝑉 β†’ ( dist β€˜ 𝐾 ) = ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) )
17 16 adantl ⊒ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( dist β€˜ 𝐾 ) = ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) )
18 incom ⊒ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( Base β€˜ 𝐾 ) )
19 14 4 ressbas ⊒ ( 𝐴 ∈ 𝑉 β†’ ( 𝐴 ∩ ( Base β€˜ 𝐾 ) ) = ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) )
20 19 adantl ⊒ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( 𝐴 ∩ ( Base β€˜ 𝐾 ) ) = ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) )
21 18 20 eqtrid ⊒ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) = ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) )
22 21 sqxpeqd ⊒ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) = ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) )
23 17 22 reseq12d ⊒ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( dist β€˜ 𝐾 ) β†Ύ ( ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) Γ— ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) ) = ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) )
24 13 23 eqtrid ⊒ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( ( dist β€˜ 𝐾 ) β†Ύ ( ( Base β€˜ 𝐾 ) Γ— ( Base β€˜ 𝐾 ) ) ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) = ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) )
25 21 fveq2d ⊒ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( Met β€˜ ( ( Base β€˜ 𝐾 ) ∩ 𝐴 ) ) = ( Met β€˜ ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) )
26 9 24 25 3eltr3d ⊒ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) ∈ ( Met β€˜ ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) )
27 eqid ⊒ ( TopOpen β€˜ 𝐾 ) = ( TopOpen β€˜ 𝐾 )
28 14 27 resstopn ⊒ ( ( TopOpen β€˜ 𝐾 ) β†Ύt 𝐴 ) = ( TopOpen β€˜ ( 𝐾 β†Ύs 𝐴 ) )
29 eqid ⊒ ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) = ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) )
30 eqid ⊒ ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) = ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) )
31 28 29 30 isms ⊒ ( ( 𝐾 β†Ύs 𝐴 ) ∈ MetSp ↔ ( ( 𝐾 β†Ύs 𝐴 ) ∈ ∞MetSp ∧ ( ( dist β€˜ ( 𝐾 β†Ύs 𝐴 ) ) β†Ύ ( ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) Γ— ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) ∈ ( Met β€˜ ( Base β€˜ ( 𝐾 β†Ύs 𝐴 ) ) ) ) )
32 3 26 31 sylanbrc ⊒ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) β†’ ( 𝐾 β†Ύs 𝐴 ) ∈ MetSp )