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 adjsym ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
3 eqcom ( ( ( 𝑡𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) )
4 3 2ralbii ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) )
5 2 4 syl6rbbr ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡𝑥 ) ·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 𝑦 ) ) }