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

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 ( 𝑇 ∈ LinOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) )
2 fveq1 ⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) )
3 2 oveq2d ⊢ ( 𝑡 = 𝑇 → ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) )
4 fveq1 ⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑧 ) )
5 3 4 oveq12d ⊢ ( 𝑡 = 𝑇 → ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) )
6 1 5 eqeq12d ⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) ) ↔ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
7 6 ralbidv ⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
8 7 2ralbidv ⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) ) ↔ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
9 df-lnop ⊢ LinOp = { 𝑡 ∈ ( ℋ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) ) }
10 8 9 elrab2 ⊢ ( 𝑇 ∈ LinOp ↔ ( 𝑇 ∈ ( ℋ ↑m ℋ ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
11 ax-hilex ⊢ ℋ ∈ V
12 11 11 elmap ⊢ ( 𝑇 ∈ ( ℋ ↑m ℋ ) ↔ 𝑇 : ℋ ⟶ ℋ )
13 12 anbi1i ⊢ ( ( 𝑇 ∈ ( ℋ ↑m ℋ ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
14 10 13 bitri ⊢ ( 𝑇 ∈ LinOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )