Metamath Proof Explorer

Theorem hmopbdoptHIL

Description: A Hermitian operator is a bounded linear operator (Hellinger-Toeplitz Theorem). (Contributed by NM, 18-Jan-2008) (New usage is discouraged.)

Ref Expression
Assertion hmopbdoptHIL ⊢ T ∈ HrmOp → T ∈ BndLinOp

Proof

Step Hyp Ref Expression
1 hmoplin ⊢ T ∈ HrmOp → T ∈ LinOp
2 hmop ⊢ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
3 2 3expib ⊢ T ∈ HrmOp → x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
4 3 ralrimivv ⊢ T ∈ HrmOp → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
5 hilhl ⊢ + ℎ ⋅ ℎ norm ℎ ∈ CHil OLD
6 df-hba ⊢ ℋ = BaseSet ⁡ + ℎ ⋅ ℎ norm ℎ
7 eqid ⊢ + ℎ ⋅ ℎ norm ℎ = + ℎ ⋅ ℎ norm ℎ
8 7 hhip ⊢ ⋅ ih = ⋅ 𝑖OLD ⁡ + ℎ ⋅ ℎ norm ℎ
9 eqid ⊢ + ℎ ⋅ ℎ norm ℎ LnOp + ℎ ⋅ ℎ norm ℎ = + ℎ ⋅ ℎ norm ℎ LnOp + ℎ ⋅ ℎ norm ℎ
10 7 9 hhlnoi ⊢ LinOp = + ℎ ⋅ ℎ norm ℎ LnOp + ℎ ⋅ ℎ norm ℎ
11 eqid ⊢ + ℎ ⋅ ℎ norm ℎ BLnOp + ℎ ⋅ ℎ norm ℎ = + ℎ ⋅ ℎ norm ℎ BLnOp + ℎ ⋅ ℎ norm ℎ
12 7 11 hhbloi ⊢ BndLinOp = + ℎ ⋅ ℎ norm ℎ BLnOp + ℎ ⋅ ℎ norm ℎ
13 6 8 10 12 htth ⊢ + ℎ ⋅ ℎ norm ℎ ∈ CHil OLD ∧ T ∈ LinOp ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y → T ∈ BndLinOp
14 5 13 mp3an1 ⊢ T ∈ LinOp ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y → T ∈ BndLinOp
15 1 4 14 syl2anc ⊢ T ∈ HrmOp → T ∈ BndLinOp