HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem cnvadj 9756
Description: The adjoint function equals its converse.
Assertion
Ref Expression
cnvadj |- `'adjh = adjh
Proof of Theorem cnvadj
StepHypRef Expression
1 cnvopab 3437 . . 3 |- `'{<.u, t>. | (u:H~-->H~ /\ t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (u` y)) = ((t` x) .ih y))} = {<.t, u>. | (u:H~-->H~ /\ t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (u` y)) = ((t` x) .ih y))}
2 3ancoma 781 . . . . 5 |- ((u:H~-->H~ /\ t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (u` y)) = ((t` x) .ih y)) <-> (t:H~-->H~ /\ u:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (u` y)) = ((t` x) .ih y)))
3 ax-his1 8888 . . . . . . . . . . . . . . . . . 18 |- (((u` y) e. H~ /\ x e. H~) -> ((u` y) .ih x) = (*` (x .ih (u` y))))
4 ffvelrn 3805 . . . . . . . . . . . . . . . . . 18 |- ((u:H~-->H~ /\ y e. H~) -> (u` y) e. H~)
53, 4sylan 448 . . . . . . . . . . . . . . . . 17 |- (((u:H~-->H~ /\ y e. H~) /\ x e. H~) -> ((u` y) .ih x) = (*` (x .ih (u` y))))
65adantrl 394 . . . . . . . . . . . . . . . 16 |- (((u:H~-->H~ /\ y e. H~) /\ (t:H~-->H~ /\ x e. H~)) -> ((u` y) .ih x) = (*` (x .ih (u` y))))
7 ax-his1 8888 . . . . . . . . . . . . . . . . . 18 |- ((y e. H~ /\ (t` x) e. H~) -> (y .ih (t` x)) = (*` ((t` x) .ih y)))
8 ffvelrn 3805 . . . . . . . . . . . . . . . . . 18 |- ((t:H~-->H~ /\ x e. H~) -> (t` x) e. H~)
97, 8sylan2 451 . . . . . . . . . . . . . . . . 17 |- ((y e. H~ /\ (t:H~-->H~ /\ x e. H~)) -> (y .ih (t` x)) = (*` ((t` x) .ih y)))
109adantll 392 . . . . . . . . . . . . . . . 16 |- (((u:H~-->H~ /\ y e. H~) /\ (t:H~-->H~ /\ x e. H~)) -> (y .ih (t` x)) = (*` ((t` x) .ih y)))
116, 10eqeq12d 1486 . . . . . . . . . . . . . . 15 |- (((u:H~-->H~ /\ y e. H~) /\ (t:H~-->H~ /\ x e. H~)) -> (((u` y) .ih x) = (y .ih (t` x)) <-> (*` (x .ih (u` y))) = (*` ((t` x) .ih y))))
1211ancoms 436 . . . . . . . . . . . . . 14 |- (((t:H~-->H~ /\ x e. H~) /\ (u:H~-->H~ /\ y e. H~)) -> (((u` y) .ih x) = (y .ih (t` x)) <-> (*` (x .ih (u` y))) = (*` ((t` x) .ih y))))
13 cj11t 6773 . . . . . . . . . . . . . . 15 |- (((x .ih (u` y)) e. CC /\ ((t` x) .ih y) e. CC) -> ((*` (x .ih (u` y))) = (*` ((t` x) .ih y)) <-> (x .ih (u` y)) = ((t` x) .ih y)))
14 hiclt 8886 . . . . . . . . . . . . . . . . 17 |- ((x e. H~ /\ (u` y) e. H~) -> (x .ih (u` y)) e. CC)
1514, 4sylan2 451 . . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ (u:H~-->H~ /\ y e. H~)) -> (x .ih (u` y)) e. CC)
1615adantll 392 . . . . . . . . . . . . . . 15 |- (((t:H~-->H~ /\ x e. H~) /\ (u:H~-->H~ /\ y e. H~)) -> (x .ih (u` y)) e. CC)
17 hiclt 8886 . . . . . . . . . . . . . . . . 17 |- (((t` x) e. H~ /\ y e. H~) -> ((t` x) .ih y) e. CC)
1817, 8sylan 448 . . . . . . . . . . . . . . . 16 |- (((t:H~-->H~ /\ x e. H~) /\ y e. H~) -> ((t` x) .ih y) e. CC)
1918adantrl 394 . . . . . . . . . . . . . . 15 |- (((t:H~-->H~ /\ x e. H~) /\ (u:H~-->H~ /\ y e. H~)) -> ((t` x) .ih y) e. CC)
2013, 16, 19sylanc 471 . . . . . . . . . . . . . 14 |- (((t:H~-->H~ /\ x e. H~) /\ (u:H~-->H~ /\ y e. H~)) -> ((*` (x .ih (u` y))) = (*` ((t` x) .ih y)) <-> (x .ih (u` y)) = ((t` x) .ih y)))
2112, 20bitr2d 528 . . . . . . . . . . . . 13 |- (((t:H~-->H~ /\ x e. H~) /\ (u:H~-->H~ /\ y e. H~)) -> ((x .ih (u` y)) = ((t` x) .ih y) <-> ((u` y) .ih x) = (y .ih (t` x))))
2221an4s 508 . . . . . . . . . . . 12 |- (((t:H~-->H~ /\ u:H~-->H~) /\ (x e. H~ /\ y e. H~)) -> ((x .ih (u` y)) = ((t` x) .ih y) <-> ((u` y) .ih x) = (y .ih (t` x))))
2322anassrs 441 . . . . . . . . . . 11 |- ((((t:H~-->H~ /\ u:H~-->H~) /\ x e. H~) /\ y e. H~) -> ((x .ih (u` y)) = ((t` x) .ih y) <-> ((u` y) .ih x) = (y .ih (t` x))))
24 eqcom 1474 . . . . . . . . . . 11 |- (((u` y) .ih x) = (y .ih (t` x)) <-> (y .ih (t` x)) = ((u` y) .ih x))
2523, 24syl6bb 535 . . . . . . . . . 10 |- ((((t:H~-->H~ /\ u:H~-->H~) /\ x e. H~) /\ y e. H~) -> ((x .ih (u` y)) = ((t` x) .ih y) <-> (y .ih (t` x)) = ((u` y) .ih x)))
2625ralbidva 1656 . . . . . . . . 9 |- (((t:H~-->H~ /\ u:H~-->H~) /\ x e. H~) -> (A.y e. H~ (x .ih (u` y)) = ((t` x) .ih y) <-> A.y e. H~ (y .ih (t` x)) = ((u` y) .ih x)))
2726ralbidva 1656 . . . . . . . 8 |- ((t:H~-->H~ /\ u:H~-->H~) -> (A.x e. H~ A.y e. H~ (x .ih (u` y)) = ((t` x) .ih y) <-> A.x e. H~ A.y e. H~ (y .ih (t` x)) = ((u` y) .ih x)))
28 ralcom 1771 . . . . . . . 8 |- (A.x e. H~ A.y e. H~ (y .ih (t` x)) = ((u` y) .ih x) <-> A.y e. H~ A.x e. H~ (y .ih (t` x)) = ((u` y) .ih x))
2927, 28syl6bb 535 . . . . . . 7 |- ((t:H~-->H~ /\ u:H~-->H~) -> (A.x e. H~ A.y e. H~ (x .ih (u` y)) = ((t` x) .ih y) <-> A.y e. H~ A.x e. H~ (y .ih (t` x)) = ((u` y) .ih x)))
3029pm5.32i 644 . . . . . 6 |- (((t:H~-->H~ /\ u:H~-->H~) /\ A.x e. H~ A.y e. H~ (x .ih (u` y)) = ((t` x) .ih y)) <-> ((t:H~-->H~ /\ u:H~-->H~) /\ A.y e. H~ A.x e. H~ (y .ih (t` x)) = ((u` y) .ih x)))
31 df-3an 776 . . . . . 6 |- ((t:H~-->H~ /\ u:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (u` y)) = ((t` x) .ih y)) <-> ((t:H~-->H~ /\ u:H~-->H~) /\ A.x e. H~ A.y e. H~ (x .ih (u` y)) = ((t` x) .ih y)))
32 df-3an 776 . . . . . 6 |- ((t:H~-->H~ /\ u:H~-->H~ /\ A.y e. H~ A.x e. H~ (y .ih (t` x)) = ((u` y) .ih x)) <-> ((t:H~-->H~ /\ u:H~-->H~) /\ A.y e. H~ A.x e. H~ (y .ih (t` x)) = ((u` y) .ih x)))
3330, 31, 323bitr4 183 . . . . 5 |- ((t:H~-->H~ /\ u:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (u` y)) = ((t` x) .ih y)) <-> (t:H~-->H~ /\ u:H~-->H~ /\ A.y e. H~ A.x e. H~ (y .ih (t` x)) = ((u` y) .ih x)))
342, 33bitr 173 . . . 4 |- ((u:H~-->H~ /\ t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (u` y)) = ((t` x) .ih y)) <-> (t:H~-->H~ /\ u:H~-->H~ /\ A.y e. H~ A.x e. H~ (y .ih (t` x)) = ((u` y) .ih x)))
3534opabbii 2666 . . 3 |- {<.t, u>. | (u:H~-->H~ /\ t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (u` y)) = ((