Definition df-aj

Description: Define the adjoint of an operator (if it exists). The domain of U adj W is the set of all operators from U to W that have an adjoint. Definition 3.9-1 of Kreyszig p. 196, although we don't require that U and W be Hilbert spaces nor that the operators be linear. Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	df-aj	⊢ adj = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑢 ) ⟶ ( BaseSet ‘ 𝑤 ) ∧ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ ( BaseSet ‘ 𝑢 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		caj	⊢ adj
1		vu	⊢ 𝑢
2		cnv	⊢ NrmCVec
3		vw	⊢ 𝑤
4		vt	⊢ 𝑡
5		vs	⊢ 𝑠
6	4	cv	⊢ 𝑡
7		cba	⊢ BaseSet
8	1	cv	⊢ 𝑢
9	8 7	cfv	⊢ ( BaseSet ‘ 𝑢 )
10	3	cv	⊢ 𝑤
11	10 7	cfv	⊢ ( BaseSet ‘ 𝑤 )
12	9 11 6	wf	⊢ 𝑡 : ( BaseSet ‘ 𝑢 ) ⟶ ( BaseSet ‘ 𝑤 )
13	5	cv	⊢ 𝑠
14	11 9 13	wf	⊢ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ ( BaseSet ‘ 𝑢 )
15		vx	⊢ 𝑥
16		vy	⊢ 𝑦
17	15	cv	⊢ 𝑥
18	17 6	cfv	⊢ ( 𝑡 ‘ 𝑥 )
19		cdip	⊢ ·𝑖OLD
20	10 19	cfv	⊢ ( ·𝑖OLD ‘ 𝑤 )
21	16	cv	⊢ 𝑦
22	18 21 20	co	⊢ ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 )
23	8 19	cfv	⊢ ( ·𝑖OLD ‘ 𝑢 )
24	21 13	cfv	⊢ ( 𝑠 ‘ 𝑦 )
25	17 24 23	co	⊢ ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) )
26	22 25	wceq	⊢ ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) )
27	26 16 11	wral	⊢ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) )
28	27 15 9	wral	⊢ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) )
29	12 14 28	w3a	⊢ ( 𝑡 : ( BaseSet ‘ 𝑢 ) ⟶ ( BaseSet ‘ 𝑤 ) ∧ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ ( BaseSet ‘ 𝑢 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) )
30	29 4 5	copab	⊢ { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑢 ) ⟶ ( BaseSet ‘ 𝑤 ) ∧ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ ( BaseSet ‘ 𝑢 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ) }
31	1 3 2 2 30	cmpo	⊢ ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑢 ) ⟶ ( BaseSet ‘ 𝑤 ) ∧ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ ( BaseSet ‘ 𝑢 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ) } )
32	0 31	wceq	⊢ adj = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑢 ) ⟶ ( BaseSet ‘ 𝑤 ) ∧ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ ( BaseSet ‘ 𝑢 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ) } )