Definition df-adjh

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
0		cado	⊢ adjℎ
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 ( 𝑢 ‘ 𝑦 ) ) ) }