Proof of Theorem nlmvscnlem1
| Step | Hyp | Ref
| Expression |
| 1 | | nlmvscn.t |
. . . 4
⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) |
| 2 | | nlmvscn.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
| 3 | 2 | rphalfcld 13089 |
. . . . 5
⊢ (𝜑 → (𝑅 / 2) ∈
ℝ+) |
| 4 | | nlmvscn.w |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ NrmMod) |
| 5 | | nlmvscn.f |
. . . . . . . . 9
⊢ 𝐹 = (Scalar‘𝑊) |
| 6 | 5 | nlmngp2 24701 |
. . . . . . . 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 24629 |
. . . . . . 7
⊢ ((𝐹 ∈ NrmGrp ∧ 𝐵 ∈ 𝐾) → (𝐴‘𝐵) ∈ ℝ) |
| 12 | 7, 8, 11 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝐵) ∈ ℝ) |
| 13 | 9, 10 | nmge0 24630 |
. . . . . . 7
⊢ ((𝐹 ∈ NrmGrp ∧ 𝐵 ∈ 𝐾) → 0 ≤ (𝐴‘𝐵)) |
| 14 | 7, 8, 13 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝐴‘𝐵)) |
| 15 | 12, 14 | ge0p1rpd 13107 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝐵) + 1) ∈
ℝ+) |
| 16 | 3, 15 | rpdivcld 13094 |
. . . 4
⊢ (𝜑 → ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) ∈
ℝ+) |
| 17 | 1, 16 | eqeltrid 2845 |
. . 3
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
| 18 | | nlmvscn.u |
. . . 4
⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) |
| 19 | | nlmngp 24698 |
. . . . . . . . 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 24629 |
. . . . . . . 8
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) ∈ ℝ) |
| 25 | 20, 21, 24 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘𝑋) ∈ ℝ) |
| 26 | 17 | rpred 13077 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 27 | 25, 26 | readdcld 11290 |
. . . . . 6
⊢ (𝜑 → ((𝑁‘𝑋) + 𝑇) ∈ ℝ) |
| 28 | | 0red 11264 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
| 29 | 22, 23 | nmge0 24630 |
. . . . . . . 8
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉) → 0 ≤ (𝑁‘𝑋)) |
| 30 | 20, 21, 29 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑁‘𝑋)) |
| 31 | 25, 17 | ltaddrpd 13110 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘𝑋) < ((𝑁‘𝑋) + 𝑇)) |
| 32 | 28, 25, 27, 30, 31 | lelttrd 11419 |
. . . . . 6
⊢ (𝜑 → 0 < ((𝑁‘𝑋) + 𝑇)) |
| 33 | 27, 32 | elrpd 13074 |
. . . . 5
⊢ (𝜑 → ((𝑁‘𝑋) + 𝑇) ∈
ℝ+) |
| 34 | 3, 33 | rpdivcld 13094 |
. . . 4
⊢ (𝜑 → ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) ∈
ℝ+) |
| 35 | 18, 34 | eqeltrid 2845 |
. . 3
⊢ (𝜑 → 𝑈 ∈
ℝ+) |
| 36 | 17, 35 | ifcld 4572 |
. 2
⊢ (𝜑 → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∈
ℝ+) |
| 37 | | nlmvscn.d |
. . . . 5
⊢ 𝐷 = (dist‘𝑊) |
| 38 | | nlmvscn.e |
. . . . 5
⊢ 𝐸 = (dist‘𝐹) |
| 39 | | nlmvscn.s |
. . . . 5
⊢ · = (
·𝑠 ‘𝑊) |
| 40 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑊 ∈ NrmMod) |
| 41 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑅 ∈
ℝ+) |
| 42 | 8 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝐵 ∈ 𝐾) |
| 43 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑋 ∈ 𝑉) |
| 44 | | simprll 779 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑥 ∈ 𝐾) |
| 45 | | simprlr 780 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑦 ∈ 𝑉) |
| 46 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝐹 ∈ NrmGrp) |
| 47 | | ngpms 24613 |
. . . . . . . 8
⊢ (𝐹 ∈ NrmGrp → 𝐹 ∈ MetSp) |
| 48 | 46, 47 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝐹 ∈ MetSp) |
| 49 | 9, 38 | mscl 24471 |
. . . . . . 7
⊢ ((𝐹 ∈ MetSp ∧ 𝐵 ∈ 𝐾 ∧ 𝑥 ∈ 𝐾) → (𝐵𝐸𝑥) ∈ ℝ) |
| 50 | 48, 42, 44, 49 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝐵𝐸𝑥) ∈ ℝ) |
| 51 | 36 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∈
ℝ+) |
| 52 | 51 | rpred 13077 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∈ ℝ) |
| 53 | 35 | rpred 13077 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ ℝ) |
| 54 | 53 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑈 ∈ ℝ) |
| 55 | | simprrl 781 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) |
| 56 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑇 ∈ ℝ) |
| 57 | | min2 13232 |
. . . . . . 7
⊢ ((𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ≤ 𝑈) |
| 58 | 56, 54, 57 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ≤ 𝑈) |
| 59 | 50, 52, 54, 55, 58 | ltletrd 11421 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝐵𝐸𝑥) < 𝑈) |
| 60 | | ngpms 24613 |
. . . . . . . . 9
⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp) |
| 61 | 20, 60 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ MetSp) |
| 62 | 61 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑊 ∈ MetSp) |
| 63 | 22, 37 | mscl 24471 |
. . . . . . 7
⊢ ((𝑊 ∈ MetSp ∧ 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑋𝐷𝑦) ∈ ℝ) |
| 64 | 62, 43, 45, 63 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝑋𝐷𝑦) ∈ ℝ) |
| 65 | | simprrr 782 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) |
| 66 | | min1 13231 |
. . . . . . 7
⊢ ((𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ≤ 𝑇) |
| 67 | 56, 54, 66 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ≤ 𝑇) |
| 68 | 64, 52, 56, 65, 67 | ltletrd 11421 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝑋𝐷𝑦) < 𝑇) |
| 69 | 5, 22, 9, 37, 38, 23, 10, 39, 1, 18, 40, 41, 42, 43, 44, 45, 59, 68 | nlmvscnlem2 24706 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅) |
| 70 | 69 | expr 456 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉)) → (((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) |
| 71 | 70 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) |
| 72 | | breq2 5147 |
. . . . . 6
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → ((𝐵𝐸𝑥) < 𝑟 ↔ (𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈))) |
| 73 | | breq2 5147 |
. . . . . 6
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → ((𝑋𝐷𝑦) < 𝑟 ↔ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈))) |
| 74 | 72, 73 | anbi12d 632 |
. . . . 5
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) ↔ ((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) |
| 75 | 74 | imbi1d 341 |
. . . 4
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → ((((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅) ↔ (((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅))) |
| 76 | 75 | 2ralbidv 3221 |
. . 3
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → (∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅) ↔ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅))) |
| 77 | 76 | rspcev 3622 |
. 2
⊢
((if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∈ ℝ+ ∧
∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝑋𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) |
| 78 | 36, 71, 77 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) |