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