Theorem bcthlem15 8013

Description: Lemma for bcth 8032. Relationship between a ball Q and the next ball P in sequence g, according to the generating function F 's value (KFQ).

Hypotheses

Ref	Expression
bcthlem16.1	|- D e. CMet
bcthlem16.3	|- X = dom dom D
bcthlem16.6	|- F = {<.<.j, y>., z>. | ((j e. NN /\ y e. A) /\ z = {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))})}
bcthlem16.8	|- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))

Assertion

Ref	Expression
bcthlem15	|- (((K e. NN /\ Q e. A) /\ P e. (KFQ)) -> (((1st` P) e. X /\ ((2nd` P) e. RR /\ 0 < (2nd` P))) /\ ((2nd` P) < ((2nd` Q) / 2) /\ ((1st` P)( ball ` D)(2nd` P)) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` Q)( ball ` D)((2nd` Q) / 2))))))

Distinct variable groups:   y,j,z,A   j,p,r,D,y,z   j,J,p,r,y,z   j,K,p,r,y,z   j,M,p,r,y,z   z,O   P,p,r   Q,j,p,r,y,z   j,X,p,r,y,z

Proof of Theorem bcthlem15

Step	Hyp	Ref	Expression
1		bcthlem16.3	. . . . . . . 8 |- X = dom dom D
2		bcthlem16.1	. . . . . . . . . 10 |- D e. CMet
3		dmexg 3358	. . . . . . . . . 10 |- (D e. CMet -> dom D e. V)
4	2, 3	ax-mp 7	. . . . . . . . 9 |- dom D e. V
5	4	dmex 3360	. . . . . . . 8 |- dom dom D e. V
6	1, 5	eqeltr 1544	. . . . . . 7 |- X e. V
7		reex 5312	. . . . . . 7 |- RR e. V
8	6, 7	xpex 3260	. . . . . 6 |- (X X. RR) e. V
9		id 59	. . . . . . . . . 10 |- ((p e. X /\ r e. RR) -> (p e. X /\ r e. RR))
10	9	adantrr 395	. . . . . . . . 9 |- ((p e. X /\ (r e. RR /\ 0 < r)) -> (p e. X /\ r e. RR))
11	10	anim1i 334	. . . . . . . 8 |- (((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` Q) / 2) /\ (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` Q)( ball ` D)((2nd` Q) / 2))))) -> ((p e. X /\ r e. RR) /\ (r < ((2nd` Q) / 2) /\ (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` Q)( ball ` D)((2nd` Q) / 2))))))
12	11	ssopab2i 2823	. . . . . . 7 |- {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` Q) / 2) /\ (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` Q)( ball ` D)((2nd` Q) / 2)))))} (_ {<.p, r>. | ((p e. X /\ r e. RR) /\ (r < ((2nd` Q) / 2) /\ (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` Q)( ball ` D)((2nd` Q) / 2)))))}
13		opabssxp 3234	. . . . . . 7 |- {<.p, r>. | ((p e. X /\ r e. RR) /\ (r < ((2nd` Q) / 2) /\ (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` Q)( ball ` D)((2nd` Q) / 2)))))} (_ (X X. RR)
14	12, 13	sstri 2073	. . . . . 6 |- {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` Q) / 2) /\ (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` Q)( ball ` D)((2nd` Q) / 2)))))} (_ (X X. RR)
15	8, 14	ssexi 2720	. . . . 5 |- {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` Q) / 2) /\ (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` Q)( ball ` D)((2nd` Q) / 2)))))} e. V
16		fveq2 3724	. . . . . . . . . . . . 13 |- (j = K -> (M` j) = (M` K))
17	16	fveq2d 3728	. . . . . . . . . . . 12 |- (j = K -> ((cls` J)` (M` j)) = ((cls` J)` (M` K)))
18	17	difeq2d 2159	. . . . . . . . . . 11 |- (j = K -> (X \ ((cls` J)` (M` j))) = (X \ ((cls` J)` (M` K))))
19	18	ineq1d 2216	. . . . . . . . . 10 |- (j = K -> ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2))) = ((X \ ((cls` J)` (M` K))) i^i ((1st` y)( ball ` D)((2nd` y) / 2))))
20		bcthlem16.8	. . . . . . . . . 10 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
21	19, 20	syl5eq 1519	. . . . . . . . 9 |- (j = K -> O = ((X \ ((cls` J)` (M` K))) i^i ((1st` y)( ball ` D)((2nd` y) / 2))))
22	21	sseq2d 2089	. . . . . . . 8 |- (j = K -> ((p( ball ` D)r) (_ O <-> (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))))
23	22	anbi2d 616	. . . . . . 7 |- (j = K -> ((r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O) <-> (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` y)( ball ` D)((2nd` y) / 2))))))
24	23	anbi2d 616	. . . . . 6 |- (j = K -> (((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O)) <-> ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))))))
25	24	opabbidv 2670	. . . . 5 |- (j = K -> {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))} = {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))))})
26		fveq2 3724	. . . . . . . . . 10 |- (y = Q -> (2nd` y) = (2nd` Q))
27	26	opreq1d 3975	. . . . . . . . 9 |- (y = Q -> ((2nd` y) / 2) = ((2nd` Q) / 2))
28	27	breq2d 2630	. . . . . . . 8 |- (y = Q -> (r < ((2nd` y) / 2) <-> r < ((2nd` Q) / 2)))
29		fveq2 3724	. . . . . . . . . . 11 |- (y = Q -> (1st` y) = (1st` Q))
30	29, 27	opreq12d 3978	. . . . . . . . . 10 |- (y = Q -> ((1st` y)( ball ` D)((2nd` y) / 2)) = ((1st` Q)( ball ` D)((2nd` Q) / 2)))
31	30	ineq2d 2217	. . . . . . . . 9 |- (y = Q -> ((X \ ((cls` J)` (M` K))) i^i ((1st` y)( ball ` D)((2nd` y) / 2))) = ((X \ ((cls` J)` (M` K))) i^i ((1st` Q)( ball ` D)((2nd` Q) / 2))))
32	31	sseq2d 2089	. . . . . . . 8 |- (y = Q -> ((p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` y)( ball ` D)((2nd` y) / 2))) <-> (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` Q)( ball ` D)((2nd` Q) / 2)))))
33	28, 32	anbi12d 628	. . . . . . 7 |- (y = Q -> ((r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` y)( ball ` D)((2nd` y) / 2))))