Proof of Theorem nmlnoubi
| Step | Hyp | Ref
| Expression |
| 1 | | 2fveq3 6911 |
. . . . . . 7
⊢ (𝑥 = 𝑍 → (𝑀‘(𝑇‘𝑥)) = (𝑀‘(𝑇‘𝑍))) |
| 2 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = 𝑍 → (𝐾‘𝑥) = (𝐾‘𝑍)) |
| 3 | 2 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑥 = 𝑍 → (𝐴 · (𝐾‘𝑥)) = (𝐴 · (𝐾‘𝑍))) |
| 4 | 1, 3 | breq12d 5156 |
. . . . . 6
⊢ (𝑥 = 𝑍 → ((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)) ↔ (𝑀‘(𝑇‘𝑍)) ≤ (𝐴 · (𝐾‘𝑍)))) |
| 5 | | id 22 |
. . . . . . . 8
⊢ ((𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) → (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) |
| 6 | 5 | imp 406 |
. . . . . . 7
⊢ (((𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) ∧ 𝑥 ≠ 𝑍) → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) |
| 7 | 6 | adantll 714 |
. . . . . 6
⊢ ((((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) ∧ (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) ∧ 𝑥 ≠ 𝑍) → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) |
| 8 | | 0le0 12367 |
. . . . . . . 8
⊢ 0 ≤
0 |
| 9 | | nmlnoubi.u |
. . . . . . . . . . . . 13
⊢ 𝑈 ∈ NrmCVec |
| 10 | | nmlnoubi.w |
. . . . . . . . . . . . 13
⊢ 𝑊 ∈ NrmCVec |
| 11 | | nmlnoubi.1 |
. . . . . . . . . . . . . 14
⊢ 𝑋 = (BaseSet‘𝑈) |
| 12 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
| 13 | | nmlnoubi.z |
. . . . . . . . . . . . . 14
⊢ 𝑍 = (0vec‘𝑈) |
| 14 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(0vec‘𝑊) = (0vec‘𝑊) |
| 15 | | nmlnoubi.7 |
. . . . . . . . . . . . . 14
⊢ 𝐿 = (𝑈 LnOp 𝑊) |
| 16 | 11, 12, 13, 14, 15 | lno0 30775 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘𝑍) = (0vec‘𝑊)) |
| 17 | 9, 10, 16 | mp3an12 1453 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ 𝐿 → (𝑇‘𝑍) = (0vec‘𝑊)) |
| 18 | 17 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ 𝐿 → (𝑀‘(𝑇‘𝑍)) = (𝑀‘(0vec‘𝑊))) |
| 19 | | nmlnoubi.m |
. . . . . . . . . . . . 13
⊢ 𝑀 =
(normCV‘𝑊) |
| 20 | 14, 19 | nvz0 30687 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ NrmCVec → (𝑀‘(0vec‘𝑊)) = 0) |
| 21 | 10, 20 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑀‘(0vec‘𝑊)) = 0 |
| 22 | 18, 21 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑇 ∈ 𝐿 → (𝑀‘(𝑇‘𝑍)) = 0) |
| 23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → (𝑀‘(𝑇‘𝑍)) = 0) |
| 24 | | nmlnoubi.k |
. . . . . . . . . . . . . 14
⊢ 𝐾 =
(normCV‘𝑈) |
| 25 | 13, 24 | nvz0 30687 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ NrmCVec → (𝐾‘𝑍) = 0) |
| 26 | 9, 25 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝐾‘𝑍) = 0 |
| 27 | 26 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ (𝐴 · (𝐾‘𝑍)) = (𝐴 · 0) |
| 28 | | recn 11245 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 29 | 28 | mul01d 11460 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) =
0) |
| 30 | 27, 29 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝐴 · (𝐾‘𝑍)) = 0) |
| 31 | 30 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → (𝐴 · (𝐾‘𝑍)) = 0) |
| 32 | 23, 31 | breq12d 5156 |
. . . . . . . 8
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → ((𝑀‘(𝑇‘𝑍)) ≤ (𝐴 · (𝐾‘𝑍)) ↔ 0 ≤ 0)) |
| 33 | 8, 32 | mpbiri 258 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → (𝑀‘(𝑇‘𝑍)) ≤ (𝐴 · (𝐾‘𝑍))) |
| 34 | 33 | adantr 480 |
. . . . . 6
⊢ (((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) ∧ (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) → (𝑀‘(𝑇‘𝑍)) ≤ (𝐴 · (𝐾‘𝑍))) |
| 35 | 4, 7, 34 | pm2.61ne 3027 |
. . . . 5
⊢ (((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) ∧ (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) |
| 36 | 35 | ex 412 |
. . . 4
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → ((𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) |
| 37 | 36 | ralimdv 3169 |
. . 3
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → (∀𝑥 ∈ 𝑋 (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) → ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) |
| 38 | 37 | 3impia 1118 |
. 2
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) → ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) |
| 39 | 11, 12, 15 | lnof 30774 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊)) |
| 40 | 9, 10, 39 | mp3an12 1453 |
. . 3
⊢ (𝑇 ∈ 𝐿 → 𝑇:𝑋⟶(BaseSet‘𝑊)) |
| 41 | | nmlnoubi.3 |
. . . 4
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) |
| 42 | 11, 12, 24, 19, 41, 9, 10 | nmoub2i 30793 |
. . 3
⊢ ((𝑇:𝑋⟶(BaseSet‘𝑊) ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) → (𝑁‘𝑇) ≤ 𝐴) |
| 43 | 40, 42 | syl3an1 1164 |
. 2
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) → (𝑁‘𝑇) ≤ 𝐴) |
| 44 | 38, 43 | syld3an3 1411 |
1
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) → (𝑁‘𝑇) ≤ 𝐴) |