Theorem metreslem 9099

Description: Lemma for metres 9100. (Contributed by FL, 10-Nov-2006.)

Hypotheses

Ref	Expression
metf.1	|- X = dom dom D
metreslem.2	|- A = dom dom ( D |` (R X. R))

Assertion

Ref	Expression
metreslem	|- ((D e. Met /\ R C_ X) -> (D |` (R X. R)) e. Met)

Proof of Theorem metreslem

Step	Hyp	Ref	Expression
1		fssres 4582	. . . . . 6 |- ((D:(X X. X)-->RR /\ (R X. R) C_ (X X. X)) -> (D |` (R X. R)):(R X. R)-->RR)
2		xpss12 4089	. . . . . . 7 |- ((R C_ X /\ R C_ X) -> (R X. R) C_ (X X. X))
3	2	anidms 480	. . . . . 6 |- (R C_ X -> (R X. R) C_ (X X. X))
4	1, 3	sylan2 500	. . . . 5 |- ((D:(X X. X)-->RR /\ R C_ X) -> (D |` (R X. R)):(R X. R)-->RR)
5		ssel 2615	. . . . . . . . 9 |- (R C_ X -> (x e. R -> x e. X))
6		ssel 2615	. . . . . . . . . . 11 |- (R C_ X -> (y e. R -> y e. X))
7		ssralv 2672	. . . . . . . . . . . 12 |- (R C_ X -> (A.z e. X (xDy) <_ ((zDx) + (zDy)) -> A.z e. R (xDy) <_ ((zDx) + (zDy))))
8	7	anim2d 620	. . . . . . . . . . 11 |- (R C_ X -> ((((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))) -> (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy)))))
9	6, 8	imim12d 69	. . . . . . . . . 10 |- (R C_ X -> ((y e. X -> (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy)))) -> (y e. R -> (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy))))))
10	9	ralimdv2 2173	. . . . . . . . 9 |- (R C_ X -> (A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))) -> A.y e. R (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy)))))
11	5, 10	imim12d 69	. . . . . . . 8 |- (R C_ X -> ((x e. X -> A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy)))) -> (x e. R -> A.y e. R (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy))))))
12	11	ralimdv2 2173	. . . . . . 7 |- (R C_ X -> (A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))) -> A.x e. R A.y e. R (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy)))))
13		oprvres 4963	. . . . . . . . . . . 12 |- ((x e. R /\ y e. R) -> (x(D |` (R X. R))y) = (xDy))
14	13	eqeq1d 1892	. . . . . . . . . . 11 |- ((x e. R /\ y e. R) -> ((x(D |` (R X. R))y) = 0 <-> (xDy) = 0))
15	14	bibi1d 681	. . . . . . . . . 10 |- ((x e. R /\ y e. R) -> (((x(D |` (R X. R))y) = 0 <-> x = y) <-> ((xDy) = 0 <-> x = y)))
16	13	adantl 424	. . . . . . . . . . . . 13 |- ((z e. R /\ (x e. R /\ y e. R)) -> (x(D |` (R X. R))y) = (xDy))
17		oprvres 4963	. . . . . . . . . . . . . . 15 |- ((z e. R /\ x e. R) -> (z(D |` (R X. R))x) = (zDx))
18		oprvres 4963	. . . . . . . . . . . . . . 15 |- ((z e. R /\ y e. R) -> (z(D |` (R X. R))y) = (zDy))
19	17, 18	opreqan12d 4902	. . . . . . . . . . . . . 14 |- (((z e. R /\ x e. R) /\ (z e. R /\ y e. R)) -> ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)) = ((zDx) + (zDy)))
20	19	anandis 570	. . . . . . . . . . . . 13 |- ((z e. R /\ (x e. R /\ y e. R)) -> ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)) = ((zDx) + (zDy)))
21	16, 20	breq12d 3351	. . . . . . . . . . . 12 |- ((z e. R /\ (x e. R /\ y e. R)) -> ((x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)) <-> (xDy) <_ ((zDx) + (zDy))))
22	21	ancoms 484	. . . . . . . . . . 11 |- (((x e. R /\ y e. R) /\ z e. R) -> ((x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)) <-> (xDy) <_ ((zDx) + (zDy))))
23	22	ralbidva 2119	. . . . . . . . . 10 |- ((x e. R /\ y e. R) -> (A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)) <-> A.z e. R (xDy) <_ ((zDx) + (zDy))))
24	15, 23	anbi12d 690	. . . . . . . . 9 |- ((x e. R /\ y e. R) -> ((((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))) <-> (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy)))))
25	24	ralbidva 2119	. . . . . . . 8 |- (x e. R -> (A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))) <-> A.y e. R (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy)))))
26	25	ralbiia 2133	. . . . . . 7 |- (A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))) <-> A.x e. R A.y e. R (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy))))
27	12, 26	syl6ibr 230	. . . . . 6 |- (R C_ X -> (A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))) -> A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)))))
28	27	impcom 378	. . . . 5 |- ((A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))) /\ R C_ X) -> A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))))
29	4, 28	anim12i 360	. . . 4 |- (((D:(X X. X)-->RR /\ R C_ X) /\ (A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))) /\ R C_ X)) -> ((D |` (R X. R)):(R X. R)-->RR /\ A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)))))
30	29	anandirs 571	. . 3 |- (((D:(X X. X)-->RR /\ A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy)))) /\ R C_ X) -> ((D |` (R X. R)):(R X. R)-->RR /\ A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)))))
31		metf.1	. . . 4 |- X = dom dom D
32	31	metflem 9083	. . 3 |- (D e. Met -> (D:(X X. X)-->RR /\ A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy)))))
33	30, 32	sylan 497	. 2 |- ((D e. Met /\ R C_ X) -> ((D |` (R X. R)):(R X. R)-->RR /\ A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)))))
34		resexg 4250	. . . . 5 |- (D e. Met -> (D |` (R X. R)) e. _V)
35	34	adantr 425	. . . 4 |- ((D e. Met /\ R C_ X) -> (D |` (R X. R)) e. _V)
36		metreslem.2	. . . . 5 |- A = dom dom ( D |` (R X. R))
37	36	ismet 9075	. . . 4 |- ((D |` (R X. R)) e. _V -> ((D |` (R X. R)) e. Met <-> ((D |` (R X. R)):(A X. A)-->RR /\ A.x e. A A.y e. A (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. A (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))))))
38	35, 37	syl 12	. . 3 |- ((D e. Met /\ R C_ X) -> ((D |` (R X. R)) e. Met <-> ((D |` (R X. R)):(A X. A)-->RR /\ A.x e. A A.y e. A (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. A (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))))))
39	3	adantl 424	. . . . . . . . . 10 |- ((D:(X X. X)-->RR /\ R C_ X) -> (R X. R) C_ (X X. X))
40		fdm 4567	. . . . . . . . . . 11 |- (D:(X X. X)-->RR -> dom D = (X X. X))
41	40	adantr 425	. . . . . . . . . 10 |- ((D:(X X. X)-->RR /\ R C_ X) -> dom D = (X X. X))
42	39, 41	sseqtr4d 2654	. . . . . . . . 9 |- ((D:(X X. X)-->RR /\ R C_ X) -> (R X. R) C_ dom D)
43		ssdmres 4235	. . . . . . . . 9 |- ((R X. R) C_ dom D <-> dom ( D |` (R X. R)) = (R X. R))
44	42, 43	sylib 215	. . . . . . . 8 |- ((D:(X X. X)-->RR /\ R C_ X) -> dom ( D |` (R X. R)) = (R X. R))
45	44	dmeqd 4159	. . . . . . 7 |- ((D:(X X. X)-->RR /\ R C_ X) -> dom dom ( D |` (R X. R)) = dom ( R X. R))
46		dmxpid 4179	. . . . . . 7 |- dom ( R X. R) = R
47	45, 46	syl6eq 1944	. . . . . 6 |- ((D:(X X. X)-->RR /\ R C_ X) -> dom dom ( D |` (R X. R)) = R)
48	31	metf 9084	. . . . . 6 |- (D e. Met -> D:(X X. X)-->RR)
49	47, 48	sylan 497	. . . . 5 |- ((D e. Met /\ R C_ X) -> dom dom ( D |` (R X. R)) = R)
50	49, 36	syl5eq 1940	. . . 4 |- ((D e. Met /\ R C_ X) -> A = R)
51		xpeq1 4016	. . . . . . 7 |- (A = R -> (A X. A) = (R X. A))
52		xpeq2 4017	. . . . . . 7 |- (A = R -> (R X. A) = (R X. R))
53	51, 52	eqtrd 1925	. . . . . 6 |- (A = R -> (A X. A) = (R X. R))
54	53	feq2d 4557	. . . . 5 |- (A = R -> ((D |` (R X. R)):(A X. A)-->RR <-> (D |` (R X. R)):(R X. R)-->RR))
55		raleq 2266	. . . . . . . 8 |- (A = R -> (A.z e. A (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)) <-> A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))))
56	55	anbi2d 678	. . . . . . 7 |- (A = R -> ((((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. A (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))) <-> (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)))))
57	56	raleqbi1dv 2271	. . . . . 6 |- (A = R -> (A.y e. A (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. A (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))) <-> A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)))))
58	57	raleqbi1dv 2271	. . . . 5 |- (A = R -> (A.x e. A A.y e. A (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. A (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))) <-> A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)))))
59	54, 58	anbi12d 690	. . . 4 |- (A = R -> (((D |` (R X. R)):(A X. A)-->RR /\ A.x e. A A.y e. A (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. A (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)))) <-> ((D |` (R X. R)):(R X. R)-->RR /\ A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))))))
60	50, 59	syl 12	. . 3 |- ((D e. Met /\ R C_ X) -> (((D |` (R X. R)):(A X. A)-->RR /\ A.x e. A A.y e. A (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. A (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)))) <-> ((D |` (R X. R)):(R X. R)-->RR /\ A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))))))
61	38, 60	bitrd 587	. 2 |- ((D e. Met /\ R C_ X) -> ((D |` (R X. R)) e. Met <-> ((D |` (R X. R)):(R X. R)-->RR /\ A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))))))
62	33, 61	mpbird 213	1 |- ((D e. Met /\ R C_ X) -> (D |` (R X. R)) e. Met)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292   C_ wss 2593   class class class wbr 3338   X. cxp 3984  dom cdm 3986   |` cres 3988  -->wf 3994  (class class class)co 4884  RRcr 6385  0cc0 6386   + caddc 6389   <_ cle 6448  Metcme 9066

This theorem is referenced by:  metres 9100

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-opr 4886  df-met 9070

Copyright terms: Public domain