Metamath Proof Explorer

Theorem ellnop

Description: Property defining a linear Hilbert space operator. (Contributed by NM, 18-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion ellnop ⊢ T ∈ LinOp ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ t = T → t ⁡ x ⋅ ℎ y + ℎ z = T ⁡ x ⋅ ℎ y + ℎ z
2 fveq1 ⊢ t = T → t ⁡ y = T ⁡ y
3 2 oveq2d ⊢ t = T → x ⋅ ℎ t ⁡ y = x ⋅ ℎ T ⁡ y
4 fveq1 ⊢ t = T → t ⁡ z = T ⁡ z
5 3 4 oveq12d ⊢ t = T → x ⋅ ℎ t ⁡ y + ℎ t ⁡ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z
6 1 5 eqeq12d ⊢ t = T → t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z ↔ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z
7 6 ralbidv ⊢ t = T → ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z ↔ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z
8 7 2ralbidv ⊢ t = T → ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z ↔ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z
9 df-lnop ⊢ LinOp = t ∈ ℋ ℋ | ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z
10 8 9 elrab2 ⊢ T ∈ LinOp ↔ T ∈ ℋ ℋ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z
11 ax-hilex ⊢ ℋ ∈ V
12 11 11 elmap ⊢ T ∈ ℋ ℋ ↔ T : ℋ ⟶ ℋ
13 12 anbi1i ⊢ T ∈ ℋ ℋ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z
14 10 13 bitri ⊢ T ∈ LinOp ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z