xpsxmet

Description: A product metric of extended metrics is an extended metric. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypotheses	xpsds.t	$⊢ T = R \times_{𝑠} S$
	xpsds.x	$⊢ X = {Base}_{R}$
	xpsds.y	$⊢ Y = {Base}_{S}$
	xpsds.1	$⊢ φ \to R \in V$
	xpsds.2	$⊢ φ \to S \in W$
	xpsds.p	$⊢ P = dist (T)$
	xpsds.m	$⊢ M = {dist (R) ↾}_{(X \times X)}$
	xpsds.n	$⊢ N = {dist (S) ↾}_{(Y \times Y)}$
	xpsds.3	$⊢ φ \to M \in ∞Met (X)$
	xpsds.4	$⊢ φ \to N \in ∞Met (Y)$
Assertion	xpsxmet	$⊢ φ \to P \in ∞Met (X \times Y)$

Proof

Step	Hyp	Ref	Expression
1		xpsds.t	$⊢ T = R \times_{𝑠} S$
2		xpsds.x	$⊢ X = {Base}_{R}$
3		xpsds.y	$⊢ Y = {Base}_{S}$
4		xpsds.1	$⊢ φ \to R \in V$
5		xpsds.2	$⊢ φ \to S \in W$
6		xpsds.p	$⊢ P = dist (T)$
7		xpsds.m	$⊢ M = {dist (R) ↾}_{(X \times X)}$
8		xpsds.n	$⊢ N = {dist (S) ↾}_{(Y \times Y)}$
9		xpsds.3	$⊢ φ \to M \in ∞Met (X)$
10		xpsds.4	$⊢ φ \to N \in ∞Met (Y)$
11		eqid	$⊢ (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) = (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
12		eqid	$⊢ Scalar (R) = Scalar (R)$
13		eqid	$⊢ Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} = Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}$
14	1 2 3 4 5 11 12 13	xpsval	$⊢ φ \to T = {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})$
15	1 2 3 4 5 11 12 13	xpsrnbas	$⊢ φ \to ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) = {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
16	11	xpsff1o2	$⊢ (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) : X \times Y \underset{1-1 onto}{⟶} ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
17		f1ocnv	$⊢ (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) : X \times Y \underset{1-1 onto}{⟶} ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \underset{1-1 onto}{⟶} X \times Y$
18	16 17	mp1i	$⊢ φ \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \underset{1-1 onto}{⟶} X \times Y$
19		ovexd	$⊢ φ \to Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} \in V$
20		eqid	$⊢ {dist (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) ↾}_{(ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \times ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}))} = {dist (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) ↾}_{(ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \times ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}))}$
21	1 2 3 4 5 6 7 8 9 10	xpsxmetlem	$⊢ φ \to dist (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) \in ∞Met (ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}))$
22		ssid	$⊢ ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \subseteq ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
23		xmetres2	$⊢ (dist (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) \in ∞Met (ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})) \land ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \subseteq ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})) \to {dist (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) ↾}_{(ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \times ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}))} \in ∞Met (ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}))$
24	21 22 23	sylancl	$⊢ φ \to {dist (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) ↾}_{(ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \times ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}))} \in ∞Met (ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}))$
25	14 15 18 19 20 6 24	imasf1oxmet	$⊢ φ \to P \in ∞Met (X \times Y)$

Metamath Proof Explorer

Theorem xpsxmet

Proof