Metamath Proof Explorer

Theorem ajval

Description: Value of the adjoint function. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ajval.1 ⊢X=BaseSet⁡U
ajval.2 ⊢Y=BaseSet⁡W
ajval.3 ⊢P=⋅𝑖OLD⁡U
ajval.4 ⊢Q=⋅𝑖OLD⁡W
ajval.5 ⊢A=UadjW
Assertion ajval ⊢U∈CPreHilOLD∧W∈NrmCVec∧T:X⟶Y→A⁡T=ιs|s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y

Proof

Step Hyp Ref Expression
1 ajval.1 ⊢X=BaseSet⁡U
2 ajval.2 ⊢Y=BaseSet⁡W
3 ajval.3 ⊢P=⋅𝑖OLD⁡U
4 ajval.4 ⊢Q=⋅𝑖OLD⁡W
5 ajval.5 ⊢A=UadjW
6 phnv ⊢U∈CPreHilOLD→U∈NrmCVec
7 1 2 3 4 5 ajfval ⊢U∈NrmCVec∧W∈NrmCVec→A=ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y
8 6 7 sylan ⊢U∈CPreHilOLD∧W∈NrmCVec→A=ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y
9 8 fveq1d ⊢U∈CPreHilOLD∧W∈NrmCVec→A⁡T=ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y⁡T
10 9 3adant3 ⊢U∈CPreHilOLD∧W∈NrmCVec∧T:X⟶Y→A⁡T=ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y⁡T
11 1 fvexi ⊢X∈V
12 fex ⊢T:X⟶Y∧X∈V→T∈V
13 11 12 mpan2 ⊢T:X⟶Y→T∈V
14 eqid ⊢ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y=ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y
15 feq1 ⊢t=T→t:X⟶Y↔T:X⟶Y
16 fveq1 ⊢t=T→t⁡x=T⁡x
17 16 oveq1d ⊢t=T→t⁡xQy=T⁡xQy
18 17 eqeq1d ⊢t=T→t⁡xQy=xPs⁡y↔T⁡xQy=xPs⁡y
19 18 2ralbidv ⊢t=T→∀x∈X∀y∈Yt⁡xQy=xPs⁡y↔∀x∈X∀y∈YT⁡xQy=xPs⁡y
20 15 19 3anbi13d ⊢t=T→t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y↔T:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y
21 14 20 fvopab5 ⊢T∈V→ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y⁡T=ιs|T:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y
22 13 21 syl ⊢T:X⟶Y→ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y⁡T=ιs|T:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y
23 3anass ⊢T:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y↔T:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y
24 23 baib ⊢T:X⟶Y→T:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y↔s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y
25 24 iotabidv ⊢T:X⟶Y→ιs|T:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y=ιs|s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y
26 22 25 eqtrd ⊢T:X⟶Y→ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y⁡T=ιs|s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y
27 26 3ad2ant3 ⊢U∈CPreHilOLD∧W∈NrmCVec∧T:X⟶Y→ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y⁡T=ιs|s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y
28 10 27 eqtrd ⊢U∈CPreHilOLD∧W∈NrmCVec∧T:X⟶Y→A⁡T=ιs|s:Y⟶X∧∀x∈X∀y∈YT⁡xQy=xPs⁡y