Metamath Proof Explorer

Theorem nmopub2tALT

Description: An upper bound for an operator norm. (Contributed by NM, 12-Apr-2006) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion nmopub2tALT ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → norm op ⁡ T ≤ A

Proof

Step Hyp Ref Expression
1 normcl ⊢ x ∈ ℋ → norm ℎ ⁡ x ∈ ℝ
2 1 ad2antlr ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ x ∈ ℝ
3 simpllr ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → A ∈ ℝ ∧ 0 ≤ A
4 simpr ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ x ≤ 1
5 1re ⊢ 1 ∈ ℝ
6 lemul2a ⊢ norm ℎ ⁡ x ∈ ℝ ∧ 1 ∈ ℝ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ norm ℎ ⁡ x ≤ 1 → A ⁢ norm ℎ ⁡ x ≤ A ⋅ 1
7 5 6 mp3anl2 ⊢ norm ℎ ⁡ x ∈ ℝ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ norm ℎ ⁡ x ≤ 1 → A ⁢ norm ℎ ⁡ x ≤ A ⋅ 1
8 2 3 4 7 syl21anc ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → A ⁢ norm ℎ ⁡ x ≤ A ⋅ 1
9 ax-1rid ⊢ A ∈ ℝ → A ⋅ 1 = A
10 9 ad2antrl ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A → A ⋅ 1 = A
11 10 ad2antrr ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → A ⋅ 1 = A
12 8 11 breqtrd ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → A ⁢ norm ℎ ⁡ x ≤ A
13 ffvelrn ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
14 normcl ⊢ T ⁡ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ∈ ℝ
15 13 14 syl ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ∈ ℝ
16 15 adantlr ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ∈ ℝ
17 remulcl ⊢ A ∈ ℝ ∧ norm ℎ ⁡ x ∈ ℝ → A ⁢ norm ℎ ⁡ x ∈ ℝ
18 1 17 sylan2 ⊢ A ∈ ℝ ∧ x ∈ ℋ → A ⁢ norm ℎ ⁡ x ∈ ℝ
19 18 adantlr ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → A ⁢ norm ℎ ⁡ x ∈ ℝ
20 19 adantll ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → A ⁢ norm ℎ ⁡ x ∈ ℝ
21 simplrl ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → A ∈ ℝ
22 letr ⊢ norm ℎ ⁡ T ⁡ x ∈ ℝ ∧ A ⁢ norm ℎ ⁡ x ∈ ℝ ∧ A ∈ ℝ → norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x ∧ A ⁢ norm ℎ ⁡ x ≤ A → norm ℎ ⁡ T ⁡ x ≤ A
23 16 20 21 22 syl3anc ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x ∧ A ⁢ norm ℎ ⁡ x ≤ A → norm ℎ ⁡ T ⁡ x ≤ A
24 23 adantr ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x ∧ A ⁢ norm ℎ ⁡ x ≤ A → norm ℎ ⁡ T ⁡ x ≤ A
25 12 24 mpan2d ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → norm ℎ ⁡ T ⁡ x ≤ A
26 25 ex ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → norm ℎ ⁡ T ⁡ x ≤ A
27 26 com23 ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A
28 27 ralimdva ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A → ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A
29 28 imp ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A
30 rexr ⊢ A ∈ ℝ → A ∈ ℝ *
31 30 adantr ⊢ A ∈ ℝ ∧ 0 ≤ A → A ∈ ℝ *
32 nmopub ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ * → norm op ⁡ T ≤ A ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A
33 31 32 sylan2 ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A → norm op ⁡ T ≤ A ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A
34 33 biimpar ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A → norm op ⁡ T ≤ A
35 29 34 syldan ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → norm op ⁡ T ≤ A
36 35 3impa ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → norm op ⁡ T ≤ A