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 ⊢A=UadjW
ajfuni.u ⊢U∈CPreHilOLD
ajfuni.w ⊢W∈NrmCVec
Assertion ajfuni ⊢Fun⁡A

Proof

Step Hyp Ref Expression
1 ajfuni.5 ⊢A=UadjW
2 ajfuni.u ⊢U∈CPreHilOLD
3 ajfuni.w ⊢W∈NrmCVec
4 funopab ⊢Fun⁡ts|t:BaseSet⁡U⟶BaseSet⁡W∧s:BaseSet⁡W⟶BaseSet⁡U∧∀x∈BaseSet⁡U∀y∈BaseSet⁡Wt⁡x⋅𝑖OLD⁡Wy=x⋅𝑖OLD⁡Us⁡y↔∀t∃*st:BaseSet⁡U⟶BaseSet⁡W∧s:BaseSet⁡W⟶BaseSet⁡U∧∀x∈BaseSet⁡U∀y∈BaseSet⁡Wt⁡x⋅𝑖OLD⁡Wy=x⋅𝑖OLD⁡Us⁡y
5 eqid ⊢BaseSet⁡U=BaseSet⁡U
6 eqid ⊢⋅𝑖OLD⁡U=⋅𝑖OLD⁡U
7 5 6 2 ajmoi ⊢∃*ss:BaseSet⁡W⟶BaseSet⁡U∧∀x∈BaseSet⁡U∀y∈BaseSet⁡Wt⁡x⋅𝑖OLD⁡Wy=x⋅𝑖OLD⁡Us⁡y
8 3simpc ⊢t:BaseSet⁡U⟶BaseSet⁡W∧s:BaseSet⁡W⟶BaseSet⁡U∧∀x∈BaseSet⁡U∀y∈BaseSet⁡Wt⁡x⋅𝑖OLD⁡Wy=x⋅𝑖OLD⁡Us⁡y→s:BaseSet⁡W⟶BaseSet⁡U∧∀x∈BaseSet⁡U∀y∈BaseSet⁡Wt⁡x⋅𝑖OLD⁡Wy=x⋅𝑖OLD⁡Us⁡y
9 8 moimi ⊢∃*ss:BaseSet⁡W⟶BaseSet⁡U∧∀x∈BaseSet⁡U∀y∈BaseSet⁡Wt⁡x⋅𝑖OLD⁡Wy=x⋅𝑖OLD⁡Us⁡y→∃*st:BaseSet⁡U⟶BaseSet⁡W∧s:BaseSet⁡W⟶BaseSet⁡U∧∀x∈BaseSet⁡U∀y∈BaseSet⁡Wt⁡x⋅𝑖OLD⁡Wy=x⋅𝑖OLD⁡Us⁡y
10 7 9 ax-mp ⊢∃*st:BaseSet⁡U⟶BaseSet⁡W∧s:BaseSet⁡W⟶BaseSet⁡U∧∀x∈BaseSet⁡U∀y∈BaseSet⁡Wt⁡x⋅𝑖OLD⁡Wy=x⋅𝑖OLD⁡Us⁡y
11 4 10 mpgbir ⊢Fun⁡ts|t:BaseSet⁡U⟶BaseSet⁡W∧s:BaseSet⁡W⟶BaseSet⁡U∧∀x∈BaseSet⁡U∀y∈BaseSet⁡Wt⁡x⋅𝑖OLD⁡Wy=x⋅𝑖OLD⁡Us⁡y
12 2 phnvi ⊢U∈NrmCVec
13 eqid ⊢BaseSet⁡W=BaseSet⁡W
14 eqid ⊢⋅𝑖OLD⁡W=⋅𝑖OLD⁡W
15 5 13 6 14 1 ajfval ⊢U∈NrmCVec∧W∈NrmCVec→A=ts|t:BaseSet⁡U⟶BaseSet⁡W∧s:BaseSet⁡W⟶BaseSet⁡U∧∀x∈BaseSet⁡U∀y∈BaseSet⁡Wt⁡x⋅𝑖OLD⁡Wy=x⋅𝑖OLD⁡Us⁡y
16 12 3 15 mp2an ⊢A=ts|t:BaseSet⁡U⟶BaseSet⁡W∧s:BaseSet⁡W⟶BaseSet⁡U∧∀x∈BaseSet⁡U∀y∈BaseSet⁡Wt⁡x⋅𝑖OLD⁡Wy=x⋅𝑖OLD⁡Us⁡y
17 16 funeqi ⊢Fun⁡A↔Fun⁡ts|t:BaseSet⁡U⟶BaseSet⁡W∧s:BaseSet⁡W⟶BaseSet⁡U∧∀x∈BaseSet⁡U∀y∈BaseSet⁡Wt⁡x⋅𝑖OLD⁡Wy=x⋅𝑖OLD⁡Us⁡y
18 11 17 mpbir ⊢Fun⁡A