Step |
Hyp |
Ref |
Expression |
1 |
|
simpr3 |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( R +e S ) <_ ( P D Q ) ) |
2 |
|
simpr1 |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> R e. RR* ) |
3 |
|
simpr2 |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> S e. RR* ) |
4 |
2 3
|
xaddcld |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( R +e S ) e. RR* ) |
5 |
|
xmetcl |
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) -> ( P D Q ) e. RR* ) |
6 |
5
|
adantr |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( P D Q ) e. RR* ) |
7 |
4 6
|
xrlenltd |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( R +e S ) <_ ( P D Q ) <-> -. ( P D Q ) < ( R +e S ) ) ) |
8 |
1 7
|
mpbid |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> -. ( P D Q ) < ( R +e S ) ) |
9 |
|
elin |
|- ( x e. ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) S ) ) <-> ( x e. ( P ( ball ` D ) R ) /\ x e. ( Q ( ball ` D ) S ) ) ) |
10 |
|
simpl1 |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> D e. ( *Met ` X ) ) |
11 |
|
simpl2 |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> P e. X ) |
12 |
|
elbl |
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) ) |
13 |
10 11 2 12
|
syl3anc |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) ) |
14 |
|
simpl3 |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> Q e. X ) |
15 |
|
elbl |
|- ( ( D e. ( *Met ` X ) /\ Q e. X /\ S e. RR* ) -> ( x e. ( Q ( ball ` D ) S ) <-> ( x e. X /\ ( Q D x ) < S ) ) ) |
16 |
10 14 3 15
|
syl3anc |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( x e. ( Q ( ball ` D ) S ) <-> ( x e. X /\ ( Q D x ) < S ) ) ) |
17 |
13 16
|
anbi12d |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( x e. ( P ( ball ` D ) R ) /\ x e. ( Q ( ball ` D ) S ) ) <-> ( ( x e. X /\ ( P D x ) < R ) /\ ( x e. X /\ ( Q D x ) < S ) ) ) ) |
18 |
|
anandi |
|- ( ( x e. X /\ ( ( P D x ) < R /\ ( Q D x ) < S ) ) <-> ( ( x e. X /\ ( P D x ) < R ) /\ ( x e. X /\ ( Q D x ) < S ) ) ) |
19 |
17 18
|
bitr4di |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( x e. ( P ( ball ` D ) R ) /\ x e. ( Q ( ball ` D ) S ) ) <-> ( x e. X /\ ( ( P D x ) < R /\ ( Q D x ) < S ) ) ) ) |
20 |
10
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> D e. ( *Met ` X ) ) |
21 |
11
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> P e. X ) |
22 |
|
simpr |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> x e. X ) |
23 |
|
xmetcl |
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. X ) -> ( P D x ) e. RR* ) |
24 |
20 21 22 23
|
syl3anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( P D x ) e. RR* ) |
25 |
14
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> Q e. X ) |
26 |
|
xmetcl |
|- ( ( D e. ( *Met ` X ) /\ Q e. X /\ x e. X ) -> ( Q D x ) e. RR* ) |
27 |
20 25 22 26
|
syl3anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( Q D x ) e. RR* ) |
28 |
2
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> R e. RR* ) |
29 |
3
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> S e. RR* ) |
30 |
|
xlt2add |
|- ( ( ( ( P D x ) e. RR* /\ ( Q D x ) e. RR* ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( ( ( P D x ) < R /\ ( Q D x ) < S ) -> ( ( P D x ) +e ( Q D x ) ) < ( R +e S ) ) ) |
31 |
24 27 28 29 30
|
syl22anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( ( ( P D x ) < R /\ ( Q D x ) < S ) -> ( ( P D x ) +e ( Q D x ) ) < ( R +e S ) ) ) |
32 |
|
xmettri3 |
|- ( ( D e. ( *Met ` X ) /\ ( P e. X /\ Q e. X /\ x e. X ) ) -> ( P D Q ) <_ ( ( P D x ) +e ( Q D x ) ) ) |
33 |
20 21 25 22 32
|
syl13anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( P D Q ) <_ ( ( P D x ) +e ( Q D x ) ) ) |
34 |
6
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( P D Q ) e. RR* ) |
35 |
24 27
|
xaddcld |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( ( P D x ) +e ( Q D x ) ) e. RR* ) |
36 |
4
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( R +e S ) e. RR* ) |
37 |
|
xrlelttr |
|- ( ( ( P D Q ) e. RR* /\ ( ( P D x ) +e ( Q D x ) ) e. RR* /\ ( R +e S ) e. RR* ) -> ( ( ( P D Q ) <_ ( ( P D x ) +e ( Q D x ) ) /\ ( ( P D x ) +e ( Q D x ) ) < ( R +e S ) ) -> ( P D Q ) < ( R +e S ) ) ) |
38 |
34 35 36 37
|
syl3anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( ( ( P D Q ) <_ ( ( P D x ) +e ( Q D x ) ) /\ ( ( P D x ) +e ( Q D x ) ) < ( R +e S ) ) -> ( P D Q ) < ( R +e S ) ) ) |
39 |
33 38
|
mpand |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( ( ( P D x ) +e ( Q D x ) ) < ( R +e S ) -> ( P D Q ) < ( R +e S ) ) ) |
40 |
31 39
|
syld |
|- ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( ( ( P D x ) < R /\ ( Q D x ) < S ) -> ( P D Q ) < ( R +e S ) ) ) |
41 |
40
|
expimpd |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( x e. X /\ ( ( P D x ) < R /\ ( Q D x ) < S ) ) -> ( P D Q ) < ( R +e S ) ) ) |
42 |
19 41
|
sylbid |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( x e. ( P ( ball ` D ) R ) /\ x e. ( Q ( ball ` D ) S ) ) -> ( P D Q ) < ( R +e S ) ) ) |
43 |
9 42
|
syl5bi |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( x e. ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) S ) ) -> ( P D Q ) < ( R +e S ) ) ) |
44 |
8 43
|
mtod |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> -. x e. ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) S ) ) ) |
45 |
44
|
eq0rdv |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) S ) ) = (/) ) |