| Step | Hyp | Ref
| Expression |
| 1 | | cnlnadjlem.1 |
. . . . . . . 8
⊢ 𝑇 ∈ LinOp |
| 2 | 1 | lnopfi 31988 |
. . . . . . 7
⊢ 𝑇: ℋ⟶
ℋ |
| 3 | 2 | ffvelcdmi 7103 |
. . . . . 6
⊢ (𝑔 ∈ ℋ → (𝑇‘𝑔) ∈ ℋ) |
| 4 | | hicl 31099 |
. . . . . 6
⊢ (((𝑇‘𝑔) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘𝑔) ·ih 𝑦) ∈
ℂ) |
| 5 | 3, 4 | sylan 580 |
. . . . 5
⊢ ((𝑔 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘𝑔) ·ih 𝑦) ∈
ℂ) |
| 6 | 5 | ancoms 458 |
. . . 4
⊢ ((𝑦 ∈ ℋ ∧ 𝑔 ∈ ℋ) → ((𝑇‘𝑔) ·ih 𝑦) ∈
ℂ) |
| 7 | | cnlnadjlem.3 |
. . . 4
⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) |
| 8 | 6, 7 | fmptd 7134 |
. . 3
⊢ (𝑦 ∈ ℋ → 𝐺:
ℋ⟶ℂ) |
| 9 | | hvmulcl 31032 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ) → (𝑥
·ℎ 𝑤) ∈ ℋ) |
| 10 | 1 | lnopaddi 31990 |
. . . . . . . . . . . 12
⊢ (((𝑥
·ℎ 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑇‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧)) = ((𝑇‘(𝑥 ·ℎ 𝑤)) +ℎ (𝑇‘𝑧))) |
| 11 | 10 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ (((𝑥
·ℎ 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑇‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧)) = ((𝑇‘(𝑥 ·ℎ 𝑤)) +ℎ (𝑇‘𝑧))) |
| 12 | 11 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (((𝑥
·ℎ 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧))
·ih 𝑦) = (((𝑇‘(𝑥 ·ℎ 𝑤)) +ℎ (𝑇‘𝑧)) ·ih 𝑦)) |
| 13 | 2 | ffvelcdmi 7103 |
. . . . . . . . . . 11
⊢ ((𝑥
·ℎ 𝑤) ∈ ℋ → (𝑇‘(𝑥 ·ℎ 𝑤)) ∈
ℋ) |
| 14 | 2 | ffvelcdmi 7103 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℋ → (𝑇‘𝑧) ∈ ℋ) |
| 15 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℋ → 𝑦 ∈
ℋ) |
| 16 | | ax-his2 31102 |
. . . . . . . . . . 11
⊢ (((𝑇‘(𝑥 ·ℎ 𝑤)) ∈ ℋ ∧ (𝑇‘𝑧) ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑇‘(𝑥 ·ℎ 𝑤)) +ℎ (𝑇‘𝑧)) ·ih 𝑦) = (((𝑇‘(𝑥 ·ℎ 𝑤))
·ih 𝑦) + ((𝑇‘𝑧) ·ih 𝑦))) |
| 17 | 13, 14, 15, 16 | syl3an 1161 |
. . . . . . . . . 10
⊢ (((𝑥
·ℎ 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑇‘(𝑥 ·ℎ 𝑤)) +ℎ (𝑇‘𝑧)) ·ih 𝑦) = (((𝑇‘(𝑥 ·ℎ 𝑤))
·ih 𝑦) + ((𝑇‘𝑧) ·ih 𝑦))) |
| 18 | 12, 17 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝑥
·ℎ 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧))
·ih 𝑦) = (((𝑇‘(𝑥 ·ℎ 𝑤))
·ih 𝑦) + ((𝑇‘𝑧) ·ih 𝑦))) |
| 19 | 18 | 3comr 1126 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℋ ∧ (𝑥
·ℎ 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑇‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧))
·ih 𝑦) = (((𝑇‘(𝑥 ·ℎ 𝑤))
·ih 𝑦) + ((𝑇‘𝑧) ·ih 𝑦))) |
| 20 | 19 | 3expa 1119 |
. . . . . . 7
⊢ (((𝑦 ∈ ℋ ∧ (𝑥
·ℎ 𝑤) ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑇‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧))
·ih 𝑦) = (((𝑇‘(𝑥 ·ℎ 𝑤))
·ih 𝑦) + ((𝑇‘𝑧) ·ih 𝑦))) |
| 21 | 9, 20 | sylanl2 681 |
. . . . . 6
⊢ (((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) → ((𝑇‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧))
·ih 𝑦) = (((𝑇‘(𝑥 ·ℎ 𝑤))
·ih 𝑦) + ((𝑇‘𝑧) ·ih 𝑦))) |
| 22 | | hvaddcl 31031 |
. . . . . . . . 9
⊢ (((𝑥
·ℎ 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 ·ℎ 𝑤) +ℎ 𝑧) ∈
ℋ) |
| 23 | 9, 22 | sylan 580 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑥
·ℎ 𝑤) +ℎ 𝑧) ∈ ℋ) |
| 24 | | cnlnadjlem.2 |
. . . . . . . . 9
⊢ 𝑇 ∈ ContOp |
| 25 | 1, 24, 7 | cnlnadjlem1 32086 |
. . . . . . . 8
⊢ (((𝑥
·ℎ 𝑤) +ℎ 𝑧) ∈ ℋ → (𝐺‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧)) = ((𝑇‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧))
·ih 𝑦)) |
| 26 | 23, 25 | syl 17 |
. . . . . . 7
⊢ (((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (𝐺‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧)) = ((𝑇‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧))
·ih 𝑦)) |
| 27 | 26 | adantll 714 |
. . . . . 6
⊢ (((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) → (𝐺‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧)) = ((𝑇‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧))
·ih 𝑦)) |
| 28 | 2 | ffvelcdmi 7103 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℋ → (𝑇‘𝑤) ∈ ℋ) |
| 29 | | ax-his3 31103 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ (𝑇‘𝑤) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑥 ·ℎ (𝑇‘𝑤)) ·ih 𝑦) = (𝑥 · ((𝑇‘𝑤) ·ih 𝑦))) |
| 30 | 28, 29 | syl3an2 1165 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑥
·ℎ (𝑇‘𝑤)) ·ih 𝑦) = (𝑥 · ((𝑇‘𝑤) ·ih 𝑦))) |
| 31 | 30 | 3comr 1126 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℋ ∧ 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ) → ((𝑥
·ℎ (𝑇‘𝑤)) ·ih 𝑦) = (𝑥 · ((𝑇‘𝑤) ·ih 𝑦))) |
| 32 | 31 | 3expb 1121 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) → ((𝑥
·ℎ (𝑇‘𝑤)) ·ih 𝑦) = (𝑥 · ((𝑇‘𝑤) ·ih 𝑦))) |
| 33 | 1 | lnopmuli 31991 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ) → (𝑇‘(𝑥 ·ℎ 𝑤)) = (𝑥 ·ℎ (𝑇‘𝑤))) |
| 34 | 33 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ) → ((𝑇‘(𝑥 ·ℎ 𝑤))
·ih 𝑦) = ((𝑥 ·ℎ (𝑇‘𝑤)) ·ih 𝑦)) |
| 35 | 34 | adantl 481 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) → ((𝑇‘(𝑥 ·ℎ 𝑤))
·ih 𝑦) = ((𝑥 ·ℎ (𝑇‘𝑤)) ·ih 𝑦)) |
| 36 | 1, 24, 7 | cnlnadjlem1 32086 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℋ → (𝐺‘𝑤) = ((𝑇‘𝑤) ·ih 𝑦)) |
| 37 | 36 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℋ → (𝑥 · (𝐺‘𝑤)) = (𝑥 · ((𝑇‘𝑤) ·ih 𝑦))) |
| 38 | 37 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) → (𝑥 · (𝐺‘𝑤)) = (𝑥 · ((𝑇‘𝑤) ·ih 𝑦))) |
| 39 | 32, 35, 38 | 3eqtr4rd 2788 |
. . . . . . 7
⊢ ((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) → (𝑥 · (𝐺‘𝑤)) = ((𝑇‘(𝑥 ·ℎ 𝑤))
·ih 𝑦)) |
| 40 | 1, 24, 7 | cnlnadjlem1 32086 |
. . . . . . 7
⊢ (𝑧 ∈ ℋ → (𝐺‘𝑧) = ((𝑇‘𝑧) ·ih 𝑦)) |
| 41 | 39, 40 | oveqan12d 7450 |
. . . . . 6
⊢ (((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) → ((𝑥 · (𝐺‘𝑤)) + (𝐺‘𝑧)) = (((𝑇‘(𝑥 ·ℎ 𝑤))
·ih 𝑦) + ((𝑇‘𝑧) ·ih 𝑦))) |
| 42 | 21, 27, 41 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) → (𝐺‘((𝑥 ·ℎ 𝑤) +ℎ 𝑧)) = ((𝑥 · (𝐺‘𝑤)) + (𝐺‘𝑧))) |
| 43 | 42 | ralrimiva 3146 |
. . . 4
⊢ ((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) →
∀𝑧 ∈ ℋ
(𝐺‘((𝑥
·ℎ 𝑤) +ℎ 𝑧)) = ((𝑥 · (𝐺‘𝑤)) + (𝐺‘𝑧))) |
| 44 | 43 | ralrimivva 3202 |
. . 3
⊢ (𝑦 ∈ ℋ →
∀𝑥 ∈ ℂ
∀𝑤 ∈ ℋ
∀𝑧 ∈ ℋ
(𝐺‘((𝑥
·ℎ 𝑤) +ℎ 𝑧)) = ((𝑥 · (𝐺‘𝑤)) + (𝐺‘𝑧))) |
| 45 | | ellnfn 31902 |
. . 3
⊢ (𝐺 ∈ LinFn ↔ (𝐺: ℋ⟶ℂ ∧
∀𝑥 ∈ ℂ
∀𝑤 ∈ ℋ
∀𝑧 ∈ ℋ
(𝐺‘((𝑥
·ℎ 𝑤) +ℎ 𝑧)) = ((𝑥 · (𝐺‘𝑤)) + (𝐺‘𝑧)))) |
| 46 | 8, 44, 45 | sylanbrc 583 |
. 2
⊢ (𝑦 ∈ ℋ → 𝐺 ∈ LinFn) |
| 47 | 1, 24 | nmcopexi 32046 |
. . . . 5
⊢
(normop‘𝑇) ∈ ℝ |
| 48 | | normcl 31144 |
. . . . 5
⊢ (𝑦 ∈ ℋ →
(normℎ‘𝑦) ∈ ℝ) |
| 49 | | remulcl 11240 |
. . . . 5
⊢
(((normop‘𝑇) ∈ ℝ ∧
(normℎ‘𝑦) ∈ ℝ) →
((normop‘𝑇) ·
(normℎ‘𝑦)) ∈ ℝ) |
| 50 | 47, 48, 49 | sylancr 587 |
. . . 4
⊢ (𝑦 ∈ ℋ →
((normop‘𝑇) ·
(normℎ‘𝑦)) ∈ ℝ) |
| 51 | 40 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝐺‘𝑧) = ((𝑇‘𝑧) ·ih 𝑦)) |
| 52 | | hicl 31099 |
. . . . . . . . . . 11
⊢ (((𝑇‘𝑧) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘𝑧) ·ih 𝑦) ∈
ℂ) |
| 53 | 14, 52 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘𝑧) ·ih 𝑦) ∈
ℂ) |
| 54 | 51, 53 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝐺‘𝑧) ∈ ℂ) |
| 55 | 54 | abscld 15475 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(abs‘(𝐺‘𝑧)) ∈
ℝ) |
| 56 | | normcl 31144 |
. . . . . . . . . 10
⊢ ((𝑇‘𝑧) ∈ ℋ →
(normℎ‘(𝑇‘𝑧)) ∈ ℝ) |
| 57 | 14, 56 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℋ →
(normℎ‘(𝑇‘𝑧)) ∈ ℝ) |
| 58 | | remulcl 11240 |
. . . . . . . . 9
⊢
(((normℎ‘(𝑇‘𝑧)) ∈ ℝ ∧
(normℎ‘𝑦) ∈ ℝ) →
((normℎ‘(𝑇‘𝑧)) ·
(normℎ‘𝑦)) ∈ ℝ) |
| 59 | 57, 48, 58 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
((normℎ‘(𝑇‘𝑧)) ·
(normℎ‘𝑦)) ∈ ℝ) |
| 60 | | normcl 31144 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℋ →
(normℎ‘𝑧) ∈ ℝ) |
| 61 | | remulcl 11240 |
. . . . . . . . . 10
⊢
(((normop‘𝑇) ∈ ℝ ∧
(normℎ‘𝑧) ∈ ℝ) →
((normop‘𝑇) ·
(normℎ‘𝑧)) ∈ ℝ) |
| 62 | 47, 60, 61 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℋ →
((normop‘𝑇) ·
(normℎ‘𝑧)) ∈ ℝ) |
| 63 | | remulcl 11240 |
. . . . . . . . 9
⊢
((((normop‘𝑇) ·
(normℎ‘𝑧)) ∈ ℝ ∧
(normℎ‘𝑦) ∈ ℝ) →
(((normop‘𝑇) ·
(normℎ‘𝑧)) ·
(normℎ‘𝑦)) ∈ ℝ) |
| 64 | 62, 48, 63 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(((normop‘𝑇) ·
(normℎ‘𝑧)) ·
(normℎ‘𝑦)) ∈ ℝ) |
| 65 | 51 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(abs‘(𝐺‘𝑧)) = (abs‘((𝑇‘𝑧) ·ih 𝑦))) |
| 66 | | bcs 31200 |
. . . . . . . . . 10
⊢ (((𝑇‘𝑧) ∈ ℋ ∧ 𝑦 ∈ ℋ) → (abs‘((𝑇‘𝑧) ·ih 𝑦)) ≤
((normℎ‘(𝑇‘𝑧)) ·
(normℎ‘𝑦))) |
| 67 | 14, 66 | sylan 580 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(abs‘((𝑇‘𝑧)
·ih 𝑦)) ≤
((normℎ‘(𝑇‘𝑧)) ·
(normℎ‘𝑦))) |
| 68 | 65, 67 | eqbrtrd 5165 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(abs‘(𝐺‘𝑧)) ≤
((normℎ‘(𝑇‘𝑧)) ·
(normℎ‘𝑦))) |
| 69 | 57 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(normℎ‘(𝑇‘𝑧)) ∈ ℝ) |
| 70 | 62 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
((normop‘𝑇) ·
(normℎ‘𝑧)) ∈ ℝ) |
| 71 | | normge0 31145 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℋ → 0 ≤
(normℎ‘𝑦)) |
| 72 | 48, 71 | jca 511 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℋ →
((normℎ‘𝑦) ∈ ℝ ∧ 0 ≤
(normℎ‘𝑦))) |
| 73 | 72 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
((normℎ‘𝑦) ∈ ℝ ∧ 0 ≤
(normℎ‘𝑦))) |
| 74 | 1, 24 | nmcoplbi 32047 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℋ →
(normℎ‘(𝑇‘𝑧)) ≤ ((normop‘𝑇) ·
(normℎ‘𝑧))) |
| 75 | 74 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(normℎ‘(𝑇‘𝑧)) ≤ ((normop‘𝑇) ·
(normℎ‘𝑧))) |
| 76 | | lemul1a 12121 |
. . . . . . . . 9
⊢
((((normℎ‘(𝑇‘𝑧)) ∈ ℝ ∧
((normop‘𝑇) ·
(normℎ‘𝑧)) ∈ ℝ ∧
((normℎ‘𝑦) ∈ ℝ ∧ 0 ≤
(normℎ‘𝑦))) ∧
(normℎ‘(𝑇‘𝑧)) ≤ ((normop‘𝑇) ·
(normℎ‘𝑧))) →
((normℎ‘(𝑇‘𝑧)) ·
(normℎ‘𝑦)) ≤ (((normop‘𝑇) ·
(normℎ‘𝑧)) ·
(normℎ‘𝑦))) |
| 77 | 69, 70, 73, 75, 76 | syl31anc 1375 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
((normℎ‘(𝑇‘𝑧)) ·
(normℎ‘𝑦)) ≤ (((normop‘𝑇) ·
(normℎ‘𝑧)) ·
(normℎ‘𝑦))) |
| 78 | 55, 59, 64, 68, 77 | letrd 11418 |
. . . . . . 7
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(abs‘(𝐺‘𝑧)) ≤
(((normop‘𝑇) ·
(normℎ‘𝑧)) ·
(normℎ‘𝑦))) |
| 79 | 60 | recnd 11289 |
. . . . . . . 8
⊢ (𝑧 ∈ ℋ →
(normℎ‘𝑧) ∈ ℂ) |
| 80 | 48 | recnd 11289 |
. . . . . . . 8
⊢ (𝑦 ∈ ℋ →
(normℎ‘𝑦) ∈ ℂ) |
| 81 | 47 | recni 11275 |
. . . . . . . . 9
⊢
(normop‘𝑇) ∈ ℂ |
| 82 | | mul32 11427 |
. . . . . . . . 9
⊢
(((normop‘𝑇) ∈ ℂ ∧
(normℎ‘𝑧) ∈ ℂ ∧
(normℎ‘𝑦) ∈ ℂ) →
(((normop‘𝑇) ·
(normℎ‘𝑧)) ·
(normℎ‘𝑦)) = (((normop‘𝑇) ·
(normℎ‘𝑦)) ·
(normℎ‘𝑧))) |
| 83 | 81, 82 | mp3an1 1450 |
. . . . . . . 8
⊢
(((normℎ‘𝑧) ∈ ℂ ∧
(normℎ‘𝑦) ∈ ℂ) →
(((normop‘𝑇) ·
(normℎ‘𝑧)) ·
(normℎ‘𝑦)) = (((normop‘𝑇) ·
(normℎ‘𝑦)) ·
(normℎ‘𝑧))) |
| 84 | 79, 80, 83 | syl2an 596 |
. . . . . . 7
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(((normop‘𝑇) ·
(normℎ‘𝑧)) ·
(normℎ‘𝑦)) = (((normop‘𝑇) ·
(normℎ‘𝑦)) ·
(normℎ‘𝑧))) |
| 85 | 78, 84 | breqtrd 5169 |
. . . . . 6
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(abs‘(𝐺‘𝑧)) ≤
(((normop‘𝑇) ·
(normℎ‘𝑦)) ·
(normℎ‘𝑧))) |
| 86 | 85 | ancoms 458 |
. . . . 5
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
(abs‘(𝐺‘𝑧)) ≤
(((normop‘𝑇) ·
(normℎ‘𝑦)) ·
(normℎ‘𝑧))) |
| 87 | 86 | ralrimiva 3146 |
. . . 4
⊢ (𝑦 ∈ ℋ →
∀𝑧 ∈ ℋ
(abs‘(𝐺‘𝑧)) ≤
(((normop‘𝑇) ·
(normℎ‘𝑦)) ·
(normℎ‘𝑧))) |
| 88 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 =
((normop‘𝑇) ·
(normℎ‘𝑦)) → (𝑥 ·
(normℎ‘𝑧)) = (((normop‘𝑇) ·
(normℎ‘𝑦)) ·
(normℎ‘𝑧))) |
| 89 | 88 | breq2d 5155 |
. . . . . 6
⊢ (𝑥 =
((normop‘𝑇) ·
(normℎ‘𝑦)) → ((abs‘(𝐺‘𝑧)) ≤ (𝑥 ·
(normℎ‘𝑧)) ↔ (abs‘(𝐺‘𝑧)) ≤ (((normop‘𝑇) ·
(normℎ‘𝑦)) ·
(normℎ‘𝑧)))) |
| 90 | 89 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 =
((normop‘𝑇) ·
(normℎ‘𝑦)) → (∀𝑧 ∈ ℋ (abs‘(𝐺‘𝑧)) ≤ (𝑥 ·
(normℎ‘𝑧)) ↔ ∀𝑧 ∈ ℋ (abs‘(𝐺‘𝑧)) ≤ (((normop‘𝑇) ·
(normℎ‘𝑦)) ·
(normℎ‘𝑧)))) |
| 91 | 90 | rspcev 3622 |
. . . 4
⊢
((((normop‘𝑇) ·
(normℎ‘𝑦)) ∈ ℝ ∧ ∀𝑧 ∈ ℋ
(abs‘(𝐺‘𝑧)) ≤
(((normop‘𝑇) ·
(normℎ‘𝑦)) ·
(normℎ‘𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ℋ (abs‘(𝐺‘𝑧)) ≤ (𝑥 ·
(normℎ‘𝑧))) |
| 92 | 50, 87, 91 | syl2anc 584 |
. . 3
⊢ (𝑦 ∈ ℋ →
∃𝑥 ∈ ℝ
∀𝑧 ∈ ℋ
(abs‘(𝐺‘𝑧)) ≤ (𝑥 ·
(normℎ‘𝑧))) |
| 93 | | lnfncon 32075 |
. . . 4
⊢ (𝐺 ∈ LinFn → (𝐺 ∈ ContFn ↔
∃𝑥 ∈ ℝ
∀𝑧 ∈ ℋ
(abs‘(𝐺‘𝑧)) ≤ (𝑥 ·
(normℎ‘𝑧)))) |
| 94 | 46, 93 | syl 17 |
. . 3
⊢ (𝑦 ∈ ℋ → (𝐺 ∈ ContFn ↔
∃𝑥 ∈ ℝ
∀𝑧 ∈ ℋ
(abs‘(𝐺‘𝑧)) ≤ (𝑥 ·
(normℎ‘𝑧)))) |
| 95 | 92, 94 | mpbird 257 |
. 2
⊢ (𝑦 ∈ ℋ → 𝐺 ∈ ContFn) |
| 96 | 46, 95 | jca 511 |
1
⊢ (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈
ContFn)) |