Proof of Theorem nlmvscnlem2
| Step | Hyp | Ref
| Expression |
| 1 | | nlmvscn.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ NrmMod) |
| 2 | | nlmngp 24698 |
. . . . 5
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ NrmGrp) |
| 4 | | ngpms 24613 |
. . . 4
⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp) |
| 5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → 𝑊 ∈ MetSp) |
| 6 | | nlmlmod 24699 |
. . . . 5
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod) |
| 7 | 1, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 8 | | nlmvscn.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝐾) |
| 9 | | nlmvscn.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 10 | | nlmvscn.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
| 11 | | nlmvscn.f |
. . . . 5
⊢ 𝐹 = (Scalar‘𝑊) |
| 12 | | nlmvscn.s |
. . . . 5
⊢ · = (
·𝑠 ‘𝑊) |
| 13 | | nlmvscn.k |
. . . . 5
⊢ 𝐾 = (Base‘𝐹) |
| 14 | 10, 11, 12, 13 | lmodvscl 20876 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝐵 · 𝑋) ∈ 𝑉) |
| 15 | 7, 8, 9, 14 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝐵 · 𝑋) ∈ 𝑉) |
| 16 | | nlmvscn.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝐾) |
| 17 | | nlmvscn.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 18 | 10, 11, 12, 13 | lmodvscl 20876 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐶 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝐶 · 𝑌) ∈ 𝑉) |
| 19 | 7, 16, 17, 18 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝐶 · 𝑌) ∈ 𝑉) |
| 20 | | nlmvscn.d |
. . . 4
⊢ 𝐷 = (dist‘𝑊) |
| 21 | 10, 20 | mscl 24471 |
. . 3
⊢ ((𝑊 ∈ MetSp ∧ (𝐵 · 𝑋) ∈ 𝑉 ∧ (𝐶 · 𝑌) ∈ 𝑉) → ((𝐵 · 𝑋)𝐷(𝐶 · 𝑌)) ∈ ℝ) |
| 22 | 5, 15, 19, 21 | syl3anc 1373 |
. 2
⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐶 · 𝑌)) ∈ ℝ) |
| 23 | 10, 11, 12, 13 | lmodvscl 20876 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝐵 · 𝑌) ∈ 𝑉) |
| 24 | 7, 8, 17, 23 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝐵 · 𝑌) ∈ 𝑉) |
| 25 | 10, 20 | mscl 24471 |
. . . 4
⊢ ((𝑊 ∈ MetSp ∧ (𝐵 · 𝑋) ∈ 𝑉 ∧ (𝐵 · 𝑌) ∈ 𝑉) → ((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) ∈ ℝ) |
| 26 | 5, 15, 24, 25 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) ∈ ℝ) |
| 27 | 10, 20 | mscl 24471 |
. . . 4
⊢ ((𝑊 ∈ MetSp ∧ (𝐵 · 𝑌) ∈ 𝑉 ∧ (𝐶 · 𝑌) ∈ 𝑉) → ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌)) ∈ ℝ) |
| 28 | 5, 24, 19, 27 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌)) ∈ ℝ) |
| 29 | 26, 28 | readdcld 11290 |
. 2
⊢ (𝜑 → (((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) + ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌))) ∈ ℝ) |
| 30 | | nlmvscn.r |
. . 3
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
| 31 | 30 | rpred 13077 |
. 2
⊢ (𝜑 → 𝑅 ∈ ℝ) |
| 32 | 10, 20 | mstri 24479 |
. . 3
⊢ ((𝑊 ∈ MetSp ∧ ((𝐵 · 𝑋) ∈ 𝑉 ∧ (𝐶 · 𝑌) ∈ 𝑉 ∧ (𝐵 · 𝑌) ∈ 𝑉)) → ((𝐵 · 𝑋)𝐷(𝐶 · 𝑌)) ≤ (((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) + ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌)))) |
| 33 | 5, 15, 19, 24, 32 | syl13anc 1374 |
. 2
⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐶 · 𝑌)) ≤ (((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) + ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌)))) |
| 34 | 11 | nlmngp2 24701 |
. . . . . . . . 9
⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp) |
| 35 | 1, 34 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ NrmGrp) |
| 36 | | nlmvscn.a |
. . . . . . . . 9
⊢ 𝐴 = (norm‘𝐹) |
| 37 | 13, 36 | nmcl 24629 |
. . . . . . . 8
⊢ ((𝐹 ∈ NrmGrp ∧ 𝐵 ∈ 𝐾) → (𝐴‘𝐵) ∈ ℝ) |
| 38 | 35, 8, 37 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴‘𝐵) ∈ ℝ) |
| 39 | 13, 36 | nmge0 24630 |
. . . . . . . 8
⊢ ((𝐹 ∈ NrmGrp ∧ 𝐵 ∈ 𝐾) → 0 ≤ (𝐴‘𝐵)) |
| 40 | 35, 8, 39 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝐴‘𝐵)) |
| 41 | 38, 40 | ge0p1rpd 13107 |
. . . . . 6
⊢ (𝜑 → ((𝐴‘𝐵) + 1) ∈
ℝ+) |
| 42 | 41 | rpred 13077 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝐵) + 1) ∈ ℝ) |
| 43 | 10, 20 | mscl 24471 |
. . . . . 6
⊢ ((𝑊 ∈ MetSp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋𝐷𝑌) ∈ ℝ) |
| 44 | 5, 9, 17, 43 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑋𝐷𝑌) ∈ ℝ) |
| 45 | 42, 44 | remulcld 11291 |
. . . 4
⊢ (𝜑 → (((𝐴‘𝐵) + 1) · (𝑋𝐷𝑌)) ∈ ℝ) |
| 46 | 31 | rehalfcld 12513 |
. . . 4
⊢ (𝜑 → (𝑅 / 2) ∈ ℝ) |
| 47 | 10, 12, 11, 13, 20, 36 | nlmdsdi 24702 |
. . . . . 6
⊢ ((𝑊 ∈ NrmMod ∧ (𝐵 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐴‘𝐵) · (𝑋𝐷𝑌)) = ((𝐵 · 𝑋)𝐷(𝐵 · 𝑌))) |
| 48 | 1, 8, 9, 17, 47 | syl13anc 1374 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝐵) · (𝑋𝐷𝑌)) = ((𝐵 · 𝑋)𝐷(𝐵 · 𝑌))) |
| 49 | | msxms 24464 |
. . . . . . . 8
⊢ (𝑊 ∈ MetSp → 𝑊 ∈
∞MetSp) |
| 50 | 5, 49 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ ∞MetSp) |
| 51 | 10, 20 | xmsge0 24473 |
. . . . . . 7
⊢ ((𝑊 ∈ ∞MetSp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 0 ≤ (𝑋𝐷𝑌)) |
| 52 | 50, 9, 17, 51 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝑋𝐷𝑌)) |
| 53 | 38 | lep1d 12199 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝐵) ≤ ((𝐴‘𝐵) + 1)) |
| 54 | 38, 42, 44, 52, 53 | lemul1ad 12207 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝐵) · (𝑋𝐷𝑌)) ≤ (((𝐴‘𝐵) + 1) · (𝑋𝐷𝑌))) |
| 55 | 48, 54 | eqbrtrrd 5167 |
. . . 4
⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) ≤ (((𝐴‘𝐵) + 1) · (𝑋𝐷𝑌))) |
| 56 | | nlmvscn.2 |
. . . . . 6
⊢ (𝜑 → (𝑋𝐷𝑌) < 𝑇) |
| 57 | | nlmvscn.t |
. . . . . 6
⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) |
| 58 | 56, 57 | breqtrdi 5184 |
. . . . 5
⊢ (𝜑 → (𝑋𝐷𝑌) < ((𝑅 / 2) / ((𝐴‘𝐵) + 1))) |
| 59 | 44, 46, 41 | ltmuldiv2d 13125 |
. . . . 5
⊢ (𝜑 → ((((𝐴‘𝐵) + 1) · (𝑋𝐷𝑌)) < (𝑅 / 2) ↔ (𝑋𝐷𝑌) < ((𝑅 / 2) / ((𝐴‘𝐵) + 1)))) |
| 60 | 58, 59 | mpbird 257 |
. . . 4
⊢ (𝜑 → (((𝐴‘𝐵) + 1) · (𝑋𝐷𝑌)) < (𝑅 / 2)) |
| 61 | 26, 45, 46, 55, 60 | lelttrd 11419 |
. . 3
⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) < (𝑅 / 2)) |
| 62 | | ngpms 24613 |
. . . . . . 7
⊢ (𝐹 ∈ NrmGrp → 𝐹 ∈ MetSp) |
| 63 | 35, 62 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ MetSp) |
| 64 | | nlmvscn.e |
. . . . . . 7
⊢ 𝐸 = (dist‘𝐹) |
| 65 | 13, 64 | mscl 24471 |
. . . . . 6
⊢ ((𝐹 ∈ MetSp ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝐾) → (𝐵𝐸𝐶) ∈ ℝ) |
| 66 | 63, 8, 16, 65 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝐵𝐸𝐶) ∈ ℝ) |
| 67 | | nlmvscn.n |
. . . . . . . 8
⊢ 𝑁 = (norm‘𝑊) |
| 68 | 10, 67 | nmcl 24629 |
. . . . . . 7
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) ∈ ℝ) |
| 69 | 3, 9, 68 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑁‘𝑋) ∈ ℝ) |
| 70 | 30 | rphalfcld 13089 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 / 2) ∈
ℝ+) |
| 71 | 70, 41 | rpdivcld 13094 |
. . . . . . . 8
⊢ (𝜑 → ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) ∈
ℝ+) |
| 72 | 57, 71 | eqeltrid 2845 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
| 73 | 72 | rpred 13077 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 74 | 69, 73 | readdcld 11290 |
. . . . 5
⊢ (𝜑 → ((𝑁‘𝑋) + 𝑇) ∈ ℝ) |
| 75 | 66, 74 | remulcld 11291 |
. . . 4
⊢ (𝜑 → ((𝐵𝐸𝐶) · ((𝑁‘𝑋) + 𝑇)) ∈ ℝ) |
| 76 | 10, 12, 11, 13, 20, 67, 64 | nlmdsdir 24703 |
. . . . . 6
⊢ ((𝑊 ∈ NrmMod ∧ (𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉)) → ((𝐵𝐸𝐶) · (𝑁‘𝑌)) = ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌))) |
| 77 | 1, 8, 16, 17, 76 | syl13anc 1374 |
. . . . 5
⊢ (𝜑 → ((𝐵𝐸𝐶) · (𝑁‘𝑌)) = ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌))) |
| 78 | 10, 67 | nmcl 24629 |
. . . . . . 7
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑌 ∈ 𝑉) → (𝑁‘𝑌) ∈ ℝ) |
| 79 | 3, 17, 78 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑁‘𝑌) ∈ ℝ) |
| 80 | | msxms 24464 |
. . . . . . . 8
⊢ (𝐹 ∈ MetSp → 𝐹 ∈
∞MetSp) |
| 81 | 63, 80 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ ∞MetSp) |
| 82 | 13, 64 | xmsge0 24473 |
. . . . . . 7
⊢ ((𝐹 ∈ ∞MetSp ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝐾) → 0 ≤ (𝐵𝐸𝐶)) |
| 83 | 81, 8, 16, 82 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝐵𝐸𝐶)) |
| 84 | 79, 69 | resubcld 11691 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁‘𝑌) − (𝑁‘𝑋)) ∈ ℝ) |
| 85 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(-g‘𝑊) = (-g‘𝑊) |
| 86 | 10, 67, 85 | nm2dif 24638 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ((𝑁‘𝑌) − (𝑁‘𝑋)) ≤ (𝑁‘(𝑌(-g‘𝑊)𝑋))) |
| 87 | 3, 17, 9, 86 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁‘𝑌) − (𝑁‘𝑋)) ≤ (𝑁‘(𝑌(-g‘𝑊)𝑋))) |
| 88 | 67, 10, 85, 20 | ngpdsr 24618 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋𝐷𝑌) = (𝑁‘(𝑌(-g‘𝑊)𝑋))) |
| 89 | 3, 9, 17, 88 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋𝐷𝑌) = (𝑁‘(𝑌(-g‘𝑊)𝑋))) |
| 90 | 87, 89 | breqtrrd 5171 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁‘𝑌) − (𝑁‘𝑋)) ≤ (𝑋𝐷𝑌)) |
| 91 | 44, 73, 56 | ltled 11409 |
. . . . . . . 8
⊢ (𝜑 → (𝑋𝐷𝑌) ≤ 𝑇) |
| 92 | 84, 44, 73, 90, 91 | letrd 11418 |
. . . . . . 7
⊢ (𝜑 → ((𝑁‘𝑌) − (𝑁‘𝑋)) ≤ 𝑇) |
| 93 | 79, 69, 73 | lesubadd2d 11862 |
. . . . . . 7
⊢ (𝜑 → (((𝑁‘𝑌) − (𝑁‘𝑋)) ≤ 𝑇 ↔ (𝑁‘𝑌) ≤ ((𝑁‘𝑋) + 𝑇))) |
| 94 | 92, 93 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝑁‘𝑌) ≤ ((𝑁‘𝑋) + 𝑇)) |
| 95 | 79, 74, 66, 83, 94 | lemul2ad 12208 |
. . . . 5
⊢ (𝜑 → ((𝐵𝐸𝐶) · (𝑁‘𝑌)) ≤ ((𝐵𝐸𝐶) · ((𝑁‘𝑋) + 𝑇))) |
| 96 | 77, 95 | eqbrtrrd 5167 |
. . . 4
⊢ (𝜑 → ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌)) ≤ ((𝐵𝐸𝐶) · ((𝑁‘𝑋) + 𝑇))) |
| 97 | | nlmvscn.1 |
. . . . . 6
⊢ (𝜑 → (𝐵𝐸𝐶) < 𝑈) |
| 98 | | nlmvscn.u |
. . . . . 6
⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) |
| 99 | 97, 98 | breqtrdi 5184 |
. . . . 5
⊢ (𝜑 → (𝐵𝐸𝐶) < ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇))) |
| 100 | | 0red 11264 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
| 101 | 10, 67 | nmge0 24630 |
. . . . . . . 8
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉) → 0 ≤ (𝑁‘𝑋)) |
| 102 | 3, 9, 101 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑁‘𝑋)) |
| 103 | 69, 72 | ltaddrpd 13110 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘𝑋) < ((𝑁‘𝑋) + 𝑇)) |
| 104 | 100, 69, 74, 102, 103 | lelttrd 11419 |
. . . . . 6
⊢ (𝜑 → 0 < ((𝑁‘𝑋) + 𝑇)) |
| 105 | | ltmuldiv 12141 |
. . . . . 6
⊢ (((𝐵𝐸𝐶) ∈ ℝ ∧ (𝑅 / 2) ∈ ℝ ∧ (((𝑁‘𝑋) + 𝑇) ∈ ℝ ∧ 0 < ((𝑁‘𝑋) + 𝑇))) → (((𝐵𝐸𝐶) · ((𝑁‘𝑋) + 𝑇)) < (𝑅 / 2) ↔ (𝐵𝐸𝐶) < ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)))) |
| 106 | 66, 46, 74, 104, 105 | syl112anc 1376 |
. . . . 5
⊢ (𝜑 → (((𝐵𝐸𝐶) · ((𝑁‘𝑋) + 𝑇)) < (𝑅 / 2) ↔ (𝐵𝐸𝐶) < ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)))) |
| 107 | 99, 106 | mpbird 257 |
. . . 4
⊢ (𝜑 → ((𝐵𝐸𝐶) · ((𝑁‘𝑋) + 𝑇)) < (𝑅 / 2)) |
| 108 | 28, 75, 46, 96, 107 | lelttrd 11419 |
. . 3
⊢ (𝜑 → ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌)) < (𝑅 / 2)) |
| 109 | 26, 28, 31, 61, 108 | lt2halvesd 12514 |
. 2
⊢ (𝜑 → (((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) + ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌))) < 𝑅) |
| 110 | 22, 29, 31, 33, 109 | lelttrd 11419 |
1
⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐶 · 𝑌)) < 𝑅) |