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 = U adj W
Assertion ajfval U NrmCVec W NrmCVec A = t s | t : X Y s : Y X x X y Y t x Q y = x P s 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 = U adj W
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 u s y = x P s y
13 12 eqeq2d u = U t x 𝑖OLD w y = x 𝑖OLD u s y t x 𝑖OLD w y = x P s y
14 13 ralbidv u = U y BaseSet w t x 𝑖OLD w y = x 𝑖OLD u s y y BaseSet w t x 𝑖OLD w y = x P s y
15 7 14 raleqbidv u = U x BaseSet u y BaseSet w t x 𝑖OLD w y = x 𝑖OLD u s y x X y BaseSet w t x 𝑖OLD w y = x P s y
16 8 9 15 3anbi123d u = U t : BaseSet u BaseSet w s : BaseSet w BaseSet u x BaseSet u y BaseSet w t x 𝑖OLD w y = x 𝑖OLD u s y t : X BaseSet w s : BaseSet w X x X y BaseSet w t x 𝑖OLD w y = x P s y
17 16 opabbidv u = U t s | t : BaseSet u BaseSet w s : BaseSet w BaseSet u x BaseSet u y BaseSet w t x 𝑖OLD w y = x 𝑖OLD u s y = t s | t : X BaseSet w s : BaseSet w X x X y BaseSet w t x 𝑖OLD w y = x P s 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 w y = t x Q y
25 24 eqeq1d w = W t x 𝑖OLD w y = x P s y t x Q y = x P s y
26 19 25 raleqbidv w = W y BaseSet w t x 𝑖OLD w y = x P s y y Y t x Q y = x P s y
27 26 ralbidv w = W x X y BaseSet w t x 𝑖OLD w y = x P s y x X y Y t x Q y = x P s y
28 20 21 27 3anbi123d w = W t : X BaseSet w s : BaseSet w X x X y BaseSet w t x 𝑖OLD w y = x P s y t : X Y s : Y X x X y Y t x Q y = x P s y
29 28 opabbidv w = W t s | t : X BaseSet w s : BaseSet w X x X y BaseSet w t x 𝑖OLD w y = x P s y = t s | t : X Y s : Y X x X y Y t x Q y = x P s y
30 df-aj adj = u NrmCVec , w NrmCVec t s | t : BaseSet u BaseSet w s : BaseSet w BaseSet u x BaseSet u y BaseSet w t x 𝑖OLD w y = x 𝑖OLD u s y
31 ovex Y X V
32 ovex X Y V
33 31 32 xpex Y X × X Y V
34 2 fvexi Y V
35 1 fvexi X V
36 34 35 elmap t Y X t : X Y
37 35 34 elmap s X Y s : Y X
38 36 37 anbi12i t Y X s X Y t : X Y s : Y X
39 38 biimpri t : X Y s : Y X t Y X s X Y
40 39 3adant3 t : X Y s : Y X x X y Y t x Q y = x P s y t Y X s X Y
41 40 ssopab2i t s | t : X Y s : Y X x X y Y t x Q y = x P s y t s | t Y X s X Y
42 df-xp Y X × X Y = t s | t Y X s X Y
43 41 42 sseqtrri t s | t : X Y s : Y X x X y Y t x Q y = x P s y Y X × X Y
44 33 43 ssexi t s | t : X Y s : Y X x X y Y t x Q y = x P s y V
45 17 29 30 44 ovmpo U NrmCVec W NrmCVec U adj W = t s | t : X Y s : Y X x X y Y t x Q y = x P s y
46 5 45 syl5eq U NrmCVec W NrmCVec A = t s | t : X Y s : Y X x X y Y t x Q y = x P s y