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

Metamath Proof Explorer

Theorem ajfuni

Description: The adjoint function is a function. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ajfuni.5 ⊢ 𝐴 = ( 𝑈 adj 𝑊 )
ajfuni.u ⊢ 𝑈 ∈ CPreHilOLD
ajfuni.w ⊢ 𝑊 ∈ NrmCVec
Assertion ajfuni Fun 𝐴

Proof

Step Hyp Ref Expression
1 ajfuni.5 ⊢ 𝐴 = ( 𝑈 adj 𝑊 )
2 ajfuni.u ⊢ 𝑈 ∈ CPreHilOLD
3 ajfuni.w ⊢ 𝑊 ∈ NrmCVec
4 funopab ⊢ ( Fun { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) } ↔ ∀ 𝑡 ∃* 𝑠 ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) )
5 eqid ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
6 eqid ⊢ ( ·𝑖OLD ‘ 𝑈 ) = ( ·𝑖OLD ‘ 𝑈 )
7 5 6 2 ajmoi ⊢ ∃* 𝑠 ( 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) )
8 3simpc ⊢ ( ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) → ( 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) )
9 8 moimi ⊢ ( ∃* 𝑠 ( 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) → ∃* 𝑠 ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) )
10 7 9 ax-mp ⊢ ∃* 𝑠 ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) )
11 4 10 mpgbir ⊢ Fun { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) }
12 2 phnvi ⊢ 𝑈 ∈ NrmCVec
13 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
14 eqid ⊢ ( ·𝑖OLD ‘ 𝑊 ) = ( ·𝑖OLD ‘ 𝑊 )
15 5 13 6 14 1 ajfval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐴 = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) } )
16 12 3 15 mp2an ⊢ 𝐴 = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) }
17 16 funeqi ⊢ ( Fun 𝐴 ↔ Fun { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) } )
18 11 17 mpbir ⊢ Fun 𝐴