Proof of Theorem nmlnoubi
Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑍 → (𝑇‘𝑥) = (𝑇‘𝑍)) |
2 | 1 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑥 = 𝑍 → (𝑀‘(𝑇‘𝑥)) = (𝑀‘(𝑇‘𝑍))) |
3 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑍 → (𝐾‘𝑥) = (𝐾‘𝑍)) |
4 | 3 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑥 = 𝑍 → (𝐴 · (𝐾‘𝑥)) = (𝐴 · (𝐾‘𝑍))) |
5 | 2, 4 | breq12d 4666 |
. . . . . 6
⊢ (𝑥 = 𝑍 → ((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)) ↔ (𝑀‘(𝑇‘𝑍)) ≤ (𝐴 · (𝐾‘𝑍)))) |
6 | | id 22 |
. . . . . . . 8
⊢ ((𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) → (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) |
7 | 6 | imp 445 |
. . . . . . 7
⊢ (((𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) ∧ 𝑥 ≠ 𝑍) → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) |
8 | 7 | adantll 750 |
. . . . . 6
⊢ ((((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) ∧ (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) ∧ 𝑥 ≠ 𝑍) → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) |
9 | | 0le0 11110 |
. . . . . . . 8
⊢ 0 ≤
0 |
10 | | nmlnoubi.u |
. . . . . . . . . . . . 13
⊢ 𝑈 ∈ NrmCVec |
11 | | nmlnoubi.w |
. . . . . . . . . . . . 13
⊢ 𝑊 ∈ NrmCVec |
12 | | nmlnoubi.1 |
. . . . . . . . . . . . . 14
⊢ 𝑋 = (BaseSet‘𝑈) |
13 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
14 | | nmlnoubi.z |
. . . . . . . . . . . . . 14
⊢ 𝑍 = (0vec‘𝑈) |
15 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(0vec‘𝑊) = (0vec‘𝑊) |
16 | | nmlnoubi.7 |
. . . . . . . . . . . . . 14
⊢ 𝐿 = (𝑈 LnOp 𝑊) |
17 | 12, 13, 14, 15, 16 | lno0 27611 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘𝑍) = (0vec‘𝑊)) |
18 | 10, 11, 17 | mp3an12 1414 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ 𝐿 → (𝑇‘𝑍) = (0vec‘𝑊)) |
19 | 18 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ 𝐿 → (𝑀‘(𝑇‘𝑍)) = (𝑀‘(0vec‘𝑊))) |
20 | | nmlnoubi.m |
. . . . . . . . . . . . 13
⊢ 𝑀 =
(normCV‘𝑊) |
21 | 15, 20 | nvz0 27523 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ NrmCVec → (𝑀‘(0vec‘𝑊)) = 0) |
22 | 11, 21 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑀‘(0vec‘𝑊)) = 0 |
23 | 19, 22 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑇 ∈ 𝐿 → (𝑀‘(𝑇‘𝑍)) = 0) |
24 | 23 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → (𝑀‘(𝑇‘𝑍)) = 0) |
25 | | nmlnoubi.k |
. . . . . . . . . . . . . 14
⊢ 𝐾 =
(normCV‘𝑈) |
26 | 14, 25 | nvz0 27523 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ NrmCVec → (𝐾‘𝑍) = 0) |
27 | 10, 26 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝐾‘𝑍) = 0 |
28 | 27 | oveq2i 6661 |
. . . . . . . . . . 11
⊢ (𝐴 · (𝐾‘𝑍)) = (𝐴 · 0) |
29 | | recn 10026 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
30 | 29 | mul01d 10235 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) =
0) |
31 | 28, 30 | syl5eq 2668 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝐴 · (𝐾‘𝑍)) = 0) |
32 | 31 | ad2antrl 764 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → (𝐴 · (𝐾‘𝑍)) = 0) |
33 | 24, 32 | breq12d 4666 |
. . . . . . . 8
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → ((𝑀‘(𝑇‘𝑍)) ≤ (𝐴 · (𝐾‘𝑍)) ↔ 0 ≤ 0)) |
34 | 9, 33 | mpbiri 248 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → (𝑀‘(𝑇‘𝑍)) ≤ (𝐴 · (𝐾‘𝑍))) |
35 | 34 | adantr 481 |
. . . . . 6
⊢ (((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) ∧ (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) → (𝑀‘(𝑇‘𝑍)) ≤ (𝐴 · (𝐾‘𝑍))) |
36 | 5, 8, 35 | pm2.61ne 2879 |
. . . . 5
⊢ (((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) ∧ (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) |
37 | 36 | ex 450 |
. . . 4
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → ((𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) |
38 | 37 | ralimdv 2963 |
. . 3
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → (∀𝑥 ∈ 𝑋 (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) → ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) |
39 | 38 | 3impia 1261 |
. 2
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) → ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) |
40 | 12, 13, 16 | lnof 27610 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊)) |
41 | 10, 11, 40 | mp3an12 1414 |
. . 3
⊢ (𝑇 ∈ 𝐿 → 𝑇:𝑋⟶(BaseSet‘𝑊)) |
42 | | nmlnoubi.3 |
. . . 4
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) |
43 | 12, 13, 25, 20, 42, 10, 11 | nmoub2i 27629 |
. . 3
⊢ ((𝑇:𝑋⟶(BaseSet‘𝑊) ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) → (𝑁‘𝑇) ≤ 𝐴) |
44 | 41, 43 | syl3an1 1359 |
. 2
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥))) → (𝑁‘𝑇) ≤ 𝐴) |
45 | 39, 44 | syld3an3 1371 |
1
⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) → (𝑁‘𝑇) ≤ 𝐴) |