Theorem bcthlem15 7947

Description: Lemma for bcth 7966. 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 3344	. . . . . . . . . 10 |- (D e. CMet -> dom D e. V)
4	2, 3	ax-mp 7	. . . . . . . . 9 |- dom D e. V
5		dmexg 3344	. . . . . . . . 9 |- (dom D e. V -> dom dom D e. V)
6	4, 5	ax-mp 7	. . . . . . . 8 |- dom dom D e. V
7	1, 6	eqeltr 1536	. . . . . . 7 |- X e. V
8		reex 5284	. . . . . . 7 |- RR e. V
9	7, 8	xpex 3250	. . . . . 6 |- (X X. RR) e. V
10		id 59	. . . . . . . . . 10 |- ((p e. X /\ r e. RR) -> (p e. X /\ r e. RR))
11	10	adantrr 395	. . . . . . . . 9 |- ((p e. X /\ (r e. RR /\ 0 < r)) -> (p e. X /\ r e. RR))
12	11	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))))))
13	12	ssopab2i 2812	. . . . . . 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)))))}
14		opabssxp 3224	. . . . . . 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)
15	13, 14	sstri 2063	. . . . . 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)
16	9, 15	ssexi 2710	. . . . 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
17		fveq2 3709	. . . . . . . . . . . . 13 |- (j = K -> (M` j) = (M` K))
18	17	fveq2d 3713	. . . . . . . . . . . 12 |- (j = K -> ((cls` J)` (M` j)) = ((cls` J)` (M` K)))
19	18	difeq2d 2149	. . . . . . . . . . 11 |- (j = K -> (X \ ((cls` J)` (M` j))) = (X \ ((cls` J)` (M` K))))
20	19	ineq1d 2206	. . . . . . . . . 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))))
21		bcthlem16.8	. . . . . . . . . 10 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
22	20, 21	syl5eq 1511	. . . . . . . . 9 |- (j = K -> O = ((X \ ((cls` J)` (M` K))) i^i ((1st` y)( ball ` D)((2nd` y) / 2))))
23	22	sseq2d 2079	. . . . . . . 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)))))
24	23	anbi2d 614	. . . . . . 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))))))
25	24	anbi2d 614	. . . . . 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)))))))
26	25	opabbidv 2660	. . . . 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)))))})
27		fveq2 3709	. . . . . . . . . 10 |- (y = Q -> (2nd` y) = (2nd` Q))
28	27	opreq1d 3960	. . . . . . . . 9 |- (y = Q -> ((2nd` y) / 2) = ((2nd` Q) / 2))
29	28	breq2d 2620	. . . . . . . 8 |- (y = Q -> (r < ((2nd` y) / 2) <-> r < ((2nd` Q) / 2)))
30		fveq2 3709	. . . . . . . . . . 11 |- (y = Q -> (1st` y) = (1st` Q))
31	30, 28	opreq12d 3963	. . . . . . . . . 10 |- (y = Q -> ((1st` y)( ball ` D)((2nd` y) / 2)) = ((1st` Q)( ball ` D)((2nd` Q) / 2)))
32	31	ineq2d 2207	. . . . . . . . 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))))
33	32	sseq2d 2079	. . . . . . . 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)))))
34	29, 33	anbi12d 626	. . . . . . 7 |- (y = Q -> ((r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ ((X \ ((cls` J)` (M` K))) i^i ((1st` y