Metamath Proof Explorer


Theorem xpsxms

Description: A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypothesis xpsms.t ⊒T=R×𝑠S
Assertion xpsxms ⊒R∈∞MetSp∧S∈∞MetSpβ†’T∈∞MetSp

Proof

Step Hyp Ref Expression
1 xpsms.t ⊒T=R×𝑠S
2 eqid ⊒BaseR=BaseR
3 eqid ⊒BaseS=BaseS
4 simpl ⊒R∈∞MetSp∧S∈∞MetSpβ†’R∈∞MetSp
5 simpr ⊒R∈∞MetSp∧S∈∞MetSpβ†’S∈∞MetSp
6 eqid ⊒x∈BaseR,y∈BaseSβŸΌβˆ…x1π‘œy=x∈BaseR,y∈BaseSβŸΌβˆ…x1π‘œy
7 eqid ⊒Scalar⁑R=Scalar⁑R
8 eqid ⊒Scalar⁑Rβ¨‰π‘ βˆ…R1π‘œS=Scalar⁑Rβ¨‰π‘ βˆ…R1π‘œS
9 1 2 3 4 5 6 7 8 xpsval ⊒R∈∞MetSp∧S∈∞MetSpβ†’T=x∈BaseR,y∈BaseSβŸΌβˆ…x1π‘œy-1β€œπ‘ Scalar⁑Rβ¨‰π‘ βˆ…R1π‘œS
10 1 2 3 4 5 6 7 8 xpsrnbas ⊒R∈∞MetSp∧S∈∞MetSpβ†’ran⁑x∈BaseR,y∈BaseSβŸΌβˆ…x1π‘œy=BaseScalar⁑Rβ¨‰π‘ βˆ…R1π‘œS
11 6 xpsff1o2 ⊒x∈BaseR,y∈BaseSβŸΌβˆ…x1π‘œy:BaseRΓ—BaseS⟢1-1 ontoran⁑x∈BaseR,y∈BaseSβŸΌβˆ…x1π‘œy
12 f1ocnv ⊒x∈BaseR,y∈BaseSβŸΌβˆ…x1π‘œy:BaseRΓ—BaseS⟢1-1 ontoran⁑x∈BaseR,y∈BaseSβŸΌβˆ…x1π‘œyβ†’x∈BaseR,y∈BaseSβŸΌβˆ…x1π‘œy-1:ran⁑x∈BaseR,y∈BaseSβŸΌβˆ…x1π‘œy⟢1-1 ontoBaseRΓ—BaseS
13 11 12 mp1i ⊒R∈∞MetSp∧S∈∞MetSpβ†’x∈BaseR,y∈BaseSβŸΌβˆ…x1π‘œy-1:ran⁑x∈BaseR,y∈BaseSβŸΌβˆ…x1π‘œy⟢1-1 ontoBaseRΓ—BaseS
14 fvexd ⊒R∈∞MetSp∧S∈∞MetSpβ†’Scalar⁑R∈V
15 2onn ⊒2π‘œβˆˆΟ‰
16 nnfi ⊒2π‘œβˆˆΟ‰β†’2π‘œβˆˆFin
17 15 16 mp1i ⊒R∈∞MetSp∧S∈∞MetSpβ†’2π‘œβˆˆFin
18 xpscf βŠ’βˆ…R1π‘œS:2π‘œβŸΆβˆžMetSp↔R∈∞MetSp∧S∈∞MetSp
19 18 biimpri ⊒R∈∞MetSp∧S∈∞MetSpβ†’βˆ…R1π‘œS:2π‘œβŸΆβˆžMetSp
20 8 prdsxms ⊒Scalar⁑R∈V∧2π‘œβˆˆFinβˆ§βˆ…R1π‘œS:2π‘œβŸΆβˆžMetSpβ†’Scalar⁑Rβ¨‰π‘ βˆ…R1π‘œS∈∞MetSp
21 14 17 19 20 syl3anc ⊒R∈∞MetSp∧S∈∞MetSpβ†’Scalar⁑Rβ¨‰π‘ βˆ…R1π‘œS∈∞MetSp
22 9 10 13 21 imasf1oxms ⊒R∈∞MetSp∧S∈∞MetSpβ†’T∈∞MetSp