Proof of Theorem nmoub3i
Step | Hyp | Ref
| Expression |
1 | | nmoubi.u |
. . . . . . . . . . . . 13
⊢ 𝑈 ∈ NrmCVec |
2 | | nmoubi.1 |
. . . . . . . . . . . . . 14
⊢ 𝑋 = (BaseSet‘𝑈) |
3 | | nmoubi.l |
. . . . . . . . . . . . . 14
⊢ 𝐿 =
(normCV‘𝑈) |
4 | 2, 3 | nvcl 28528 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → (𝐿‘𝑥) ∈ ℝ) |
5 | 1, 4 | mpan 690 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 → (𝐿‘𝑥) ∈ ℝ) |
6 | | remulcl 10645 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ (𝐿‘𝑥) ∈ ℝ) → (𝐴 · (𝐿‘𝑥)) ∈ ℝ) |
7 | 5, 6 | sylan2 596 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → (𝐴 · (𝐿‘𝑥)) ∈ ℝ) |
8 | 7 | adantr 485 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (𝐴 · (𝐿‘𝑥)) ∈ ℝ) |
9 | | recn 10650 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
10 | 9 | abscld 14829 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ →
(abs‘𝐴) ∈
ℝ) |
11 | | remulcl 10645 |
. . . . . . . . . . . 12
⊢
(((abs‘𝐴)
∈ ℝ ∧ (𝐿‘𝑥) ∈ ℝ) → ((abs‘𝐴) · (𝐿‘𝑥)) ∈ ℝ) |
12 | 10, 5, 11 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → ((abs‘𝐴) · (𝐿‘𝑥)) ∈ ℝ) |
13 | 12 | adantr 485 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · (𝐿‘𝑥)) ∈ ℝ) |
14 | 10 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (abs‘𝐴) ∈ ℝ) |
15 | | simpl 487 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℝ) |
16 | 10 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → (abs‘𝐴) ∈ ℝ) |
17 | 2, 3 | nvge0 28540 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → 0 ≤ (𝐿‘𝑥)) |
18 | 1, 17 | mpan 690 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 → 0 ≤ (𝐿‘𝑥)) |
19 | 5, 18 | jca 516 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑋 → ((𝐿‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐿‘𝑥))) |
20 | 19 | adantl 486 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → ((𝐿‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐿‘𝑥))) |
21 | | leabs 14692 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴)) |
22 | 21 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → 𝐴 ≤ (abs‘𝐴)) |
23 | | lemul1a 11517 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧
(abs‘𝐴) ∈
ℝ ∧ ((𝐿‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐿‘𝑥))) ∧ 𝐴 ≤ (abs‘𝐴)) → (𝐴 · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · (𝐿‘𝑥))) |
24 | 15, 16, 20, 22, 23 | syl31anc 1371 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → (𝐴 · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · (𝐿‘𝑥))) |
25 | 24 | adantr 485 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (𝐴 · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · (𝐿‘𝑥))) |
26 | 5 | adantl 486 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → (𝐿‘𝑥) ∈ ℝ) |
27 | | 1red 10665 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → 1 ∈ ℝ) |
28 | 9 | absge0d 14837 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ → 0 ≤
(abs‘𝐴)) |
29 | 28 | adantr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘𝐴)) |
30 | 16, 29 | jca 516 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) |
31 | 26, 27, 30 | 3jca 1126 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → ((𝐿‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧
((abs‘𝐴) ∈
ℝ ∧ 0 ≤ (abs‘𝐴)))) |
32 | | lemul2a 11518 |
. . . . . . . . . . . 12
⊢ ((((𝐿‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧
((abs‘𝐴) ∈
ℝ ∧ 0 ≤ (abs‘𝐴))) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · 1)) |
33 | 31, 32 | sylan 584 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · 1)) |
34 | 10 | recnd 10692 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ →
(abs‘𝐴) ∈
ℂ) |
35 | 34 | mulid1d 10681 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ →
((abs‘𝐴) · 1)
= (abs‘𝐴)) |
36 | 35 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · 1) = (abs‘𝐴)) |
37 | 33, 36 | breqtrd 5051 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · (𝐿‘𝑥)) ≤ (abs‘𝐴)) |
38 | 8, 13, 14, 25, 37 | letrd 10820 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) |
39 | 38 | adantlll 718 |
. . . . . . . 8
⊢ ((((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) |
40 | | nmoubi.w |
. . . . . . . . . . . 12
⊢ 𝑊 ∈ NrmCVec |
41 | | ffvelrn 6833 |
. . . . . . . . . . . 12
⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝑥 ∈ 𝑋) → (𝑇‘𝑥) ∈ 𝑌) |
42 | | nmoubi.y |
. . . . . . . . . . . . 13
⊢ 𝑌 = (BaseSet‘𝑊) |
43 | | nmoubi.m |
. . . . . . . . . . . . 13
⊢ 𝑀 =
(normCV‘𝑊) |
44 | 42, 43 | nvcl 28528 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ 𝑌) → (𝑀‘(𝑇‘𝑥)) ∈ ℝ) |
45 | 40, 41, 44 | sylancr 591 |
. . . . . . . . . . 11
⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝑥 ∈ 𝑋) → (𝑀‘(𝑇‘𝑥)) ∈ ℝ) |
46 | 45 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (𝑀‘(𝑇‘𝑥)) ∈ ℝ) |
47 | 7 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (𝐴 · (𝐿‘𝑥)) ∈ ℝ) |
48 | 10 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (abs‘𝐴) ∈ ℝ) |
49 | | letr 10757 |
. . . . . . . . . 10
⊢ (((𝑀‘(𝑇‘𝑥)) ∈ ℝ ∧ (𝐴 · (𝐿‘𝑥)) ∈ ℝ ∧ (abs‘𝐴) ∈ ℝ) →
(((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) ∧ (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) |
50 | 46, 47, 48, 49 | syl3anc 1369 |
. . . . . . . . 9
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) ∧ (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) |
51 | 50 | adantr 485 |
. . . . . . . 8
⊢ ((((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) ∧ (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) |
52 | 39, 51 | mpan2d 694 |
. . . . . . 7
⊢ ((((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) |
53 | 52 | ex 417 |
. . . . . 6
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → ((𝐿‘𝑥) ≤ 1 → ((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))) |
54 | 53 | com23 86 |
. . . . 5
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → ((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))) |
55 | 54 | ralimdva 3106 |
. . . 4
⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) → (∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))) |
56 | 55 | imp 411 |
. . 3
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) |
57 | 10 | rexrd 10714 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(abs‘𝐴) ∈
ℝ*) |
58 | | nmoubi.3 |
. . . . . 6
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) |
59 | 2, 42, 3, 43, 58, 1, 40 | nmoubi 28639 |
. . . . 5
⊢ ((𝑇:𝑋⟶𝑌 ∧ (abs‘𝐴) ∈ ℝ*) → ((𝑁‘𝑇) ≤ (abs‘𝐴) ↔ ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))) |
60 | 57, 59 | sylan2 596 |
. . . 4
⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) → ((𝑁‘𝑇) ≤ (abs‘𝐴) ↔ ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))) |
61 | 60 | biimpar 482 |
. . 3
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) → (𝑁‘𝑇) ≤ (abs‘𝐴)) |
62 | 56, 61 | syldan 595 |
. 2
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ (abs‘𝐴)) |
63 | 62 | 3impa 1108 |
1
⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ (abs‘𝐴)) |