This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hhlnoi

Description: The linear operators of Hilbert space. (Contributed by NM, 19-Nov-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses hhlno.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
hhlno.2 ⊢ L = U LnOp U
Assertion hhlnoi ⊢ LinOp = L

Proof

Step Hyp Ref Expression
1 hhlno.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 hhlno.2 ⊢ L = U LnOp U
3 df-lnop ⊢ LinOp = t ∈ ℋ ℋ | ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z
4 1 hhnv ⊢ U ∈ NrmCVec
5 1 hhba ⊢ ℋ = BaseSet ⁡ U
6 1 hhva ⊢ + ℎ = + v ⁡ U
7 1 hhsm ⊢ ⋅ ℎ = ⋅ 𝑠OLD ⁡ U
8 5 5 6 6 7 7 2 lnoval ⊢ U ∈ NrmCVec ∧ U ∈ NrmCVec → L = t ∈ ℋ ℋ | ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z
9 4 4 8 mp2an ⊢ L = t ∈ ℋ ℋ | ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z
10 3 9 eqtr4i ⊢ LinOp = L