Metamath Proof Explorer


Theorem xpsms

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 xpsms RMetSpSMetSpTMetSp

Proof

Step Hyp Ref Expression
1 xpsms.t T=R×𝑠S
2 eqid BaseR=BaseR
3 eqid BaseS=BaseS
4 simpl RMetSpSMetSpRMetSp
5 simpr RMetSpSMetSpSMetSp
6 eqid xBaseR,yBaseSx1𝑜y=xBaseR,yBaseSx1𝑜y
7 eqid ScalarR=ScalarR
8 eqid ScalarR𝑠R1𝑜S=ScalarR𝑠R1𝑜S
9 1 2 3 4 5 6 7 8 xpsval RMetSpSMetSpT=xBaseR,yBaseSx1𝑜y-1𝑠ScalarR𝑠R1𝑜S
10 1 2 3 4 5 6 7 8 xpsrnbas RMetSpSMetSpranxBaseR,yBaseSx1𝑜y=BaseScalarR𝑠R1𝑜S
11 6 xpsff1o2 xBaseR,yBaseSx1𝑜y:BaseR×BaseS1-1 ontoranxBaseR,yBaseSx1𝑜y
12 f1ocnv xBaseR,yBaseSx1𝑜y:BaseR×BaseS1-1 ontoranxBaseR,yBaseSx1𝑜yxBaseR,yBaseSx1𝑜y-1:ranxBaseR,yBaseSx1𝑜y1-1 ontoBaseR×BaseS
13 11 12 mp1i RMetSpSMetSpxBaseR,yBaseSx1𝑜y-1:ranxBaseR,yBaseSx1𝑜y1-1 ontoBaseR×BaseS
14 fvexd RMetSpSMetSpScalarRV
15 2onn 2𝑜ω
16 nnfi 2𝑜ω2𝑜Fin
17 15 16 mp1i RMetSpSMetSp2𝑜Fin
18 xpscf R1𝑜S:2𝑜MetSpRMetSpSMetSp
19 18 biimpri RMetSpSMetSpR1𝑜S:2𝑜MetSp
20 8 prdsms ScalarRV2𝑜FinR1𝑜S:2𝑜MetSpScalarR𝑠R1𝑜SMetSp
21 14 17 19 20 syl3anc RMetSpSMetSpScalarR𝑠R1𝑜SMetSp
22 9 10 13 21 imasf1oms RMetSpSMetSpTMetSp