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 ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) → 𝑇 ≤op ( ( normop ‘ 𝑇 ) ·op Iop ) )

Proof

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