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 ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( normℎ ‘ 𝑥 ) ) ) → ( normop ‘ 𝑇 ) ≤ 𝐴 )

Proof

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