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 30681 | . . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → (𝐿‘𝑥) ∈ ℝ) | 
| 5 | 1, 4 | mpan 690 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 → (𝐿‘𝑥) ∈ ℝ) | 
| 6 |  | remulcl 11241 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ (𝐿‘𝑥) ∈ ℝ) → (𝐴 · (𝐿‘𝑥)) ∈ ℝ) | 
| 7 | 5, 6 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → (𝐴 · (𝐿‘𝑥)) ∈ ℝ) | 
| 8 | 7 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (𝐴 · (𝐿‘𝑥)) ∈ ℝ) | 
| 9 |  | recn 11246 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) | 
| 10 | 9 | abscld 15476 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ →
(abs‘𝐴) ∈
ℝ) | 
| 11 |  | remulcl 11241 | . . . . . . . . . . . 12
⊢
(((abs‘𝐴)
∈ ℝ ∧ (𝐿‘𝑥) ∈ ℝ) → ((abs‘𝐴) · (𝐿‘𝑥)) ∈ ℝ) | 
| 12 | 10, 5, 11 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → ((abs‘𝐴) · (𝐿‘𝑥)) ∈ ℝ) | 
| 13 | 12 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · (𝐿‘𝑥)) ∈ ℝ) | 
| 14 | 10 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (abs‘𝐴) ∈ ℝ) | 
| 15 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℝ) | 
| 16 | 10 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → (abs‘𝐴) ∈ ℝ) | 
| 17 | 2, 3 | nvge0 30693 | . . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → 0 ≤ (𝐿‘𝑥)) | 
| 18 | 1, 17 | mpan 690 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 → 0 ≤ (𝐿‘𝑥)) | 
| 19 | 5, 18 | jca 511 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑋 → ((𝐿‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐿‘𝑥))) | 
| 20 | 19 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → ((𝐿‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐿‘𝑥))) | 
| 21 |  | leabs 15339 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴)) | 
| 22 | 21 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → 𝐴 ≤ (abs‘𝐴)) | 
| 23 |  | lemul1a 12122 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧
(abs‘𝐴) ∈
ℝ ∧ ((𝐿‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐿‘𝑥))) ∧ 𝐴 ≤ (abs‘𝐴)) → (𝐴 · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · (𝐿‘𝑥))) | 
| 24 | 15, 16, 20, 22, 23 | syl31anc 1374 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → (𝐴 · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · (𝐿‘𝑥))) | 
| 25 | 24 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (𝐴 · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · (𝐿‘𝑥))) | 
| 26 | 5 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → (𝐿‘𝑥) ∈ ℝ) | 
| 27 |  | 1red 11263 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → 1 ∈ ℝ) | 
| 28 | 9 | absge0d 15484 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ → 0 ≤
(abs‘𝐴)) | 
| 29 | 28 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘𝐴)) | 
| 30 | 16, 29 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) | 
| 31 | 26, 27, 30 | 3jca 1128 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → ((𝐿‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧
((abs‘𝐴) ∈
ℝ ∧ 0 ≤ (abs‘𝐴)))) | 
| 32 |  | lemul2a 12123 | . . . . . . . . . . . 12
⊢ ((((𝐿‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧
((abs‘𝐴) ∈
ℝ ∧ 0 ≤ (abs‘𝐴))) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · 1)) | 
| 33 | 31, 32 | sylan 580 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · 1)) | 
| 34 | 10 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ →
(abs‘𝐴) ∈
ℂ) | 
| 35 | 34 | mulridd 11279 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ →
((abs‘𝐴) · 1)
= (abs‘𝐴)) | 
| 36 | 35 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · 1) = (abs‘𝐴)) | 
| 37 | 33, 36 | breqtrd 5168 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · (𝐿‘𝑥)) ≤ (abs‘𝐴)) | 
| 38 | 8, 13, 14, 25, 37 | letrd 11419 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) | 
| 39 | 38 | adantlll 718 | . . . . . . . 8
⊢ ((((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) | 
| 40 |  | nmoubi.w | . . . . . . . . . . . 12
⊢ 𝑊 ∈ NrmCVec | 
| 41 |  | ffvelcdm 7100 | . . . . . . . . . . . 12
⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝑥 ∈ 𝑋) → (𝑇‘𝑥) ∈ 𝑌) | 
| 42 |  | nmoubi.y | . . . . . . . . . . . . 13
⊢ 𝑌 = (BaseSet‘𝑊) | 
| 43 |  | nmoubi.m | . . . . . . . . . . . . 13
⊢ 𝑀 =
(normCV‘𝑊) | 
| 44 | 42, 43 | nvcl 30681 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ 𝑌) → (𝑀‘(𝑇‘𝑥)) ∈ ℝ) | 
| 45 | 40, 41, 44 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝑥 ∈ 𝑋) → (𝑀‘(𝑇‘𝑥)) ∈ ℝ) | 
| 46 | 45 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (𝑀‘(𝑇‘𝑥)) ∈ ℝ) | 
| 47 | 7 | adantll 714 | . . . . . . . . . 10
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (𝐴 · (𝐿‘𝑥)) ∈ ℝ) | 
| 48 | 10 | ad2antlr 727 | . . . . . . . . . 10
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (abs‘𝐴) ∈ ℝ) | 
| 49 |  | letr 11356 | . . . . . . . . . 10
⊢ (((𝑀‘(𝑇‘𝑥)) ∈ ℝ ∧ (𝐴 · (𝐿‘𝑥)) ∈ ℝ ∧ (abs‘𝐴) ∈ ℝ) →
(((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) ∧ (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) | 
| 50 | 46, 47, 48, 49 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) ∧ (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) | 
| 51 | 50 | adantr 480 | . . . . . . . 8
⊢ ((((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) ∧ (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) | 
| 52 | 39, 51 | mpan2d 694 | . . . . . . 7
⊢ ((((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) | 
| 53 | 52 | ex 412 | . . . . . 6
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → ((𝐿‘𝑥) ≤ 1 → ((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))) | 
| 54 | 53 | com23 86 | . . . . 5
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → ((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))) | 
| 55 | 54 | ralimdva 3166 | . . . 4
⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) → (∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))) | 
| 56 | 55 | imp 406 | . . 3
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) | 
| 57 | 10 | rexrd 11312 | . . . . 5
⊢ (𝐴 ∈ ℝ →
(abs‘𝐴) ∈
ℝ*) | 
| 58 |  | nmoubi.3 | . . . . . 6
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) | 
| 59 | 2, 42, 3, 43, 58, 1, 40 | nmoubi 30792 | . . . . 5
⊢ ((𝑇:𝑋⟶𝑌 ∧ (abs‘𝐴) ∈ ℝ*) → ((𝑁‘𝑇) ≤ (abs‘𝐴) ↔ ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))) | 
| 60 | 57, 59 | sylan2 593 | . . . 4
⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) → ((𝑁‘𝑇) ≤ (abs‘𝐴) ↔ ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))) | 
| 61 | 60 | biimpar 477 | . . 3
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) → (𝑁‘𝑇) ≤ (abs‘𝐴)) | 
| 62 | 56, 61 | syldan 591 | . 2
⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ (abs‘𝐴)) | 
| 63 | 62 | 3impa 1109 | 1
⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ (abs‘𝐴)) |