Theorem metxplem4 7833

Description: Lemma for metxp 7834. Triangle inequality. Warning: The HTML proof page is 0.6 megabyte in size.

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
metxplem4	|- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> (wDv) <_ ((uDw) + (uDv)))

Distinct variable groups:   x,y,z,B   x,C,y,z   v,u,w,D   x,u,y,z,X,v,w   u,Y,v,w,x,y,z

Proof of Theorem metxplem4

Step	Hyp	Ref	Expression
1		metxp.6	. . . 4 |- C e. Met
2		metxp.3	. . . 4 |- Y = dom dom C
3		eqid 1475	. . . 4 |- (2nd` w) = (2nd` w)
4		eqid 1475	. . . 4 |- (2nd` v) = (2nd` v)
5	1, 2, 3, 4	metxplem2 7827	. . 3 |- ((w e. (X X. Y) /\ v e. (X X. Y)) -> ((2nd` w)C(2nd` v)) e. RR)
6	5	3adant1 797	. 2 |- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> ((2nd` w)C(2nd` v)) e. RR)
7		metxp.5	. . . 4 |- B e. Met
8		metxp.1	. . . 4 |- X = dom dom B
9		eqid 1475	. . . 4 |- (1st` w) = (1st` w)
10		eqid 1475	. . . 4 |- (1st` v) = (1st` v)
11	7, 8, 9, 10	metxplem1 7826	. . 3 |- ((w e. (X X. Y) /\ v e. (X X. Y)) -> ((1st` w)B(1st` v)) e. RR)
12	11	3adant1 797	. 2 |- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> ((1st` w)B(1st` v)) e. RR)
13		metxp.7	. . . . 5 |- 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, < ))}
14	8, 2, 7, 1, 13, 9, 3, 10, 4	metxptval 7830	. . . 4 |- (((w e. (X X. Y) /\ v e. (X X. Y)) /\ ((2nd` w)C(2nd` v)) <_ ((1st` w)B(1st` v))) -> (wDv) = ((1st` w)B(1st` v)))
15	14	3adantl1 803	. . 3 |- (((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) /\ ((2nd` w)C(2nd` v)) <_ ((1st` w)B(1st` v))) -> (wDv) = ((1st` w)B(1st` v)))
16		eqid 1475	. . . . . . 7 |- (2nd` u) = (2nd` u)
17	1, 2, 16, 3	metxplem2 7827	. . . . . 6 |- ((u e. (X X. Y) /\ w e. (X X. Y)) -> ((2nd` u)C(2nd` w)) e. RR)
18	17	3adant3 799	. . . . 5 |- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> ((2nd` u)C(2nd` w)) e. RR)
19		eqid 1475	. . . . . . 7 |- (1st` u) = (1st` u)
20	7, 8, 19, 9	metxplem1 7826	. . . . . 6 |- ((u e. (X X. Y) /\ w e. (X X. Y)) -> ((1st` u)B(1st` w)) e. RR)
21	20	3adant3 799	. . . . 5 |- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> ((1st` u)B(1st` w)) e. RR)
22	1, 2, 16, 4	metxplem2 7827	. . . . . . . . 9 |- ((u e. (X X. Y) /\ v e. (X X. Y)) -> ((2nd` u)C(2nd` v)) e. RR)
23	22	3adant2 798	. . . . . . . 8 |- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> ((2nd` u)C(2nd` v)) e. RR)
24	7, 8, 19, 10	metxplem1 7826	. . . . . . . . 9 |- ((u e. (X X. Y) /\ v e. (X X. Y)) -> ((1st` u)B(1st` v)) e. RR)
25	24	3adant2 798	. . . . . . . 8 |- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> ((1st` u)B(1st` v)) e. RR)
26		leidt 5531	. . . . . . . . . . . . 13 |- (((1st` u)B(1st` w)) e. RR -> ((1st` u)B(1st` w)) <_ ((1st` u)B(1st` w)))
27	20, 26	syl 10	. . . . . . . . . . . 12 |- ((u e. (X X. Y) /\ w e. (X X. Y)) -> ((1st` u)B(1st` w)) <_ ((1st` u)B(1st` w)))
28	27	3adant3 799	. . . . . . . . . . 11 |- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> ((1st` u)B(1st` w)) <_ ((1st` u)B(1st` w)))
29		leidt 5531	. . . . . . . . . . . . . 14 |- (((1st` u)B(1st` v)) e. RR -> ((1st` u)B(1st` v)) <_ ((1st` u)B(1st` v)))
30	24, 29	syl 10	. . . . . . . . . . . . 13 |- ((u e. (X X. Y) /\ v e. (X X. Y)) -> ((1st` u)B(1st` v)) <_ ((1st` u)B(1st` v)))
31	30	3adant2 798	. . . . . . . . . . . 12 |- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> ((1st` u)B(1st` v)) <_ ((1st` u)B(1st` v)))
32		elxp7 4103	. . . . . . . . . . . . . . . 16 |- (u e. (X X. Y) <-> (u e. (V X. V) /\ ((1st` u) e. X /\ (2nd` u) e. Y)))
33	32	pm3.27bi 326	. . . . . . . . . . . . . . 15 |- (u e. (X X. Y) -> ((1st` u) e. X /\ (2nd` u) e. Y))
34	33	pm3.26d 321	. . . . . . . . . . . . . 14 |- (u e. (X X. Y) -> (1st` u) e. X)
35		elxp7 4103	. . . . . . . . . . . . . . . 16 |- (w e. (X X. Y) <-> (w e. (V X. V) /\ ((1st` w) e. X /\ (2nd` w) e. Y)))
36	35	pm3.27bi 326	. . . . . . . . . . . . . . 15 |- (w e. (X X. Y) -> ((1st` w) e. X /\ (2nd` w) e. Y))
37	36	pm3.26d 321	. . . . . . . . . . . . . 14 |- (w e. (X X. Y) -> (1st` w) e. X)
38		elxp7 4103	. . . . . . . . . . . . . . . 16 |- (v e. (X X. Y) <-> (v e. (V X. V) /\ ((1st` v) e. X /\ (2nd` v) e. Y)))
39	38	pm3.27bi 326	. . . . . . . . . . . . . . 15 |- (v e. (X X. Y) -> ((1st` v) e. X /\ (2nd` v) e. Y))
40	39	pm3.26d 321	. . . . . . . . . . . . . 14 |- (v e. (X X. Y) -> (1st` v) e. X)
41	34, 37, 40	3anim123i 821	. . . . . . . . . . . . 13 |- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> ((1st` u) e. X /\ (1st` w) e. X /\ (1st` v) e. X))
42	7, 8, 21, 25, 41	metxplem3 7828	. . . . . . . . . . . 12 |- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> (((1st` u)B(1st` w)) <_ ((1st` u)B(1st` w)) -> (((1st` u)B(1st` v)) <_ ((1st` u)B(1st` v)) -> ((1st` w)B(1st` v)) <_ (((1st` u)B(1st` w)) + ((1st` u)B(1st` v))))))
43	31, 42	mpid 47	. . . . . . . . . . 11 |- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> (((1st` u)B(1st` w)) <_ ((1st` u)B(1st` w)) -> ((1st` w)B(1st` v)) <_ (((1st` u)B(1st` w)) + ((1st` u)B(1st` v)))))
44	28, 43	mpd 26	. . . . . . . . . 10 |- ((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) -> ((1st` w)B(1st` v)) <_ (((1st` u)B(1st` w)) + ((1st` u)B(1st` v))))
45	44	adantr 389	. . . . . . . . 9 |- (((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) /\ ((2nd` u)C(2nd` v)) <_ ((1st` u)B(1st` v))) -> ((1st` w)B(1st` v)) <_ (((1st` u)B(1st` w)) + ((1st` u)B(1st` v))))
46	8, 2, 7, 1, 13, 19, 16, 10, 4	metxptval 7830	. . . . . . . . . . 11 |- (((u e. (X X. Y) /\ v e. (X X. Y)) /\ ((2nd` u)C(2nd` v)) <_ ((1st` u)B(1st` v))) -> (uDv) = ((1st` u)B(1st` v)))
47	46	3adantl2 804	. . . . . . . . . 10 |- (((u e. (X X. Y) /\ w e. (X X. Y) /\ v e. (X X. Y)) /\ ((2nd