Theorem metxp 7834

Description: The direct product of two metric spaces. Definition 14-1.5 of [Gleason] p. 225.

Hypotheses

Ref	Expression
metxp.1	|- X = dom dom B
metxp.3	|- Y = dom dom C
metxp.5	|- B e. Met
metxp.6	|- C e. Met
metxp.7	|- D = {<.<.x, y>., z>. | ((x e. (X X. Y) /\ y e. (X X. Y)) /\ z = sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ))}

Assertion

Ref	Expression
metxp	|- D e. Met

Distinct variable groups:   x,y,z,B   x,C,y,z   x,X,y,z   x,Y,y,z

Proof of Theorem metxp

Step	Hyp	Ref	Expression
1		metxp.1	. . . 4 |- X = dom dom B
2		metxp.5	. . . . . 6 |- B e. Met
3		dmexg 3358	. . . . . 6 |- (B e. Met -> dom B e. V)
4	2, 3	ax-mp 7	. . . . 5 |- dom B e. V
5	4	dmex 3360	. . . 4 |- dom dom B e. V
6	1, 5	eqeltr 1544	. . 3 |- X e. V
7		metxp.3	. . . 4 |- Y = dom dom C
8		metxp.6	. . . . . 6 |- C e. Met
9		dmexg 3358	. . . . . 6 |- (C e. Met -> dom C e. V)
10	8, 9	ax-mp 7	. . . . 5 |- dom C e. V
11	10	dmex 3360	. . . 4 |- dom dom C e. V
12	7, 11	eqeltr 1544	. . 3 |- Y e. V
13	6, 12	xpex 3260	. 2 |- (X X. Y) e. V
14		ffnoprval 4014	. . 3 |- (D:((X X. Y) X. (X X. Y))-->RR <-> (D Fn ((X X. Y) X. (X X. Y)) /\ A.w e. (X X. Y)A.v e. (X X. Y)(wDv) e. RR))
15		ltso 5512	. . . . 5 |- < Or RR
16	15	supex 4577	. . . 4 |- sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ) e. V
17		metxp.7	. . . 4 |- D = {<.<.x, y>., z>. | ((x e. (X X. Y) /\ y e. (X X. Y)) /\ z = sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ))}
18	16, 17	fnoprab2 4122	. . 3 |- D Fn ((X X. Y) X. (X X. Y))
19	1, 7, 2, 8, 17	metxpcl 7832	. . . 4 |- ((w e. (X X. Y) /\ v e. (X X. Y)) -> (wDv) e. RR)
20	19	rgen2a 1699	. . 3 |- A.w e. (X X. Y)A.v e. (X X. Y)(wDv) e. RR
21	14, 18, 20	mpbir2an 730	. 2 |- D:((X X. Y) X. (X X. Y))-->RR
22		eqid 1475	. . . . 5 |- (1st` w) = (1st` w)
23		eqid 1475	. . . . 5 |- (2nd` w) = (2nd` w)
24		eqid 1475	. . . . 5 |- (1st` v) = (1st` v)
25		eqid 1475	. . . . 5 |- (2nd` v) = (2nd` v)
26	1, 7, 2, 8, 17, 22, 23, 24, 25	metxpdval 7829	. . . 4 |- ((w e. (X X. Y) /\ v e. (X X. Y)) -> (wDv) = if(((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v)), ((1st` w)B(1st` v)), ((2nd` w)C(2nd` v))))
27	26	eqeq1d 1483	. . 3 |- ((w e. (X X. Y) /\ v e. (X X. Y)) -> ((wDv) = 0 <-> if(((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v)), ((1st` w)B(1st` v)), ((2nd` w)C(2nd` v))) = 0))
28		iftrue 2366	. . . . . . . 8 |- (((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v)) -> if(((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v)), ((1st` w)B(1st` v)), ((2nd` w)C(2nd` v))) = ((1st` w)B(1st` v)))
29	28	eqeq1d 1483	. . . . . . 7 |- (((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v)) -> (if(((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v)), ((1st` w)B(1st` v)), ((2nd` w)C(2nd` v))) = 0 <-> ((1st` w)B(1st` v)) = 0))
30	29	adantl 388	. . . . . 6 |- (((w e. (X X. Y) /\ v e. (X X. Y)) /\ ((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v))) -> (if(((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v)), ((1st` w)B(1st` v)), ((2nd` w)C(2nd` v))) = 0 <-> ((1st` w)B(1st` v)) = 0))
31		breq2 2623	. . . . . . . . . 10 |- (((1st` w)B(1st` v)) = 0 -> (((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v)) <-> ((2nd` w)C(2nd` v)) < 0))
32	31	biimpac 418	. . . . . . . . 9 |- ((((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v)) /\ ((1st` w)B(1st` v)) = 0) -> ((2nd` w)C(2nd` v)) < 0)
33	32	adantll 392	. . . . . . . 8 |- ((((w e. (X X. Y) /\ v e. (X X. Y)) /\ ((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v))) /\ ((1st` w)B(1st` v)) = 0) -> ((2nd` w)C(2nd` v)) < 0)
34	7	metge0 7819	. . . . . . . . . . . . 13 |- ((C e. Met /\ (2nd` w) e. Y /\ (2nd` v) e. Y) -> 0 <_ ((2nd` w)C(2nd` v)))
35	8, 34	mp3an1 903	. . . . . . . . . . . 12 |- (((2nd` w) e. Y /\ (2nd` v) e. Y) -> 0 <_ ((2nd` w)C(2nd` v)))
36	7	metcl 7811	. . . . . . . . . . . . . 14 |- ((C e. Met /\ (2nd` w) e. Y /\ (2nd` v) e. Y) -> ((2nd` w)C(2nd` v)) e. RR)
37	8, 36	mp3an1 903	. . . . . . . . . . . . 13 |- (((2nd` w) e. Y /\ (2nd` v) e. Y) -> ((2nd` w)C(2nd` v)) e. RR)
38		0re 5440	. . . . . . . . . . . . . 14 |- 0 e. RR
39		lenltt 5510	. . . . . . . . . . . . . 14 |- ((0 e. RR /\ ((2nd` w)C(2nd` v)) e. RR) -> (0 <_ ((2nd` w)C(2nd` v)) <-> -. ((2nd` w)C(2nd` v)) < 0))
40	38, 39	mpan 695	. . . . . . . . . . . . 13 |- (((2nd` w)C(2nd` v)) e. RR -> (0 <_ ((2nd` w)C(2nd` v)) <-> -. ((2nd` w)C(2nd` v)) < 0))
41	37, 40	syl 10	. . . . . . . . . . . 12 |- (((2nd` w) e. Y /\ (2nd` v) e. Y) -> (0 <_ ((2nd` w)C(2nd` v)) <-> -. ((2nd` w)C(2nd` v)) < 0))
42	35, 41	mpbid 195	. . . . . . . . . . 11 |- (((2nd` w) e. Y /\ (2nd` v) e. Y) -> -. ((2nd` w)C(2nd` v)) < 0)
43		elxp7 4103	. . . . . . . . . . . . 13 |- (w e. (X X. Y) <-> (w e. (V X. V) /\ ((1st` w) e. X /\ (2nd` w) e. Y)))
44	43	pm3.27bi 326	. . . . . . . . . . . 12 |- (w e. (X X. Y) -> ((1st` w) e. X /\ (2nd` w) e. Y))
45	44	pm3.27d 325	. . . . . . . . . . 11 |- (w e. (X X. Y) -> (2nd` w) e. Y)
46		elxp7 4103	. . . . . . . . . . . . 13 |- (v e. (X X. Y) <-> (v e. (V X. V) /\ ((1st` v) e. X /\ (2nd` v) e. Y)))
47	46	pm3.27bi 326	. . . . . . . . . . . 12 |- (v e. (X X. Y) -> ((1st` v) e. X /\ (2nd` v) e. Y))
48	47	pm3.27d 325	. . . . . . . . . . 11 |- (v e. (X X. Y) -> (2nd` v) e. Y)
49	42, 45, 48	syl2an 454	. . . . . . . . . 10 |- ((w e. (X X. Y) /\ v e. (X X. Y)) -> -. ((2nd` w)C(2nd` v)) < 0)
50	49	pm2.21d 78	. . . . . . . . 9 |- ((w e. (X X. Y) /\ v e. (X X. Y)) -> (((2nd` w)C(2nd` v)) < 0 -> w = v))
51	50	ad2antrr 404	. . . . . . . 8 |- ((((w e. (X X. Y) /\ v e. (X X. Y)) /\ ((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v))) /\ ((1st` w)B(1st` v)) = 0) -> (((2nd` w)C(2nd` v)) < 0 -> w = v))
52	33, 51	mpd 26	. . . . . . 7 |- ((((w e. (X X. Y) /\ v e. (X X. Y)) /\ ((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v))) /\ ((1st` w)B(1st` v)) = 0) -> w = v)
53	52	ex 373	. . . . . 6 |- (((w e. (X X. Y) /\ v e. (X X. Y)) /\ ((2nd` w)C(2nd` v)) < ((1st` w)B(1st` v)