Metamath Proof Explorer


Theorem xpsdsfn

Description: Closure of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses xpsds.t T = R × 𝑠 S
xpsds.x X = Base R
xpsds.y Y = Base S
xpsds.1 φ R V
xpsds.2 φ S W
xpsds.p P = dist T
Assertion xpsdsfn φ P Fn X × Y × X × Y

Proof

Step Hyp Ref Expression
1 xpsds.t T = R × 𝑠 S
2 xpsds.x X = Base R
3 xpsds.y Y = Base S
4 xpsds.1 φ R V
5 xpsds.2 φ S W
6 xpsds.p P = dist T
7 eqid x X , y Y x 1 𝑜 y = x X , y Y x 1 𝑜 y
8 eqid Scalar R = Scalar R
9 eqid Scalar R 𝑠 R 1 𝑜 S = Scalar R 𝑠 R 1 𝑜 S
10 1 2 3 4 5 7 8 9 xpsval φ T = x X , y Y x 1 𝑜 y -1 𝑠 Scalar R 𝑠 R 1 𝑜 S
11 1 2 3 4 5 7 8 9 xpsrnbas φ ran x X , y Y x 1 𝑜 y = Base Scalar R 𝑠 R 1 𝑜 S
12 7 xpsff1o2 x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y
13 12 a1i φ x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y
14 f1ocnv x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y x X , y Y x 1 𝑜 y -1 : ran x X , y Y x 1 𝑜 y 1-1 onto X × Y
15 f1ofo x X , y Y x 1 𝑜 y -1 : ran x X , y Y x 1 𝑜 y 1-1 onto X × Y x X , y Y x 1 𝑜 y -1 : ran x X , y Y x 1 𝑜 y onto X × Y
16 13 14 15 3syl φ x X , y Y x 1 𝑜 y -1 : ran x X , y Y x 1 𝑜 y onto X × Y
17 ovexd φ Scalar R 𝑠 R 1 𝑜 S V
18 eqid dist Scalar R 𝑠 R 1 𝑜 S = dist Scalar R 𝑠 R 1 𝑜 S
19 10 11 16 17 18 6 imasdsfn φ P Fn X × Y × X × Y