Metamath Proof Explorer

Theorem leopnmid

Description: A bounded Hermitian operator is less than or equal to its norm times the identity operator. (Contributed by NM, 11-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion leopnmid ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ → T ≤ op norm op ⁡ T · op I op

Proof

Step Hyp Ref Expression
1 hmopre ⊢ T ∈ HrmOp ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ∈ ℝ
2 1 adantlr ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ∈ ℝ
3 1 recnd ⊢ T ∈ HrmOp ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ∈ ℂ
4 3 abscld ⊢ T ∈ HrmOp ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ∈ ℝ
5 4 adantlr ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ∈ ℝ
6 idhmop ⊢ I op ∈ HrmOp
7 hmopm ⊢ norm op ⁡ T ∈ ℝ ∧ I op ∈ HrmOp → norm op ⁡ T · op I op ∈ HrmOp
8 6 7 mpan2 ⊢ norm op ⁡ T ∈ ℝ → norm op ⁡ T · op I op ∈ HrmOp
9 hmopre ⊢ norm op ⁡ T · op I op ∈ HrmOp ∧ x ∈ ℋ → norm op ⁡ T · op I op ⁡ x ⋅ ih x ∈ ℝ
10 8 9 sylan ⊢ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T · op I op ⁡ x ⋅ ih x ∈ ℝ
11 10 adantll ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T · op I op ⁡ x ⋅ ih x ∈ ℝ
12 1 leabsd ⊢ T ∈ HrmOp ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ≤ T ⁡ x ⋅ ih x
13 12 adantlr ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ≤ T ⁡ x ⋅ ih x
14 hmopf ⊢ T ∈ HrmOp → T : ℋ ⟶ ℋ
15 ffvelrn ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
16 normcl ⊢ T ⁡ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ∈ ℝ
17 15 16 syl ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ∈ ℝ
18 14 17 sylan ⊢ T ∈ HrmOp ∧ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ∈ ℝ
19 18 adantlr ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ∈ ℝ
20 normcl ⊢ x ∈ ℋ → norm ℎ ⁡ x ∈ ℝ
21 20 adantl ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm ℎ ⁡ x ∈ ℝ
22 19 21 remulcld ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ⁢ norm ℎ ⁡ x ∈ ℝ
23 14 15 sylan ⊢ T ∈ HrmOp ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
24 bcs ⊢ T ⁡ x ∈ ℋ ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ≤ norm ℎ ⁡ T ⁡ x ⁢ norm ℎ ⁡ x
25 23 24 sylancom ⊢ T ∈ HrmOp ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ≤ norm ℎ ⁡ T ⁡ x ⁢ norm ℎ ⁡ x
26 25 adantlr ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ≤ norm ℎ ⁡ T ⁡ x ⁢ norm ℎ ⁡ x
27 remulcl ⊢ norm op ⁡ T ∈ ℝ ∧ norm ℎ ⁡ x ∈ ℝ → norm op ⁡ T ⁢ norm ℎ ⁡ x ∈ ℝ
28 20 27 sylan2 ⊢ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T ⁢ norm ℎ ⁡ x ∈ ℝ
29 28 adantll ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T ⁢ norm ℎ ⁡ x ∈ ℝ
30 normge0 ⊢ x ∈ ℋ → 0 ≤ norm ℎ ⁡ x
31 20 30 jca ⊢ x ∈ ℋ → norm ℎ ⁡ x ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ x
32 31 adantl ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm ℎ ⁡ x ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ x
33 hmoplin ⊢ T ∈ HrmOp → T ∈ LinOp
34 elbdop2 ⊢ T ∈ BndLinOp ↔ T ∈ LinOp ∧ norm op ⁡ T ∈ ℝ
35 34 biimpri ⊢ T ∈ LinOp ∧ norm op ⁡ T ∈ ℝ → T ∈ BndLinOp
36 33 35 sylan ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ → T ∈ BndLinOp
37 nmbdoplb ⊢ T ∈ BndLinOp ∧ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ T ⁢ norm ℎ ⁡ x
38 36 37 sylan ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ T ⁢ norm ℎ ⁡ x
39 lemul1a ⊢ norm ℎ ⁡ T ⁡ x ∈ ℝ ∧ norm op ⁡ T ⁢ norm ℎ ⁡ x ∈ ℝ ∧ norm ℎ ⁡ x ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ x ∧ norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ T ⁢ norm ℎ ⁡ x → norm ℎ ⁡ T ⁡ x ⁢ norm ℎ ⁡ x ≤ norm op ⁡ T ⁢ norm ℎ ⁡ x ⁢ norm ℎ ⁡ x
40 19 29 32 38 39 syl31anc ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ⁢ norm ℎ ⁡ x ≤ norm op ⁡ T ⁢ norm ℎ ⁡ x ⁢ norm ℎ ⁡ x
41 recn ⊢ norm op ⁡ T ∈ ℝ → norm op ⁡ T ∈ ℂ
42 41 ad2antlr ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T ∈ ℂ
43 21 recnd ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm ℎ ⁡ x ∈ ℂ
44 42 43 43 mulassd ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T ⁢ norm ℎ ⁡ x ⁢ norm ℎ ⁡ x = norm op ⁡ T ⁢ norm ℎ ⁡ x ⁢ norm ℎ ⁡ x
45 simpr ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → x ∈ ℋ
46 ax-his3 ⊢ norm op ⁡ T ∈ ℂ ∧ x ∈ ℋ ∧ x ∈ ℋ → norm op ⁡ T ⋅ ℎ x ⋅ ih x = norm op ⁡ T ⁢ x ⋅ ih x
47 42 45 45 46 syl3anc ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T ⋅ ℎ x ⋅ ih x = norm op ⁡ T ⁢ x ⋅ ih x
48 20 recnd ⊢ x ∈ ℋ → norm ℎ ⁡ x ∈ ℂ
49 48 sqvald ⊢ x ∈ ℋ → norm ℎ ⁡ x 2 = norm ℎ ⁡ x ⁢ norm ℎ ⁡ x
50 normsq ⊢ x ∈ ℋ → norm ℎ ⁡ x 2 = x ⋅ ih x
51 49 50 eqtr3d ⊢ x ∈ ℋ → norm ℎ ⁡ x ⁢ norm ℎ ⁡ x = x ⋅ ih x
52 51 oveq2d ⊢ x ∈ ℋ → norm op ⁡ T ⁢ norm ℎ ⁡ x ⁢ norm ℎ ⁡ x = norm op ⁡ T ⁢ x ⋅ ih x
53 52 adantl ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T ⁢ norm ℎ ⁡ x ⁢ norm ℎ ⁡ x = norm op ⁡ T ⁢ x ⋅ ih x
54 47 53 eqtr4d ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T ⋅ ℎ x ⋅ ih x = norm op ⁡ T ⁢ norm ℎ ⁡ x ⁢ norm ℎ ⁡ x
55 44 54 eqtr4d ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T ⁢ norm ℎ ⁡ x ⁢ norm ℎ ⁡ x = norm op ⁡ T ⋅ ℎ x ⋅ ih x
56 hoif ⊢ I op : ℋ ⟶ 1-1 onto ℋ
57 f1of ⊢ I op : ℋ ⟶ 1-1 onto ℋ → I op : ℋ ⟶ ℋ
58 56 57 mp1i ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → I op : ℋ ⟶ ℋ
59 homval ⊢ norm op ⁡ T ∈ ℂ ∧ I op : ℋ ⟶ ℋ ∧ x ∈ ℋ → norm op ⁡ T · op I op ⁡ x = norm op ⁡ T ⋅ ℎ I op ⁡ x
60 42 58 45 59 syl3anc ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T · op I op ⁡ x = norm op ⁡ T ⋅ ℎ I op ⁡ x
61 hoival ⊢ x ∈ ℋ → I op ⁡ x = x
62 61 oveq2d ⊢ x ∈ ℋ → norm op ⁡ T ⋅ ℎ I op ⁡ x = norm op ⁡ T ⋅ ℎ x
63 62 adantl ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T ⋅ ℎ I op ⁡ x = norm op ⁡ T ⋅ ℎ x
64 60 63 eqtrd ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T · op I op ⁡ x = norm op ⁡ T ⋅ ℎ x
65 64 oveq1d ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T · op I op ⁡ x ⋅ ih x = norm op ⁡ T ⋅ ℎ x ⋅ ih x
66 55 65 eqtr4d ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm op ⁡ T ⁢ norm ℎ ⁡ x ⁢ norm ℎ ⁡ x = norm op ⁡ T · op I op ⁡ x ⋅ ih x
67 40 66 breqtrd ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ⁢ norm ℎ ⁡ x ≤ norm op ⁡ T · op I op ⁡ x ⋅ ih x
68 5 22 11 26 67 letrd ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ≤ norm op ⁡ T · op I op ⁡ x ⋅ ih x
69 2 5 11 13 68 letrd ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ≤ norm op ⁡ T · op I op ⁡ x ⋅ ih x
70 69 ralrimiva ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ → ∀ x ∈ ℋ T ⁡ x ⋅ ih x ≤ norm op ⁡ T · op I op ⁡ x ⋅ ih x
71 leop2 ⊢ T ∈ HrmOp ∧ norm op ⁡ T · op I op ∈ HrmOp → T ≤ op norm op ⁡ T · op I op ↔ ∀ x ∈ ℋ T ⁡ x ⋅ ih x ≤ norm op ⁡ T · op I op ⁡ x ⋅ ih x
72 8 71 sylan2 ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ → T ≤ op norm op ⁡ T · op I op ↔ ∀ x ∈ ℋ T ⁡ x ⋅ ih x ≤ norm op ⁡ T · op I op ⁡ x ⋅ ih x
73 70 72 mpbird ⊢ T ∈ HrmOp ∧ norm op ⁡ T ∈ ℝ → T ≤ op norm op ⁡ T · op I op