Metamath Proof Explorer

Theorem nmophmi

Description: The norm of the scalar product of a bounded linear operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmophm.1 ⊢T∈BndLinOp
Assertion nmophmi ⊢A∈ℂ→normop⁡A·opT=A⁢normop⁡T

Proof

Step Hyp Ref Expression
1 nmophm.1 ⊢T∈BndLinOp
2 bdopf ⊢T∈BndLinOp→T:ℋ⟶ℋ
3 1 2 ax-mp ⊢T:ℋ⟶ℋ
4 homval ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A·opT⁡x=A⋅ℎT⁡x
5 3 4 mp3an2 ⊢A∈ℂ∧x∈ℋ→A·opT⁡x=A⋅ℎT⁡x
6 5 fveq2d ⊢A∈ℂ∧x∈ℋ→normℎ⁡A·opT⁡x=normℎ⁡A⋅ℎT⁡x
7 3 ffvelcdmi ⊢x∈ℋ→T⁡x∈ℋ
8 norm-iii ⊢A∈ℂ∧T⁡x∈ℋ→normℎ⁡A⋅ℎT⁡x=A⁢normℎ⁡T⁡x
9 7 8 sylan2 ⊢A∈ℂ∧x∈ℋ→normℎ⁡A⋅ℎT⁡x=A⁢normℎ⁡T⁡x
10 6 9 eqtrd ⊢A∈ℂ∧x∈ℋ→normℎ⁡A·opT⁡x=A⁢normℎ⁡T⁡x
11 10 adantr ⊢A∈ℂ∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡A·opT⁡x=A⁢normℎ⁡T⁡x
12 normcl ⊢T⁡x∈ℋ→normℎ⁡T⁡x∈ℝ
13 7 12 syl ⊢x∈ℋ→normℎ⁡T⁡x∈ℝ
14 13 ad2antlr ⊢A∈ℂ∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡x∈ℝ
15 abscl ⊢A∈ℂ→A∈ℝ
16 absge0 ⊢A∈ℂ→0≤A
17 15 16 jca ⊢A∈ℂ→A∈ℝ∧0≤A
18 17 ad2antrr ⊢A∈ℂ∧x∈ℋ∧normℎ⁡x≤1→A∈ℝ∧0≤A
19 nmoplb ⊢T:ℋ⟶ℋ∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡x≤normop⁡T
20 3 19 mp3an1 ⊢x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡x≤normop⁡T
21 20 adantll ⊢A∈ℂ∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡x≤normop⁡T
22 nmopre ⊢T∈BndLinOp→normop⁡T∈ℝ
23 1 22 ax-mp ⊢normop⁡T∈ℝ
24 lemul2a ⊢normℎ⁡T⁡x∈ℝ∧normop⁡T∈ℝ∧A∈ℝ∧0≤A∧normℎ⁡T⁡x≤normop⁡T→A⁢normℎ⁡T⁡x≤A⁢normop⁡T
25 23 24 mp3anl2 ⊢normℎ⁡T⁡x∈ℝ∧A∈ℝ∧0≤A∧normℎ⁡T⁡x≤normop⁡T→A⁢normℎ⁡T⁡x≤A⁢normop⁡T
26 14 18 21 25 syl21anc ⊢A∈ℂ∧x∈ℋ∧normℎ⁡x≤1→A⁢normℎ⁡T⁡x≤A⁢normop⁡T
27 11 26 eqbrtrd ⊢A∈ℂ∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡A·opT⁡x≤A⁢normop⁡T
28 27 ex ⊢A∈ℂ∧x∈ℋ→normℎ⁡x≤1→normℎ⁡A·opT⁡x≤A⁢normop⁡T
29 28 ralrimiva ⊢A∈ℂ→∀x∈ℋnormℎ⁡x≤1→normℎ⁡A·opT⁡x≤A⁢normop⁡T
30 homulcl ⊢A∈ℂ∧T:ℋ⟶ℋ→A·opT:ℋ⟶ℋ
31 3 30 mpan2 ⊢A∈ℂ→A·opT:ℋ⟶ℋ
32 remulcl ⊢A∈ℝ∧normop⁡T∈ℝ→A⁢normop⁡T∈ℝ
33 15 23 32 sylancl ⊢A∈ℂ→A⁢normop⁡T∈ℝ
34 33 rexrd ⊢A∈ℂ→A⁢normop⁡T∈ℝ*
35 nmopub ⊢A·opT:ℋ⟶ℋ∧A⁢normop⁡T∈ℝ*→normop⁡A·opT≤A⁢normop⁡T↔∀x∈ℋnormℎ⁡x≤1→normℎ⁡A·opT⁡x≤A⁢normop⁡T
36 31 34 35 syl2anc ⊢A∈ℂ→normop⁡A·opT≤A⁢normop⁡T↔∀x∈ℋnormℎ⁡x≤1→normℎ⁡A·opT⁡x≤A⁢normop⁡T
37 29 36 mpbird ⊢A∈ℂ→normop⁡A·opT≤A⁢normop⁡T
38 fveq2 ⊢A=0→A=0
39 abs0 ⊢0=0
40 38 39 eqtrdi ⊢A=0→A=0
41 40 oveq1d ⊢A=0→A⁢normop⁡T=0⋅normop⁡T
42 23 recni ⊢normop⁡T∈ℂ
43 42 mul02i ⊢0⋅normop⁡T=0
44 41 43 eqtrdi ⊢A=0→A⁢normop⁡T=0
45 44 adantl ⊢A∈ℂ∧A=0→A⁢normop⁡T=0
46 nmopge0 ⊢A·opT:ℋ⟶ℋ→0≤normop⁡A·opT
47 31 46 syl ⊢A∈ℂ→0≤normop⁡A·opT
48 47 adantr ⊢A∈ℂ∧A=0→0≤normop⁡A·opT
49 45 48 eqbrtrd ⊢A∈ℂ∧A=0→A⁢normop⁡T≤normop⁡A·opT
50 nmoplb ⊢A·opT:ℋ⟶ℋ∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡A·opT⁡x≤normop⁡A·opT
51 31 50 syl3an1 ⊢A∈ℂ∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡A·opT⁡x≤normop⁡A·opT
52 51 3expa ⊢A∈ℂ∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡A·opT⁡x≤normop⁡A·opT
53 11 52 eqbrtrrd ⊢A∈ℂ∧x∈ℋ∧normℎ⁡x≤1→A⁢normℎ⁡T⁡x≤normop⁡A·opT
54 53 adantllr ⊢A∈ℂ∧A≠0∧x∈ℋ∧normℎ⁡x≤1→A⁢normℎ⁡T⁡x≤normop⁡A·opT
55 13 adantl ⊢A∈ℂ∧A≠0∧x∈ℋ→normℎ⁡T⁡x∈ℝ
56 nmopxr ⊢A·opT:ℋ⟶ℋ→normop⁡A·opT∈ℝ*
57 31 56 syl ⊢A∈ℂ→normop⁡A·opT∈ℝ*
58 nmopgtmnf ⊢A·opT:ℋ⟶ℋ→−∞<normop⁡A·opT
59 31 58 syl ⊢A∈ℂ→−∞<normop⁡A·opT
60 xrre ⊢normop⁡A·opT∈ℝ*∧A⁢normop⁡T∈ℝ∧−∞<normop⁡A·opT∧normop⁡A·opT≤A⁢normop⁡T→normop⁡A·opT∈ℝ
61 57 33 59 37 60 syl22anc ⊢A∈ℂ→normop⁡A·opT∈ℝ
62 61 ad2antrr ⊢A∈ℂ∧A≠0∧x∈ℋ→normop⁡A·opT∈ℝ
63 15 ad2antrr ⊢A∈ℂ∧A≠0∧x∈ℋ→A∈ℝ
64 absgt0 ⊢A∈ℂ→A≠0↔0<A
65 64 biimpa ⊢A∈ℂ∧A≠0→0<A
66 65 adantr ⊢A∈ℂ∧A≠0∧x∈ℋ→0<A
67 lemuldiv2 ⊢normℎ⁡T⁡x∈ℝ∧normop⁡A·opT∈ℝ∧A∈ℝ∧0<A→A⁢normℎ⁡T⁡x≤normop⁡A·opT↔normℎ⁡T⁡x≤normop⁡A·opTA
68 55 62 63 66 67 syl112anc ⊢A∈ℂ∧A≠0∧x∈ℋ→A⁢normℎ⁡T⁡x≤normop⁡A·opT↔normℎ⁡T⁡x≤normop⁡A·opTA
69 68 adantr ⊢A∈ℂ∧A≠0∧x∈ℋ∧normℎ⁡x≤1→A⁢normℎ⁡T⁡x≤normop⁡A·opT↔normℎ⁡T⁡x≤normop⁡A·opTA
70 54 69 mpbid ⊢A∈ℂ∧A≠0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡x≤normop⁡A·opTA
71 70 ex ⊢A∈ℂ∧A≠0∧x∈ℋ→normℎ⁡x≤1→normℎ⁡T⁡x≤normop⁡A·opTA
72 71 ralrimiva ⊢A∈ℂ∧A≠0→∀x∈ℋnormℎ⁡x≤1→normℎ⁡T⁡x≤normop⁡A·opTA
73 61 adantr ⊢A∈ℂ∧A≠0→normop⁡A·opT∈ℝ
74 15 adantr ⊢A∈ℂ∧A≠0→A∈ℝ
75 abs00 ⊢A∈ℂ→A=0↔A=0
76 75 necon3bid ⊢A∈ℂ→A≠0↔A≠0
77 76 biimpar ⊢A∈ℂ∧A≠0→A≠0
78 73 74 77 redivcld ⊢A∈ℂ∧A≠0→normop⁡A·opTA∈ℝ
79 78 rexrd ⊢A∈ℂ∧A≠0→normop⁡A·opTA∈ℝ*
80 nmopub ⊢T:ℋ⟶ℋ∧normop⁡A·opTA∈ℝ*→normop⁡T≤normop⁡A·opTA↔∀x∈ℋnormℎ⁡x≤1→normℎ⁡T⁡x≤normop⁡A·opTA
81 3 79 80 sylancr ⊢A∈ℂ∧A≠0→normop⁡T≤normop⁡A·opTA↔∀x∈ℋnormℎ⁡x≤1→normℎ⁡T⁡x≤normop⁡A·opTA
82 72 81 mpbird ⊢A∈ℂ∧A≠0→normop⁡T≤normop⁡A·opTA
83 23 a1i ⊢A∈ℂ∧A≠0→normop⁡T∈ℝ
84 lemuldiv2 ⊢normop⁡T∈ℝ∧normop⁡A·opT∈ℝ∧A∈ℝ∧0<A→A⁢normop⁡T≤normop⁡A·opT↔normop⁡T≤normop⁡A·opTA
85 83 73 74 65 84 syl112anc ⊢A∈ℂ∧A≠0→A⁢normop⁡T≤normop⁡A·opT↔normop⁡T≤normop⁡A·opTA
86 82 85 mpbird ⊢A∈ℂ∧A≠0→A⁢normop⁡T≤normop⁡A·opT
87 49 86 pm2.61dane ⊢A∈ℂ→A⁢normop⁡T≤normop⁡A·opT
88 61 33 letri3d ⊢A∈ℂ→normop⁡A·opT=A⁢normop⁡T↔normop⁡A·opT≤A⁢normop⁡T∧A⁢normop⁡T≤normop⁡A·opT
89 37 87 88 mpbir2and ⊢A∈ℂ→normop⁡A·opT=A⁢normop⁡T