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

Metamath Proof Explorer

Theorem elhmop

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

		Ref	Expression
	Assertion	elhmop	⊢ ( 𝑇 ∈ HrmOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) )
2	1	oveq2d	⊢ ( 𝑡 = 𝑇 → ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·_ih ( 𝑇 ‘ 𝑦 ) ) )
3		fveq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
4	3	oveq1d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 ‘ 𝑥 ) ·_ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) )
5	2 4	eqeq12d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·_ih 𝑦 ) ↔ ( 𝑥 ·_ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) ) )
6	5	2ralbidv	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·_ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) ) )
7		df-hmop	⊢ HrmOp = { 𝑡 ∈ ( ℋ ↑_m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·_ih 𝑦 ) }
8	6 7	elrab2	⊢ ( 𝑇 ∈ HrmOp ↔ ( 𝑇 ∈ ( ℋ ↑_m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) ) )
9		ax-hilex	⊢ ℋ ∈ V
10	9 9	elmap	⊢ ( 𝑇 ∈ ( ℋ ↑_m ℋ ) ↔ 𝑇 : ℋ ⟶ ℋ )
11	10	anbi1i	⊢ ( ( 𝑇 ∈ ( ℋ ↑_m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) ) )
12	8 11	bitri	⊢ ( 𝑇 ∈ HrmOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) ) )