Metamath Proof Explorer

Theorem nmcopexi

Description: The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of Beran p. 99. (Contributed by NM, 5-Feb-2006) (Proof shortened by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmcopex.1 ⊢T∈LinOp
nmcopex.2 ⊢T∈ContOp
Assertion nmcopexi ⊢normop⁡T∈ℝ

Proof

Step Hyp Ref Expression
1 nmcopex.1 ⊢T∈LinOp
2 nmcopex.2 ⊢T∈ContOp
3 ax-hv0cl ⊢0ℎ∈ℋ
4 1rp ⊢1∈ℝ+
5 cnopc ⊢T∈ContOp∧0ℎ∈ℋ∧1∈ℝ+→∃y∈ℝ+∀z∈ℋnormℎ⁡z-ℎ0ℎ<y→normℎ⁡T⁡z-ℎT⁡0ℎ<1
6 2 3 4 5 mp3an ⊢∃y∈ℝ+∀z∈ℋnormℎ⁡z-ℎ0ℎ<y→normℎ⁡T⁡z-ℎT⁡0ℎ<1
7 hvsub0 ⊢z∈ℋ→z-ℎ0ℎ=z
8 7 fveq2d ⊢z∈ℋ→normℎ⁡z-ℎ0ℎ=normℎ⁡z
9 8 breq1d ⊢z∈ℋ→normℎ⁡z-ℎ0ℎ<y↔normℎ⁡z<y
10 1 lnop0i ⊢T⁡0ℎ=0ℎ
11 10 oveq2i ⊢T⁡z-ℎT⁡0ℎ=T⁡z-ℎ0ℎ
12 1 lnopfi ⊢T:ℋ⟶ℋ
13 12 ffvelcdmi ⊢z∈ℋ→T⁡z∈ℋ
14 hvsub0 ⊢T⁡z∈ℋ→T⁡z-ℎ0ℎ=T⁡z
15 13 14 syl ⊢z∈ℋ→T⁡z-ℎ0ℎ=T⁡z
16 11 15 eqtrid ⊢z∈ℋ→T⁡z-ℎT⁡0ℎ=T⁡z
17 16 fveq2d ⊢z∈ℋ→normℎ⁡T⁡z-ℎT⁡0ℎ=normℎ⁡T⁡z
18 17 breq1d ⊢z∈ℋ→normℎ⁡T⁡z-ℎT⁡0ℎ<1↔normℎ⁡T⁡z<1
19 9 18 imbi12d ⊢z∈ℋ→normℎ⁡z-ℎ0ℎ<y→normℎ⁡T⁡z-ℎT⁡0ℎ<1↔normℎ⁡z<y→normℎ⁡T⁡z<1
20 19 ralbiia ⊢∀z∈ℋnormℎ⁡z-ℎ0ℎ<y→normℎ⁡T⁡z-ℎT⁡0ℎ<1↔∀z∈ℋnormℎ⁡z<y→normℎ⁡T⁡z<1
21 20 rexbii ⊢∃y∈ℝ+∀z∈ℋnormℎ⁡z-ℎ0ℎ<y→normℎ⁡T⁡z-ℎT⁡0ℎ<1↔∃y∈ℝ+∀z∈ℋnormℎ⁡z<y→normℎ⁡T⁡z<1
22 6 21 mpbi ⊢∃y∈ℝ+∀z∈ℋnormℎ⁡z<y→normℎ⁡T⁡z<1
23 nmopval ⊢T:ℋ⟶ℋ→normop⁡T=supm|∃x∈ℋnormℎ⁡x≤1∧m=normℎ⁡T⁡xℝ*<
24 12 23 ax-mp ⊢normop⁡T=supm|∃x∈ℋnormℎ⁡x≤1∧m=normℎ⁡T⁡xℝ*<
25 12 ffvelcdmi ⊢x∈ℋ→T⁡x∈ℋ
26 normcl ⊢T⁡x∈ℋ→normℎ⁡T⁡x∈ℝ
27 25 26 syl ⊢x∈ℋ→normℎ⁡T⁡x∈ℝ
28 10 fveq2i ⊢normℎ⁡T⁡0ℎ=normℎ⁡0ℎ
29 norm0 ⊢normℎ⁡0ℎ=0
30 28 29 eqtri ⊢normℎ⁡T⁡0ℎ=0
31 rpcn ⊢y2∈ℝ+→y2∈ℂ
32 1 lnopmuli ⊢y2∈ℂ∧x∈ℋ→T⁡y2⋅ℎx=y2⋅ℎT⁡x
33 31 32 sylan ⊢y2∈ℝ+∧x∈ℋ→T⁡y2⋅ℎx=y2⋅ℎT⁡x
34 33 fveq2d ⊢y2∈ℝ+∧x∈ℋ→normℎ⁡T⁡y2⋅ℎx=normℎ⁡y2⋅ℎT⁡x
35 norm-iii ⊢y2∈ℂ∧T⁡x∈ℋ→normℎ⁡y2⋅ℎT⁡x=y2⁢normℎ⁡T⁡x
36 31 25 35 syl2an ⊢y2∈ℝ+∧x∈ℋ→normℎ⁡y2⋅ℎT⁡x=y2⁢normℎ⁡T⁡x
37 rpre ⊢y2∈ℝ+→y2∈ℝ
38 rpge0 ⊢y2∈ℝ+→0≤y2
39 37 38 absidd ⊢y2∈ℝ+→y2=y2
40 39 adantr ⊢y2∈ℝ+∧x∈ℋ→y2=y2
41 40 oveq1d ⊢y2∈ℝ+∧x∈ℋ→y2⁢normℎ⁡T⁡x=y2⁢normℎ⁡T⁡x
42 34 36 41 3eqtrrd ⊢y2∈ℝ+∧x∈ℋ→y2⁢normℎ⁡T⁡x=normℎ⁡T⁡y2⋅ℎx
43 22 24 27 30 42 nmcexi ⊢normop⁡T∈ℝ