Metamath Proof Explorer

Theorem ajfval

Description: The adjoint function. (Contributed by NM, 25-Jan-2008) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ajfval.1 ⊢X=BaseSet⁡U
2 ajfval.2 ⊢Y=BaseSet⁡W
3 ajfval.3 ⊢P=⋅𝑖OLD⁡U
4 ajfval.4 ⊢Q=⋅𝑖OLD⁡W
5 ajfval.5 ⊢A=UadjW
6 fveq2 ⊢u=U→BaseSet⁡u=BaseSet⁡U
7 6 1 eqtr4di ⊢u=U→BaseSet⁡u=X
8 7 feq2d ⊢u=U→t:BaseSet⁡u⟶BaseSet⁡w↔t:X⟶BaseSet⁡w
9 7 feq3d ⊢u=U→s:BaseSet⁡w⟶BaseSet⁡u↔s:BaseSet⁡w⟶X
10 fveq2 ⊢u=U→⋅𝑖OLD⁡u=⋅𝑖OLD⁡U
11 10 3 eqtr4di ⊢u=U→⋅𝑖OLD⁡u=P
12 11 oveqd ⊢u=U→x⋅𝑖OLD⁡us⁡y=xPs⁡y
13 12 eqeq2d ⊢u=U→t⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y↔t⁡x⋅𝑖OLD⁡wy=xPs⁡y
14 13 ralbidv ⊢u=U→∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y↔∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=xPs⁡y
15 7 14 raleqbidv ⊢u=U→∀x∈BaseSet⁡u∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y↔∀x∈X∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=xPs⁡y
16 8 9 15 3anbi123d ⊢u=U→t:BaseSet⁡u⟶BaseSet⁡w∧s:BaseSet⁡w⟶BaseSet⁡u∧∀x∈BaseSet⁡u∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y↔t:X⟶BaseSet⁡w∧s:BaseSet⁡w⟶X∧∀x∈X∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=xPs⁡y
17 16 opabbidv ⊢u=U→ts|t:BaseSet⁡u⟶BaseSet⁡w∧s:BaseSet⁡w⟶BaseSet⁡u∧∀x∈BaseSet⁡u∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y=ts|t:X⟶BaseSet⁡w∧s:BaseSet⁡w⟶X∧∀x∈X∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=xPs⁡y
18 fveq2 ⊢w=W→BaseSet⁡w=BaseSet⁡W
19 18 2 eqtr4di ⊢w=W→BaseSet⁡w=Y
20 19 feq3d ⊢w=W→t:X⟶BaseSet⁡w↔t:X⟶Y
21 19 feq2d ⊢w=W→s:BaseSet⁡w⟶X↔s:Y⟶X
22 fveq2 ⊢w=W→⋅𝑖OLD⁡w=⋅𝑖OLD⁡W
23 22 4 eqtr4di ⊢w=W→⋅𝑖OLD⁡w=Q
24 23 oveqd ⊢w=W→t⁡x⋅𝑖OLD⁡wy=t⁡xQy
25 24 eqeq1d ⊢w=W→t⁡x⋅𝑖OLD⁡wy=xPs⁡y↔t⁡xQy=xPs⁡y
26 19 25 raleqbidv ⊢w=W→∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=xPs⁡y↔∀y∈Yt⁡xQy=xPs⁡y
27 26 ralbidv ⊢w=W→∀x∈X∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=xPs⁡y↔∀x∈X∀y∈Yt⁡xQy=xPs⁡y
28 20 21 27 3anbi123d ⊢w=W→t:X⟶BaseSet⁡w∧s:BaseSet⁡w⟶X∧∀x∈X∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=xPs⁡y↔t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y
29 28 opabbidv ⊢w=W→ts|t:X⟶BaseSet⁡w∧s:BaseSet⁡w⟶X∧∀x∈X∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=xPs⁡y=ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y
30 df-aj ⊢adj=u∈NrmCVec,w∈NrmCVec⟼ts|t:BaseSet⁡u⟶BaseSet⁡w∧s:BaseSet⁡w⟶BaseSet⁡u∧∀x∈BaseSet⁡u∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y
31 ovex ⊢YX∈V
32 ovex ⊢XY∈V
33 31 32 xpex ⊢YX×XY∈V
34 2 fvexi ⊢Y∈V
35 1 fvexi ⊢X∈V
36 34 35 elmap ⊢t∈YX↔t:X⟶Y
37 35 34 elmap ⊢s∈XY↔s:Y⟶X
38 36 37 anbi12i ⊢t∈YX∧s∈XY↔t:X⟶Y∧s:Y⟶X
39 38 biimpri ⊢t:X⟶Y∧s:Y⟶X→t∈YX∧s∈XY
40 39 3adant3 ⊢t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y→t∈YX∧s∈XY
41 40 ssopab2i ⊢ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y⊆ts|t∈YX∧s∈XY
42 df-xp ⊢YX×XY=ts|t∈YX∧s∈XY
43 41 42 sseqtrri ⊢ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y⊆YX×XY
44 33 43 ssexi ⊢ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y∈V
45 17 29 30 44 ovmpo ⊢U∈NrmCVec∧W∈NrmCVec→UadjW=ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y
46 5 45 eqtrid ⊢U∈NrmCVec∧W∈NrmCVec→A=ts|t:X⟶Y∧s:Y⟶X∧∀x∈X∀y∈Yt⁡xQy=xPs⁡y