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{\times }_{𝑠}S$$
	xpsds.x	$$⊢X={\mathrm{Base}}_R$$
	xpsds.y	$$⊢Y={\mathrm{Base}}_S$$
	xpsds.1	$$⊢\phi \to R\in V$$
	xpsds.2	$$⊢\phi \to S\in W$$
	xpsds.p	$$⊢P=\mathrm{dist}\left(T\right)$$
Assertion	xpsdsfn	$$⊢\phi \to PFn\left(\left(X\times Y\right)\times \left(X\times Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpsds.t	$$⊢T=R{\times }_{𝑠}S$$
2		xpsds.x	$$⊢X={\mathrm{Base}}_R$$
3		xpsds.y	$$⊢Y={\mathrm{Base}}_S$$
4		xpsds.1	$$⊢\phi \to R\in V$$
5		xpsds.2	$$⊢\phi \to S\in W$$
6		xpsds.p	$$⊢P=\mathrm{dist}\left(T\right)$$
7		eqid	$$⊢\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)=\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
8		eqid	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(R\right)$$
9		eqid	$$⊢\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}$$
10	1 2 3 4 5 7 8 9	xpsval	$$⊢\phi \to T={\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}{“}_{𝑠}\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)$$
11	1 2 3 4 5 7 8 9	xpsrnbas	$$⊢\phi \to \mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)={\mathrm{Base}}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)}$$
12	7	xpsff1o2	$$⊢\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right):X\times Y\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
13	12	a1i	$$⊢\phi \to \left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right):X\times Y\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
14		f1ocnv	$$⊢\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right):X\times Y\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\to {\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{1-1\; onto}{⟶}X\times Y$$
15		f1ofo	$$⊢{\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{1-1\; onto}{⟶}X\times Y\to {\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{onto}{⟶}X\times Y$$
16	13 14 15	3syl	$$⊢\phi \to {\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{onto}{⟶}X\times Y$$
17		ovexd	$$⊢\phi \to \mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\in \mathrm{V}$$
18		eqid	$$⊢\mathrm{dist}\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)=\mathrm{dist}\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)$$
19	10 11 16 17 18 6	imasdsfn	$$⊢\phi \to PFn\left(\left(X\times Y\right)\times \left(X\times Y\right)\right)$$