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

Metamath Proof Explorer

Theorem dfadj2

Description: Alternate definition of the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion dfadj2 adjℎ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) }

Proof

Step Hyp Ref Expression
1 df-adjh ⊢ adjℎ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) }
2 eqcom ⊢ ( ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) )
3 2 2ralbii ⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) )
4 adjsym ⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
5 3 4 bitr4id ⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) )
6 5 pm5.32i ⊢ ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) ↔ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) )
7 df-3an ⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) ↔ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) )
8 df-3an ⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) )
9 6 7 8 3bitr4i ⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) )
10 9 opabbii ⊢ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) } = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) }
11 1 10 eqtri ⊢ adjℎ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) }