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→normop⁡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 ffvelcdm ⊢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∈ℝ*→normop⁡T≤A↔∀x∈ℋnormℎ⁡x≤1→normℎ⁡T⁡x≤A
33 31 32 sylan2 ⊢T:ℋ⟶ℋ∧A∈ℝ∧0≤A→normop⁡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→normop⁡T≤A
35 29 34 syldan ⊢T:ℋ⟶ℋ∧A∈ℝ∧0≤A∧∀x∈ℋnormℎ⁡T⁡x≤A⁢normℎ⁡x→normop⁡T≤A
36 35 3impa ⊢T:ℋ⟶ℋ∧A∈ℝ∧0≤A∧∀x∈ℋnormℎ⁡T⁡x≤A⁢normℎ⁡x→normop⁡T≤A