Step |
Hyp |
Ref |
Expression |
1 |
|
minvec.x |
⊢ 𝑋 = ( Base ‘ 𝑈 ) |
2 |
|
minvec.m |
⊢ − = ( -g ‘ 𝑈 ) |
3 |
|
minvec.n |
⊢ 𝑁 = ( norm ‘ 𝑈 ) |
4 |
|
minvec.u |
⊢ ( 𝜑 → 𝑈 ∈ ℂPreHil ) |
5 |
|
minvec.y |
⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) ) |
6 |
|
minvec.w |
⊢ ( 𝜑 → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp ) |
7 |
|
minvec.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑋 ) |
8 |
|
minvec.j |
⊢ 𝐽 = ( TopOpen ‘ 𝑈 ) |
9 |
|
minvec.r |
⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) |
10 |
|
minvec.s |
⊢ 𝑆 = inf ( 𝑅 , ℝ , < ) |
11 |
|
minvec.d |
⊢ 𝐷 = ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) |
12 |
|
minvec.f |
⊢ 𝐹 = ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) |
13 |
|
ssrab2 |
⊢ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ⊆ 𝑌 |
14 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) ) |
15 |
|
elpw2g |
⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → ( { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ∈ 𝒫 𝑌 ↔ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ⊆ 𝑌 ) ) |
16 |
14 15
|
syl |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ∈ 𝒫 𝑌 ↔ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ⊆ 𝑌 ) ) |
17 |
13 16
|
mpbiri |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ∈ 𝒫 𝑌 ) |
18 |
17
|
fmpttd |
⊢ ( 𝜑 → ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) : ℝ+ ⟶ 𝒫 𝑌 ) |
19 |
18
|
frnd |
⊢ ( 𝜑 → ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) ⊆ 𝒫 𝑌 ) |
20 |
12 19
|
eqsstrid |
⊢ ( 𝜑 → 𝐹 ⊆ 𝒫 𝑌 ) |
21 |
|
1rp |
⊢ 1 ∈ ℝ+ |
22 |
|
eqid |
⊢ ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) = ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) |
23 |
22 17
|
dmmptd |
⊢ ( 𝜑 → dom ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) = ℝ+ ) |
24 |
21 23
|
eleqtrrid |
⊢ ( 𝜑 → 1 ∈ dom ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) ) |
25 |
24
|
ne0d |
⊢ ( 𝜑 → dom ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) ≠ ∅ ) |
26 |
|
dm0rn0 |
⊢ ( dom ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) = ∅ ↔ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) = ∅ ) |
27 |
12
|
eqeq1i |
⊢ ( 𝐹 = ∅ ↔ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) = ∅ ) |
28 |
26 27
|
bitr4i |
⊢ ( dom ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) = ∅ ↔ 𝐹 = ∅ ) |
29 |
28
|
necon3bii |
⊢ ( dom ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) ≠ ∅ ↔ 𝐹 ≠ ∅ ) |
30 |
25 29
|
sylib |
⊢ ( 𝜑 → 𝐹 ≠ ∅ ) |
31 |
1 2 3 4 5 6 7 8 9 10
|
minveclem4c |
⊢ ( 𝜑 → 𝑆 ∈ ℝ ) |
32 |
31
|
resqcld |
⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℝ ) |
33 |
|
ltaddrp |
⊢ ( ( ( 𝑆 ↑ 2 ) ∈ ℝ ∧ 𝑟 ∈ ℝ+ ) → ( 𝑆 ↑ 2 ) < ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) |
34 |
32 33
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( 𝑆 ↑ 2 ) < ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) |
35 |
32
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( 𝑆 ↑ 2 ) ∈ ℝ ) |
36 |
|
rpre |
⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ ) |
37 |
36
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ ) |
38 |
35 37
|
readdcld |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑆 ↑ 2 ) + 𝑟 ) ∈ ℝ ) |
39 |
38
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑆 ↑ 2 ) + 𝑟 ) ∈ ℂ ) |
40 |
39
|
sqsqrtd |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ↑ 2 ) = ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) |
41 |
34 40
|
breqtrrd |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( 𝑆 ↑ 2 ) < ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ↑ 2 ) ) |
42 |
1 2 3 4 5 6 7 8 9
|
minveclem1 |
⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) ) |
43 |
42
|
simp1d |
⊢ ( 𝜑 → 𝑅 ⊆ ℝ ) |
44 |
43
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑅 ⊆ ℝ ) |
45 |
42
|
simp2d |
⊢ ( 𝜑 → 𝑅 ≠ ∅ ) |
46 |
45
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑅 ≠ ∅ ) |
47 |
|
0re |
⊢ 0 ∈ ℝ |
48 |
42
|
simp3d |
⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) |
49 |
|
breq1 |
⊢ ( 𝑦 = 0 → ( 𝑦 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) ) |
50 |
49
|
ralbidv |
⊢ ( 𝑦 = 0 → ( ∀ 𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) ) |
51 |
50
|
rspcev |
⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 ) |
52 |
47 48 51
|
sylancr |
⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 ) |
53 |
52
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 ) |
54 |
|
infrecl |
⊢ ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ ) |
55 |
44 46 53 54
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ ) |
56 |
10 55
|
eqeltrid |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑆 ∈ ℝ ) |
57 |
|
0red |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 0 ∈ ℝ ) |
58 |
56
|
sqge0d |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 0 ≤ ( 𝑆 ↑ 2 ) ) |
59 |
57 35 38 58 34
|
lelttrd |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 0 < ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) |
60 |
57 38 59
|
ltled |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 0 ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) |
61 |
38 60
|
resqrtcld |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ∈ ℝ ) |
62 |
48
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) |
63 |
|
infregelb |
⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 ) ∧ 0 ∈ ℝ ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) ) |
64 |
44 46 53 57 63
|
syl31anc |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) ) |
65 |
62 64
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 0 ≤ inf ( 𝑅 , ℝ , < ) ) |
66 |
65 10
|
breqtrrdi |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 0 ≤ 𝑆 ) |
67 |
38 60
|
sqrtge0d |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 0 ≤ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ) |
68 |
56 61 66 67
|
lt2sqd |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( 𝑆 < ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ↔ ( 𝑆 ↑ 2 ) < ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ↑ 2 ) ) ) |
69 |
41 68
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑆 < ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ) |
70 |
56 61
|
ltnled |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( 𝑆 < ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ↔ ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ 𝑆 ) ) |
71 |
69 70
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ 𝑆 ) |
72 |
10
|
breq2i |
⊢ ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ 𝑆 ↔ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ inf ( 𝑅 , ℝ , < ) ) |
73 |
|
infregelb |
⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 ) ∧ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ∈ ℝ ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ 𝑤 ) ) |
74 |
44 46 53 61 73
|
syl31anc |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ 𝑤 ) ) |
75 |
9
|
raleqi |
⊢ ( ∀ 𝑤 ∈ 𝑅 ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ 𝑤 ↔ ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ 𝑤 ) |
76 |
|
fvex |
⊢ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ V |
77 |
76
|
rgenw |
⊢ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ V |
78 |
|
eqid |
⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) |
79 |
|
breq2 |
⊢ ( 𝑤 = ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ 𝑤 ↔ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) |
80 |
78 79
|
ralrnmptw |
⊢ ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ V → ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) |
81 |
77 80
|
ax-mp |
⊢ ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) |
82 |
75 81
|
bitri |
⊢ ( ∀ 𝑤 ∈ 𝑅 ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) |
83 |
74 82
|
bitrdi |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) |
84 |
72 83
|
syl5bb |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ 𝑆 ↔ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) |
85 |
71 84
|
mtbid |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ¬ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) |
86 |
|
rexnal |
⊢ ( ∃ 𝑦 ∈ 𝑌 ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ↔ ¬ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) |
87 |
85 86
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑦 ∈ 𝑌 ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) |
88 |
61
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ∈ ℝ ) |
89 |
|
cphngp |
⊢ ( 𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp ) |
90 |
4 89
|
syl |
⊢ ( 𝜑 → 𝑈 ∈ NrmGrp ) |
91 |
|
ngpms |
⊢ ( 𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp ) |
92 |
1 11
|
msmet |
⊢ ( 𝑈 ∈ MetSp → 𝐷 ∈ ( Met ‘ 𝑋 ) ) |
93 |
90 91 92
|
3syl |
⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) ) |
94 |
93
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) ) |
95 |
7
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 ) |
96 |
|
eqid |
⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 ) |
97 |
1 96
|
lssss |
⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → 𝑌 ⊆ 𝑋 ) |
98 |
14 97
|
syl |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑌 ⊆ 𝑋 ) |
99 |
98
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑋 ) |
100 |
|
metcl |
⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 𝐷 𝑦 ) ∈ ℝ ) |
101 |
94 95 99 100
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑦 ) ∈ ℝ ) |
102 |
67
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → 0 ≤ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ) |
103 |
|
metge0 |
⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝑦 ) ) |
104 |
94 95 99 103
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → 0 ≤ ( 𝐴 𝐷 𝑦 ) ) |
105 |
88 101 102 104
|
le2sqd |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝐴 𝐷 𝑦 ) ↔ ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ↑ 2 ) ≤ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ) ) |
106 |
11
|
oveqi |
⊢ ( 𝐴 𝐷 𝑦 ) = ( 𝐴 ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) 𝑦 ) |
107 |
95 99
|
ovresd |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) 𝑦 ) = ( 𝐴 ( dist ‘ 𝑈 ) 𝑦 ) ) |
108 |
106 107
|
syl5eq |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑦 ) = ( 𝐴 ( dist ‘ 𝑈 ) 𝑦 ) ) |
109 |
90
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → 𝑈 ∈ NrmGrp ) |
110 |
|
eqid |
⊢ ( dist ‘ 𝑈 ) = ( dist ‘ 𝑈 ) |
111 |
3 1 2 110
|
ngpds |
⊢ ( ( 𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 ( dist ‘ 𝑈 ) 𝑦 ) = ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) |
112 |
109 95 99 111
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ( dist ‘ 𝑈 ) 𝑦 ) = ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) |
113 |
108 112
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) |
114 |
113
|
breq2d |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝐴 𝐷 𝑦 ) ↔ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) |
115 |
40
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ↑ 2 ) = ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) |
116 |
115
|
breq1d |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ↑ 2 ) ≤ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ↔ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ≤ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ) ) |
117 |
105 114 116
|
3bitr3d |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ↔ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ≤ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ) ) |
118 |
117
|
notbid |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ↔ ¬ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ≤ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ) ) |
119 |
38
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑆 ↑ 2 ) + 𝑟 ) ∈ ℝ ) |
120 |
101
|
resqcld |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ∈ ℝ ) |
121 |
119 120
|
letrid |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( 𝑆 ↑ 2 ) + 𝑟 ) ≤ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ∨ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ) |
122 |
121
|
ord |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( ¬ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ≤ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) → ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ) |
123 |
118 122
|
sylbid |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) → ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ) |
124 |
123
|
reximdva |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ 𝑌 ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) → ∃ 𝑦 ∈ 𝑌 ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ) |
125 |
87 124
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑦 ∈ 𝑌 ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) |
126 |
|
rabn0 |
⊢ ( { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ≠ ∅ ↔ ∃ 𝑦 ∈ 𝑌 ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) |
127 |
125 126
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ≠ ∅ ) |
128 |
127
|
necomd |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∅ ≠ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) |
129 |
128
|
neneqd |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ¬ ∅ = { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) |
130 |
129
|
nrexdv |
⊢ ( 𝜑 → ¬ ∃ 𝑟 ∈ ℝ+ ∅ = { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) |
131 |
12
|
eleq2i |
⊢ ( ∅ ∈ 𝐹 ↔ ∅ ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) ) |
132 |
|
0ex |
⊢ ∅ ∈ V |
133 |
22
|
elrnmpt |
⊢ ( ∅ ∈ V → ( ∅ ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) ↔ ∃ 𝑟 ∈ ℝ+ ∅ = { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) ) |
134 |
132 133
|
ax-mp |
⊢ ( ∅ ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) ↔ ∃ 𝑟 ∈ ℝ+ ∅ = { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) |
135 |
131 134
|
bitri |
⊢ ( ∅ ∈ 𝐹 ↔ ∃ 𝑟 ∈ ℝ+ ∅ = { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) |
136 |
130 135
|
sylnibr |
⊢ ( 𝜑 → ¬ ∅ ∈ 𝐹 ) |
137 |
|
df-nel |
⊢ ( ∅ ∉ 𝐹 ↔ ¬ ∅ ∈ 𝐹 ) |
138 |
136 137
|
sylibr |
⊢ ( 𝜑 → ∅ ∉ 𝐹 ) |
139 |
56
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → 𝑆 ∈ ℝ ) |
140 |
139
|
resqcld |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑆 ↑ 2 ) ∈ ℝ ) |
141 |
37
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → 𝑟 ∈ ℝ ) |
142 |
120 140 141
|
lesubadd2d |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 ↔ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) ) |
143 |
142
|
rabbidva |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } = { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) |
144 |
143
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) = ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) ) |
145 |
144
|
rneqd |
⊢ ( 𝜑 → ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) = ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) ) |
146 |
12 145
|
eqtr4id |
⊢ ( 𝜑 → 𝐹 = ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) ) |
147 |
146
|
eleq2d |
⊢ ( 𝜑 → ( 𝑢 ∈ 𝐹 ↔ 𝑢 ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) ) ) |
148 |
|
breq2 |
⊢ ( 𝑟 = 𝑠 → ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 ↔ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 ) ) |
149 |
148
|
rabbidv |
⊢ ( 𝑟 = 𝑠 → { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ) |
150 |
149
|
cbvmptv |
⊢ ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) = ( 𝑠 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ) |
151 |
150
|
elrnmpt |
⊢ ( 𝑢 ∈ V → ( 𝑢 ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) ↔ ∃ 𝑠 ∈ ℝ+ 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ) ) |
152 |
151
|
elv |
⊢ ( 𝑢 ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) ↔ ∃ 𝑠 ∈ ℝ+ 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ) |
153 |
147 152
|
bitrdi |
⊢ ( 𝜑 → ( 𝑢 ∈ 𝐹 ↔ ∃ 𝑠 ∈ ℝ+ 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ) ) |
154 |
146
|
eleq2d |
⊢ ( 𝜑 → ( 𝑣 ∈ 𝐹 ↔ 𝑣 ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) ) ) |
155 |
|
breq2 |
⊢ ( 𝑟 = 𝑡 → ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 ↔ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 ) ) |
156 |
155
|
rabbidv |
⊢ ( 𝑟 = 𝑡 → { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) |
157 |
156
|
cbvmptv |
⊢ ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) = ( 𝑡 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) |
158 |
157
|
elrnmpt |
⊢ ( 𝑣 ∈ V → ( 𝑣 ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) ↔ ∃ 𝑡 ∈ ℝ+ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) ) |
159 |
158
|
elv |
⊢ ( 𝑣 ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) ↔ ∃ 𝑡 ∈ ℝ+ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) |
160 |
154 159
|
bitrdi |
⊢ ( 𝜑 → ( 𝑣 ∈ 𝐹 ↔ ∃ 𝑡 ∈ ℝ+ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) ) |
161 |
153 160
|
anbi12d |
⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐹 ∧ 𝑣 ∈ 𝐹 ) ↔ ( ∃ 𝑠 ∈ ℝ+ 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ∧ ∃ 𝑡 ∈ ℝ+ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) ) ) |
162 |
|
reeanv |
⊢ ( ∃ 𝑠 ∈ ℝ+ ∃ 𝑡 ∈ ℝ+ ( 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) ↔ ( ∃ 𝑠 ∈ ℝ+ 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ∧ ∃ 𝑡 ∈ ℝ+ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) ) |
163 |
93
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) ) |
164 |
7
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 ) |
165 |
5 97
|
syl |
⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 ) |
166 |
165
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) → 𝑌 ⊆ 𝑋 ) |
167 |
166
|
sselda |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑋 ) |
168 |
163 164 167 100
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑦 ) ∈ ℝ ) |
169 |
168
|
resqcld |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ∈ ℝ ) |
170 |
32
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑆 ↑ 2 ) ∈ ℝ ) |
171 |
169 170
|
resubcld |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ∈ ℝ ) |
172 |
|
simplrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝑠 ∈ ℝ+ ) |
173 |
172
|
rpred |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝑠 ∈ ℝ ) |
174 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝑡 ∈ ℝ+ ) |
175 |
174
|
rpred |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝑡 ∈ ℝ ) |
176 |
|
lemin |
⊢ ( ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) ↔ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 ) ) ) |
177 |
171 173 175 176
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) ↔ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 ) ) ) |
178 |
177
|
rabbidva |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) → { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) } = { 𝑦 ∈ 𝑌 ∣ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 ) } ) |
179 |
|
ifcl |
⊢ ( ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) → if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) ∈ ℝ+ ) |
180 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) ) |
181 |
|
rabexg |
⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) } ∈ V ) |
182 |
180 181
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) → { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) } ∈ V ) |
183 |
|
eqid |
⊢ ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) = ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) |
184 |
|
breq2 |
⊢ ( 𝑟 = if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) → ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 ↔ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) ) ) |
185 |
184
|
rabbidv |
⊢ ( 𝑟 = if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) → { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) } ) |
186 |
183 185
|
elrnmpt1s |
⊢ ( ( if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) ∈ ℝ+ ∧ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) } ∈ V ) → { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) } ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) ) |
187 |
179 182 186
|
syl2an2 |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) → { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) } ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) ) |
188 |
146
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) → 𝐹 = ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑟 } ) ) |
189 |
187 188
|
eleqtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) → { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ if ( 𝑠 ≤ 𝑡 , 𝑠 , 𝑡 ) } ∈ 𝐹 ) |
190 |
178 189
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) → { 𝑦 ∈ 𝑌 ∣ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 ) } ∈ 𝐹 ) |
191 |
|
ineq12 |
⊢ ( ( 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) → ( 𝑢 ∩ 𝑣 ) = ( { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ∩ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) ) |
192 |
|
inrab |
⊢ ( { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ∩ { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) = { 𝑦 ∈ 𝑌 ∣ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 ) } |
193 |
191 192
|
eqtrdi |
⊢ ( ( 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) → ( 𝑢 ∩ 𝑣 ) = { 𝑦 ∈ 𝑌 ∣ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 ) } ) |
194 |
193
|
eleq1d |
⊢ ( ( 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) → ( ( 𝑢 ∩ 𝑣 ) ∈ 𝐹 ↔ { 𝑦 ∈ 𝑌 ∣ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 ) } ∈ 𝐹 ) ) |
195 |
190 194
|
syl5ibrcom |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) → ( ( 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝐹 ) ) |
196 |
|
vex |
⊢ 𝑢 ∈ V |
197 |
196
|
inex1 |
⊢ ( 𝑢 ∩ 𝑣 ) ∈ V |
198 |
197
|
pwid |
⊢ ( 𝑢 ∩ 𝑣 ) ∈ 𝒫 ( 𝑢 ∩ 𝑣 ) |
199 |
|
inelcm |
⊢ ( ( ( 𝑢 ∩ 𝑣 ) ∈ 𝐹 ∧ ( 𝑢 ∩ 𝑣 ) ∈ 𝒫 ( 𝑢 ∩ 𝑣 ) ) → ( 𝐹 ∩ 𝒫 ( 𝑢 ∩ 𝑣 ) ) ≠ ∅ ) |
200 |
198 199
|
mpan2 |
⊢ ( ( 𝑢 ∩ 𝑣 ) ∈ 𝐹 → ( 𝐹 ∩ 𝒫 ( 𝑢 ∩ 𝑣 ) ) ≠ ∅ ) |
201 |
195 200
|
syl6 |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) ) → ( ( 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) → ( 𝐹 ∩ 𝒫 ( 𝑢 ∩ 𝑣 ) ) ≠ ∅ ) ) |
202 |
201
|
rexlimdvva |
⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ℝ+ ∃ 𝑡 ∈ ℝ+ ( 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) → ( 𝐹 ∩ 𝒫 ( 𝑢 ∩ 𝑣 ) ) ≠ ∅ ) ) |
203 |
162 202
|
syl5bir |
⊢ ( 𝜑 → ( ( ∃ 𝑠 ∈ ℝ+ 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑠 } ∧ ∃ 𝑡 ∈ ℝ+ 𝑣 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ≤ 𝑡 } ) → ( 𝐹 ∩ 𝒫 ( 𝑢 ∩ 𝑣 ) ) ≠ ∅ ) ) |
204 |
161 203
|
sylbid |
⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐹 ∧ 𝑣 ∈ 𝐹 ) → ( 𝐹 ∩ 𝒫 ( 𝑢 ∩ 𝑣 ) ) ≠ ∅ ) ) |
205 |
204
|
ralrimivv |
⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐹 ∀ 𝑣 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑢 ∩ 𝑣 ) ) ≠ ∅ ) |
206 |
30 138 205
|
3jca |
⊢ ( 𝜑 → ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑢 ∈ 𝐹 ∀ 𝑣 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑢 ∩ 𝑣 ) ) ≠ ∅ ) ) |
207 |
|
isfbas |
⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ↔ ( 𝐹 ⊆ 𝒫 𝑌 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑢 ∈ 𝐹 ∀ 𝑣 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑢 ∩ 𝑣 ) ) ≠ ∅ ) ) ) ) |
208 |
5 207
|
syl |
⊢ ( 𝜑 → ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ↔ ( 𝐹 ⊆ 𝒫 𝑌 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑢 ∈ 𝐹 ∀ 𝑣 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑢 ∩ 𝑣 ) ) ≠ ∅ ) ) ) ) |
209 |
20 206 208
|
mpbir2and |
⊢ ( 𝜑 → 𝐹 ∈ ( fBas ‘ 𝑌 ) ) |