Proof of Theorem nlmvscnlem1
Step | Hyp | Ref
| Expression |
1 | | nlmvscn.t |
. . . 4
⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) |
2 | | nlmvscn.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
3 | 2 | rphalfcld 12527 |
. . . . 5
⊢ (𝜑 → (𝑅 / 2) ∈
ℝ+) |
4 | | nlmvscn.w |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ NrmMod) |
5 | | nlmvscn.f |
. . . . . . . . 9
⊢ 𝐹 = (Scalar‘𝑊) |
6 | 5 | nlmngp2 23434 |
. . . . . . . 8
⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp) |
7 | 4, 6 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ NrmGrp) |
8 | | nlmvscn.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝐾) |
9 | | nlmvscn.k |
. . . . . . . 8
⊢ 𝐾 = (Base‘𝐹) |
10 | | nlmvscn.a |
. . . . . . . 8
⊢ 𝐴 = (norm‘𝐹) |
11 | 9, 10 | nmcl 23370 |
. . . . . . 7
⊢ ((𝐹 ∈ NrmGrp ∧ 𝐵 ∈ 𝐾) → (𝐴‘𝐵) ∈ ℝ) |
12 | 7, 8, 11 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝐵) ∈ ℝ) |
13 | 9, 10 | nmge0 23371 |
. . . . . . 7
⊢ ((𝐹 ∈ NrmGrp ∧ 𝐵 ∈ 𝐾) → 0 ≤ (𝐴‘𝐵)) |
14 | 7, 8, 13 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝐴‘𝐵)) |
15 | 12, 14 | ge0p1rpd 12545 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝐵) + 1) ∈
ℝ+) |
16 | 3, 15 | rpdivcld 12532 |
. . . 4
⊢ (𝜑 → ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) ∈
ℝ+) |
17 | 1, 16 | eqeltrid 2837 |
. . 3
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
18 | | nlmvscn.u |
. . . 4
⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) |
19 | | nlmngp 23431 |
. . . . . . . . 9
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) |
20 | 4, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ NrmGrp) |
21 | | nlmvscn.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
22 | | nlmvscn.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑊) |
23 | | nlmvscn.n |
. . . . . . . . 9
⊢ 𝑁 = (norm‘𝑊) |
24 | 22, 23 | nmcl 23370 |
. . . . . . . 8
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) ∈ ℝ) |
25 | 20, 21, 24 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘𝑋) ∈ ℝ) |
26 | 17 | rpred 12515 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ℝ) |
27 | 25, 26 | readdcld 10749 |
. . . . . 6
⊢ (𝜑 → ((𝑁‘𝑋) + 𝑇) ∈ ℝ) |
28 | | 0red 10723 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
29 | 22, 23 | nmge0 23371 |
. . . . . . . 8
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉) → 0 ≤ (𝑁‘𝑋)) |
30 | 20, 21, 29 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑁‘𝑋)) |
31 | 25, 17 | ltaddrpd 12548 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘𝑋) < ((𝑁‘𝑋) + 𝑇)) |
32 | 28, 25, 27, 30, 31 | lelttrd 10877 |
. . . . . 6
⊢ (𝜑 → 0 < ((𝑁‘𝑋) + 𝑇)) |
33 | 27, 32 | elrpd 12512 |
. . . . 5
⊢ (𝜑 → ((𝑁‘𝑋) + 𝑇) ∈
ℝ+) |
34 | 3, 33 | rpdivcld 12532 |
. . . 4
⊢ (𝜑 → ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) ∈
ℝ+) |
35 | 18, 34 | eqeltrid 2837 |
. . 3
⊢ (𝜑 → 𝑈 ∈
ℝ+) |
36 | 17, 35 | ifcld 4461 |
. 2
⊢ (𝜑 → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∈
ℝ+) |
37 | | nlmvscn.d |
. . . . 5
⊢ 𝐷 = (dist‘𝑊) |
38 | | nlmvscn.e |
. . . . 5
⊢ 𝐸 = (dist‘𝐹) |
39 | | nlmvscn.s |
. . . . 5
⊢ · = (
·𝑠 ‘𝑊) |
40 | 4 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑊 ∈ NrmMod) |
41 | 2 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑅 ∈
ℝ+) |
42 | 8 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝐵 ∈ 𝐾) |
43 | 21 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑋 ∈ 𝑉) |
44 | | simprll 779 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑥 ∈ 𝐾) |
45 | | simprlr 780 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑦 ∈ 𝑉) |
46 | 7 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝐹 ∈ NrmGrp) |
47 | | ngpms 23354 |
. . . . . . . 8
⊢ (𝐹 ∈ NrmGrp → 𝐹 ∈ MetSp) |
48 | 46, 47 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝐹 ∈ MetSp) |
49 | 9, 38 | mscl 23215 |
. . . . . . 7
⊢ ((𝐹 ∈ MetSp ∧ 𝐵 ∈ 𝐾 ∧ 𝑥 ∈ 𝐾) → (𝐵𝐸𝑥) ∈ ℝ) |
50 | 48, 42, 44, 49 | syl3anc 1372 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝐵𝐸𝑥) ∈ ℝ) |
51 | 36 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∈
ℝ+) |
52 | 51 | rpred 12515 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∈ ℝ) |
53 | 35 | rpred 12515 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ ℝ) |
54 | 53 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑈 ∈ ℝ) |
55 | | simprrl 781 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) |
56 | 26 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑇 ∈ ℝ) |
57 | | min2 12667 |
. . . . . . 7
⊢ ((𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ≤ 𝑈) |
58 | 56, 54, 57 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ≤ 𝑈) |
59 | 50, 52, 54, 55, 58 | ltletrd 10879 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝐵𝐸𝑥) < 𝑈) |
60 | | ngpms 23354 |
. . . . . . . . 9
⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp) |
61 | 20, 60 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ MetSp) |
62 | 61 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑊 ∈ MetSp) |
63 | 22, 37 | mscl 23215 |
. . . . . . 7
⊢ ((𝑊 ∈ MetSp ∧ 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑋𝐷𝑦) ∈ ℝ) |
64 | 62, 43, 45, 63 | syl3anc 1372 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝑋𝐷𝑦) ∈ ℝ) |
65 | | simprrr 782 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) |
66 | | min1 12666 |
. . . . . . 7
⊢ ((𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ≤ 𝑇) |
67 | 56, 54, 66 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ≤ 𝑇) |
68 | 64, 52, 56, 65, 67 | ltletrd 10879 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝑋𝐷𝑦) < 𝑇) |
69 | 5, 22, 9, 37, 38, 23, 10, 39, 1, 18, 40, 41, 42, 43, 44, 45, 59, 68 | nlmvscnlem2 23439 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅) |
70 | 69 | expr 460 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉)) → (((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) |
71 | 70 | ralrimivva 3103 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) |
72 | | breq2 5035 |
. . . . . 6
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → ((𝐵𝐸𝑥) < 𝑟 ↔ (𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈))) |
73 | | breq2 5035 |
. . . . . 6
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → ((𝑋𝐷𝑦) < 𝑟 ↔ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈))) |
74 | 72, 73 | anbi12d 634 |
. . . . 5
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) ↔ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) |
75 | 74 | imbi1d 345 |
. . . 4
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → ((((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅) ↔ (((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅))) |
76 | 75 | 2ralbidv 3111 |
. . 3
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → (∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅) ↔ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅))) |
77 | 76 | rspcev 3527 |
. 2
⊢
((if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∈ ℝ+ ∧
∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) |
78 | 36, 71, 77 | syl2anc 587 |
1
⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) |