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

Metamath Proof Explorer

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 ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ) } )