Proof of Theorem nlmvscnlem2
Step | Hyp | Ref
| Expression |
1 | | nlmvscn.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ NrmMod) |
2 | | nlmngp 23841 |
. . . . 5
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ NrmGrp) |
4 | | ngpms 23756 |
. . . 4
⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → 𝑊 ∈ MetSp) |
6 | | nlmlmod 23842 |
. . . . 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 20140 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝐵 · 𝑋) ∈ 𝑉) |
15 | 7, 8, 9, 14 | syl3anc 1370 |
. . 3
⊢ (𝜑 → (𝐵 · 𝑋) ∈ 𝑉) |
16 | | nlmvscn.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝐾) |
17 | | nlmvscn.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
18 | 10, 11, 12, 13 | lmodvscl 20140 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐶 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝐶 · 𝑌) ∈ 𝑉) |
19 | 7, 16, 17, 18 | syl3anc 1370 |
. . 3
⊢ (𝜑 → (𝐶 · 𝑌) ∈ 𝑉) |
20 | | nlmvscn.d |
. . . 4
⊢ 𝐷 = (dist‘𝑊) |
21 | 10, 20 | mscl 23614 |
. . 3
⊢ ((𝑊 ∈ MetSp ∧ (𝐵 · 𝑋) ∈ 𝑉 ∧ (𝐶 · 𝑌) ∈ 𝑉) → ((𝐵 · 𝑋)𝐷(𝐶 · 𝑌)) ∈ ℝ) |
22 | 5, 15, 19, 21 | syl3anc 1370 |
. 2
⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐶 · 𝑌)) ∈ ℝ) |
23 | 10, 11, 12, 13 | lmodvscl 20140 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝐵 · 𝑌) ∈ 𝑉) |
24 | 7, 8, 17, 23 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → (𝐵 · 𝑌) ∈ 𝑉) |
25 | 10, 20 | mscl 23614 |
. . . 4
⊢ ((𝑊 ∈ MetSp ∧ (𝐵 · 𝑋) ∈ 𝑉 ∧ (𝐵 · 𝑌) ∈ 𝑉) → ((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) ∈ ℝ) |
26 | 5, 15, 24, 25 | syl3anc 1370 |
. . 3
⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) ∈ ℝ) |
27 | 10, 20 | mscl 23614 |
. . . 4
⊢ ((𝑊 ∈ MetSp ∧ (𝐵 · 𝑌) ∈ 𝑉 ∧ (𝐶 · 𝑌) ∈ 𝑉) → ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌)) ∈ ℝ) |
28 | 5, 24, 19, 27 | syl3anc 1370 |
. . 3
⊢ (𝜑 → ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌)) ∈ ℝ) |
29 | 26, 28 | readdcld 11004 |
. 2
⊢ (𝜑 → (((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) + ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌))) ∈ ℝ) |
30 | | nlmvscn.r |
. . 3
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
31 | 30 | rpred 12772 |
. 2
⊢ (𝜑 → 𝑅 ∈ ℝ) |
32 | 10, 20 | mstri 23622 |
. . 3
⊢ ((𝑊 ∈ MetSp ∧ ((𝐵 · 𝑋) ∈ 𝑉 ∧ (𝐶 · 𝑌) ∈ 𝑉 ∧ (𝐵 · 𝑌) ∈ 𝑉)) → ((𝐵 · 𝑋)𝐷(𝐶 · 𝑌)) ≤ (((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) + ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌)))) |
33 | 5, 15, 19, 24, 32 | syl13anc 1371 |
. 2
⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐶 · 𝑌)) ≤ (((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) + ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌)))) |
34 | 11 | nlmngp2 23844 |
. . . . . . . . 9
⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp) |
35 | 1, 34 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ NrmGrp) |
36 | | nlmvscn.a |
. . . . . . . . 9
⊢ 𝐴 = (norm‘𝐹) |
37 | 13, 36 | nmcl 23772 |
. . . . . . . 8
⊢ ((𝐹 ∈ NrmGrp ∧ 𝐵 ∈ 𝐾) → (𝐴‘𝐵) ∈ ℝ) |
38 | 35, 8, 37 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴‘𝐵) ∈ ℝ) |
39 | 13, 36 | nmge0 23773 |
. . . . . . . 8
⊢ ((𝐹 ∈ NrmGrp ∧ 𝐵 ∈ 𝐾) → 0 ≤ (𝐴‘𝐵)) |
40 | 35, 8, 39 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝐴‘𝐵)) |
41 | 38, 40 | ge0p1rpd 12802 |
. . . . . 6
⊢ (𝜑 → ((𝐴‘𝐵) + 1) ∈
ℝ+) |
42 | 41 | rpred 12772 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝐵) + 1) ∈ ℝ) |
43 | 10, 20 | mscl 23614 |
. . . . . 6
⊢ ((𝑊 ∈ MetSp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋𝐷𝑌) ∈ ℝ) |
44 | 5, 9, 17, 43 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (𝑋𝐷𝑌) ∈ ℝ) |
45 | 42, 44 | remulcld 11005 |
. . . 4
⊢ (𝜑 → (((𝐴‘𝐵) + 1) · (𝑋𝐷𝑌)) ∈ ℝ) |
46 | 31 | rehalfcld 12220 |
. . . 4
⊢ (𝜑 → (𝑅 / 2) ∈ ℝ) |
47 | 10, 12, 11, 13, 20, 36 | nlmdsdi 23845 |
. . . . . 6
⊢ ((𝑊 ∈ NrmMod ∧ (𝐵 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐴‘𝐵) · (𝑋𝐷𝑌)) = ((𝐵 · 𝑋)𝐷(𝐵 · 𝑌))) |
48 | 1, 8, 9, 17, 47 | syl13anc 1371 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝐵) · (𝑋𝐷𝑌)) = ((𝐵 · 𝑋)𝐷(𝐵 · 𝑌))) |
49 | | msxms 23607 |
. . . . . . . 8
⊢ (𝑊 ∈ MetSp → 𝑊 ∈
∞MetSp) |
50 | 5, 49 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ ∞MetSp) |
51 | 10, 20 | xmsge0 23616 |
. . . . . . 7
⊢ ((𝑊 ∈ ∞MetSp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 0 ≤ (𝑋𝐷𝑌)) |
52 | 50, 9, 17, 51 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝑋𝐷𝑌)) |
53 | 38 | lep1d 11906 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝐵) ≤ ((𝐴‘𝐵) + 1)) |
54 | 38, 42, 44, 52, 53 | lemul1ad 11914 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝐵) · (𝑋𝐷𝑌)) ≤ (((𝐴‘𝐵) + 1) · (𝑋𝐷𝑌))) |
55 | 48, 54 | eqbrtrrd 5098 |
. . . 4
⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) ≤ (((𝐴‘𝐵) + 1) · (𝑋𝐷𝑌))) |
56 | | nlmvscn.2 |
. . . . . 6
⊢ (𝜑 → (𝑋𝐷𝑌) < 𝑇) |
57 | | nlmvscn.t |
. . . . . 6
⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) |
58 | 56, 57 | breqtrdi 5115 |
. . . . 5
⊢ (𝜑 → (𝑋𝐷𝑌) < ((𝑅 / 2) / ((𝐴‘𝐵) + 1))) |
59 | 44, 46, 41 | ltmuldiv2d 12820 |
. . . . 5
⊢ (𝜑 → ((((𝐴‘𝐵) + 1) · (𝑋𝐷𝑌)) < (𝑅 / 2) ↔ (𝑋𝐷𝑌) < ((𝑅 / 2) / ((𝐴‘𝐵) + 1)))) |
60 | 58, 59 | mpbird 256 |
. . . 4
⊢ (𝜑 → (((𝐴‘𝐵) + 1) · (𝑋𝐷𝑌)) < (𝑅 / 2)) |
61 | 26, 45, 46, 55, 60 | lelttrd 11133 |
. . 3
⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) < (𝑅 / 2)) |
62 | | ngpms 23756 |
. . . . . . 7
⊢ (𝐹 ∈ NrmGrp → 𝐹 ∈ MetSp) |
63 | 35, 62 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ MetSp) |
64 | | nlmvscn.e |
. . . . . . 7
⊢ 𝐸 = (dist‘𝐹) |
65 | 13, 64 | mscl 23614 |
. . . . . 6
⊢ ((𝐹 ∈ MetSp ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝐾) → (𝐵𝐸𝐶) ∈ ℝ) |
66 | 63, 8, 16, 65 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (𝐵𝐸𝐶) ∈ ℝ) |
67 | | nlmvscn.n |
. . . . . . . 8
⊢ 𝑁 = (norm‘𝑊) |
68 | 10, 67 | nmcl 23772 |
. . . . . . 7
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) ∈ ℝ) |
69 | 3, 9, 68 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑁‘𝑋) ∈ ℝ) |
70 | 30 | rphalfcld 12784 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 / 2) ∈
ℝ+) |
71 | 70, 41 | rpdivcld 12789 |
. . . . . . . 8
⊢ (𝜑 → ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) ∈
ℝ+) |
72 | 57, 71 | eqeltrid 2843 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
73 | 72 | rpred 12772 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ ℝ) |
74 | 69, 73 | readdcld 11004 |
. . . . 5
⊢ (𝜑 → ((𝑁‘𝑋) + 𝑇) ∈ ℝ) |
75 | 66, 74 | remulcld 11005 |
. . . 4
⊢ (𝜑 → ((𝐵𝐸𝐶) · ((𝑁‘𝑋) + 𝑇)) ∈ ℝ) |
76 | 10, 12, 11, 13, 20, 67, 64 | nlmdsdir 23846 |
. . . . . 6
⊢ ((𝑊 ∈ NrmMod ∧ (𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉)) → ((𝐵𝐸𝐶) · (𝑁‘𝑌)) = ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌))) |
77 | 1, 8, 16, 17, 76 | syl13anc 1371 |
. . . . 5
⊢ (𝜑 → ((𝐵𝐸𝐶) · (𝑁‘𝑌)) = ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌))) |
78 | 10, 67 | nmcl 23772 |
. . . . . . 7
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑌 ∈ 𝑉) → (𝑁‘𝑌) ∈ ℝ) |
79 | 3, 17, 78 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑁‘𝑌) ∈ ℝ) |
80 | | msxms 23607 |
. . . . . . . 8
⊢ (𝐹 ∈ MetSp → 𝐹 ∈
∞MetSp) |
81 | 63, 80 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ ∞MetSp) |
82 | 13, 64 | xmsge0 23616 |
. . . . . . 7
⊢ ((𝐹 ∈ ∞MetSp ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝐾) → 0 ≤ (𝐵𝐸𝐶)) |
83 | 81, 8, 16, 82 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝐵𝐸𝐶)) |
84 | 79, 69 | resubcld 11403 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁‘𝑌) − (𝑁‘𝑋)) ∈ ℝ) |
85 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(-g‘𝑊) = (-g‘𝑊) |
86 | 10, 67, 85 | nm2dif 23781 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ((𝑁‘𝑌) − (𝑁‘𝑋)) ≤ (𝑁‘(𝑌(-g‘𝑊)𝑋))) |
87 | 3, 17, 9, 86 | syl3anc 1370 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁‘𝑌) − (𝑁‘𝑋)) ≤ (𝑁‘(𝑌(-g‘𝑊)𝑋))) |
88 | 67, 10, 85, 20 | ngpdsr 23761 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋𝐷𝑌) = (𝑁‘(𝑌(-g‘𝑊)𝑋))) |
89 | 3, 9, 17, 88 | syl3anc 1370 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋𝐷𝑌) = (𝑁‘(𝑌(-g‘𝑊)𝑋))) |
90 | 87, 89 | breqtrrd 5102 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁‘𝑌) − (𝑁‘𝑋)) ≤ (𝑋𝐷𝑌)) |
91 | 44, 73, 56 | ltled 11123 |
. . . . . . . 8
⊢ (𝜑 → (𝑋𝐷𝑌) ≤ 𝑇) |
92 | 84, 44, 73, 90, 91 | letrd 11132 |
. . . . . . 7
⊢ (𝜑 → ((𝑁‘𝑌) − (𝑁‘𝑋)) ≤ 𝑇) |
93 | 79, 69, 73 | lesubadd2d 11574 |
. . . . . . 7
⊢ (𝜑 → (((𝑁‘𝑌) − (𝑁‘𝑋)) ≤ 𝑇 ↔ (𝑁‘𝑌) ≤ ((𝑁‘𝑋) + 𝑇))) |
94 | 92, 93 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → (𝑁‘𝑌) ≤ ((𝑁‘𝑋) + 𝑇)) |
95 | 79, 74, 66, 83, 94 | lemul2ad 11915 |
. . . . 5
⊢ (𝜑 → ((𝐵𝐸𝐶) · (𝑁‘𝑌)) ≤ ((𝐵𝐸𝐶) · ((𝑁‘𝑋) + 𝑇))) |
96 | 77, 95 | eqbrtrrd 5098 |
. . . 4
⊢ (𝜑 → ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌)) ≤ ((𝐵𝐸𝐶) · ((𝑁‘𝑋) + 𝑇))) |
97 | | nlmvscn.1 |
. . . . . 6
⊢ (𝜑 → (𝐵𝐸𝐶) < 𝑈) |
98 | | nlmvscn.u |
. . . . . 6
⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) |
99 | 97, 98 | breqtrdi 5115 |
. . . . 5
⊢ (𝜑 → (𝐵𝐸𝐶) < ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇))) |
100 | | 0red 10978 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
101 | 10, 67 | nmge0 23773 |
. . . . . . . 8
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉) → 0 ≤ (𝑁‘𝑋)) |
102 | 3, 9, 101 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑁‘𝑋)) |
103 | 69, 72 | ltaddrpd 12805 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘𝑋) < ((𝑁‘𝑋) + 𝑇)) |
104 | 100, 69, 74, 102, 103 | lelttrd 11133 |
. . . . . 6
⊢ (𝜑 → 0 < ((𝑁‘𝑋) + 𝑇)) |
105 | | ltmuldiv 11848 |
. . . . . 6
⊢ (((𝐵𝐸𝐶) ∈ ℝ ∧ (𝑅 / 2) ∈ ℝ ∧ (((𝑁‘𝑋) + 𝑇) ∈ ℝ ∧ 0 < ((𝑁‘𝑋) + 𝑇))) → (((𝐵𝐸𝐶) · ((𝑁‘𝑋) + 𝑇)) < (𝑅 / 2) ↔ (𝐵𝐸𝐶) < ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)))) |
106 | 66, 46, 74, 104, 105 | syl112anc 1373 |
. . . . 5
⊢ (𝜑 → (((𝐵𝐸𝐶) · ((𝑁‘𝑋) + 𝑇)) < (𝑅 / 2) ↔ (𝐵𝐸𝐶) < ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)))) |
107 | 99, 106 | mpbird 256 |
. . . 4
⊢ (𝜑 → ((𝐵𝐸𝐶) · ((𝑁‘𝑋) + 𝑇)) < (𝑅 / 2)) |
108 | 28, 75, 46, 96, 107 | lelttrd 11133 |
. . 3
⊢ (𝜑 → ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌)) < (𝑅 / 2)) |
109 | 26, 28, 31, 61, 108 | lt2halvesd 12221 |
. 2
⊢ (𝜑 → (((𝐵 · 𝑋)𝐷(𝐵 · 𝑌)) + ((𝐵 · 𝑌)𝐷(𝐶 · 𝑌))) < 𝑅) |
110 | 22, 29, 31, 33, 109 | lelttrd 11133 |
1
⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐶 · 𝑌)) < 𝑅) |