xpsmet

Description: The direct product of two metric spaces. Definition 14-1.5 of Gleason p. 225. (Contributed by NM, 20-Jun-2007) (Revised by Mario Carneiro, 20-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)}$
	xpsmet.3	$⊢ φ \to M \in Met (X)$
	xpsmet.4	$⊢ φ \to N \in Met (Y)$
Assertion	xpsmet	$⊢ φ \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		xpsmet.3	$⊢ φ \to M \in Met (X)$
10		xpsmet.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		eqid	$⊢ Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) = Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k))$
22		eqid	$⊢ {Base}_{(Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)))} = {Base}_{(Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)))}$
23		eqid	$⊢ {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} = {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)}$
24		eqid	$⊢ {dist (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) ↾}_{({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \times {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})} = {dist (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) ↾}_{({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \times {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})}$
25		eqid	$⊢ dist (Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k))) = dist (Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)))$
26		fvexd	$⊢ φ \to Scalar (R) \in V$
27		2onn	$⊢ 2_{𝑜} \in ω$
28		nnfi	$⊢ 2_{𝑜} \in ω \to 2_{𝑜} \in Fin$
29	27 28	mp1i	$⊢ φ \to 2_{𝑜} \in Fin$
30		fvexd	$⊢ (φ \land k \in 2_{𝑜}) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k) \in V$
31		elpri	$⊢ k \in \{\emptyset, 1_{𝑜}\} \to (k = \emptyset \lor k = 1_{𝑜})$
32		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
33	31 32	eleq2s	$⊢ k \in 2_{𝑜} \to (k = \emptyset \lor k = 1_{𝑜})$
34	9	adantr	$⊢ (φ \land k = \emptyset) \to M \in Met (X)$
35		fveq2	$⊢ k = \emptyset \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k) = \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (\emptyset)$
36		fvpr0o	$⊢ R \in V \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (\emptyset) = R$
37	4 36	syl	$⊢ φ \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (\emptyset) = R$
38	35 37	sylan9eqr	$⊢ (φ \land k = \emptyset) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k) = R$
39	38	fveq2d	$⊢ (φ \land k = \emptyset) \to dist (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) = dist (R)$
40	38	fveq2d	$⊢ (φ \land k = \emptyset) \to {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} = {Base}_{R}$
41	40 2	syl6eqr	$⊢ (φ \land k = \emptyset) \to {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} = X$
42	41	sqxpeqd	$⊢ (φ \land k = \emptyset) \to {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \times {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} = X \times X$
43	39 42	reseq12d	$⊢ (φ \land k = \emptyset) \to {dist (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) ↾}_{({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \times {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})} = {dist (R) ↾}_{(X \times X)}$
44	43 7	syl6eqr	$⊢ (φ \land k = \emptyset) \to {dist (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) ↾}_{({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \times {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})} = M$
45	41	fveq2d	$⊢ (φ \land k = \emptyset) \to Met ({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)}) = Met (X)$
46	34 44 45	3eltr4d	$⊢ (φ \land k = \emptyset) \to {dist (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) ↾}_{({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \times {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})} \in Met ({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})$
47	10	adantr	$⊢ (φ \land k = 1_{𝑜}) \to N \in Met (Y)$
48		fveq2	$⊢ k = 1_{𝑜} \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k) = \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜})$
49		fvpr1o	$⊢ S \in W \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜}) = S$
50	5 49	syl	$⊢ φ \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜}) = S$
51	48 50	sylan9eqr	$⊢ (φ \land k = 1_{𝑜}) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k) = S$
52	51	fveq2d	$⊢ (φ \land k = 1_{𝑜}) \to dist (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) = dist (S)$
53	51	fveq2d	$⊢ (φ \land k = 1_{𝑜}) \to {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} = {Base}_{S}$
54	53 3	syl6eqr	$⊢ (φ \land k = 1_{𝑜}) \to {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} = Y$
55	54	sqxpeqd	$⊢ (φ \land k = 1_{𝑜}) \to {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \times {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} = Y \times Y$
56	52 55	reseq12d	$⊢ (φ \land k = 1_{𝑜}) \to {dist (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) ↾}_{({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \times {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})} = {dist (S) ↾}_{(Y \times Y)}$
57	56 8	syl6eqr	$⊢ (φ \land k = 1_{𝑜}) \to {dist (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) ↾}_{({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \times {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})} = N$
58	54	fveq2d	$⊢ (φ \land k = 1_{𝑜}) \to Met ({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)}) = Met (Y)$
59	47 57 58	3eltr4d	$⊢ (φ \land k = 1_{𝑜}) \to {dist (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) ↾}_{({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \times {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})} \in Met ({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})$
60	46 59	jaodan	$⊢ (φ \land (k = \emptyset \lor k = 1_{𝑜})) \to {dist (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) ↾}_{({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \times {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})} \in Met ({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})$
61	33 60	sylan2	$⊢ (φ \land k \in 2_{𝑜}) \to {dist (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)) ↾}_{({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \times {Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})} \in Met ({Base}_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)})$
62	21 22 23 24 25 26 29 30 61	prdsmet	$⊢ φ \to dist (Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k))) \in Met ({Base}_{(Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)))})$
63		fnpr2o	$⊢ (R \in V \land S \in W) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜}$
64	4 5 63	syl2anc	$⊢ φ \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜}$
65		dffn5	$⊢ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜} \leftrightarrow \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} = (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k))$
66	64 65	sylib	$⊢ φ \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} = (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k))$
67	66	oveq2d	$⊢ φ \to Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} = Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k))$
68	67	fveq2d	$⊢ φ \to dist (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) = dist (Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)))$
69	67	fveq2d	$⊢ φ \to {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} = {Base}_{(Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)))}$
70	15 69	eqtrd	$⊢ φ \to ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) = {Base}_{(Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)))}$
71	70	fveq2d	$⊢ φ \to Met (ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})) = Met ({Base}_{(Scalar (R) ⨉_{𝑠} (k \in 2_{𝑜} ⟼ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)))})$
72	62 68 71	3eltr4d	$⊢ φ \to dist (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) \in Met (ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}))$
73		ssid	$⊢ ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \subseteq ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
74		metres2	$⊢ (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⟩\}))$
75	72 73 74	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⟩\}))$
76	14 15 18 19 20 6 75	imasf1omet	$⊢ φ \to P \in Met (X \times Y)$

Metamath Proof Explorer

Theorem xpsmet

Proof