Metamath Proof Explorer

Description: Define the adjoint of a Hilbert space operator (if it exists). The domain of adjh is the set of all adjoint operators. Definition of adjoint in Kalmbach2 p. 8. Unlike Kalmbach (and most authors), we do not demand that the operator be linear, but instead show (in adjbdln ) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

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

Detailed syntax breakdown

Step Hyp Ref Expression
1 vt 𝑡
2 vu 𝑢
3 1 cv 𝑡
4 chba
5 4 4 3 wf 𝑡 : ℋ ⟶ ℋ
6 2 cv 𝑢
7 4 4 6 wf 𝑢 : ℋ ⟶ ℋ
8 vx 𝑥
9 vy 𝑦
10 8 cv 𝑥
11 10 3 cfv ( 𝑡𝑥 )
12 csp ·ih
13 9 cv 𝑦
14 11 13 12 co ( ( 𝑡𝑥 ) ·ih 𝑦 )
15 13 6 cfv ( 𝑢𝑦 )
16 10 15 12 co ( 𝑥 ·ih ( 𝑢𝑦 ) )
17 14 16 wceq ( ( 𝑡𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢𝑦 ) )
18 17 9 4 wral 𝑦 ∈ ℋ ( ( 𝑡𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢𝑦 ) )
19 18 8 4 wral 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢𝑦 ) )
20 5 7 19 w3a ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢𝑦 ) ) )
21 20 1 2 copab { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢𝑦 ) ) ) }
22 0 21 wceq adj = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢𝑦 ) ) ) }