HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem cnvadj 9811
Description: The adjoint function equals its converse.
Assertion
Ref Expression
cnvadj |- `'adjh = adjh
Proof of Theorem cnvadj
StepHypRef Expression
1 cnvopab 3451 . . 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 784 . . . . 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 8944 . . . . . . . . . . . . . . . . . 18 |- (((u` y) e. H~ /\ x e. H~) -> ((u` y) .ih x) = (*` (x .ih (u` y))))
4 ffvelrn 3820 . . . . . . . . . . . . . . . . . 18 |- ((u:H~-->H~ /\ y e. H~) -> (u` y) e. H~)
53, 4sylan 450 . . . . . . . . . . . . . . . . 17 |- (((u:H~-->H~ /\ y e. H~) /\ x e. H~) -> ((u` y) .ih x) = (*` (x .ih (u` y))))
65adantrl 396 . . . . . . . . . . . . . . . 16 |- (((u:H~-->H~ /\ y e. H~) /\ (t:H~-->H~ /\ x e. H~)) -> ((u` y) .ih x) = (*` (x .ih (u` y))))
7 ax-his1 8944 . . . . . . . . . . . . . . . . . 18 |- ((y e. H~ /\ (t` x) e. H~) -> (y .ih (t` x)) = (*` ((t` x) .ih y)))
8 ffvelrn 3820 . . . . . . . . . . . . . . . . . 18 |- ((t:H~-->H~ /\ x e. H~) -> (t` x) e. H~)
97, 8sylan2 453 . . . . . . . . . . . . . . . . 17 |- ((y e. H~ /\ (t:H~-->H~ /\ x e. H~)) -> (y .ih (t` x)) = (*` ((t` x) .ih y)))
109adantll 394 . . . . . . . . . . . . . . . 16 |- (((u:H~-->H~ /\ y e. H~) /\ (t:H~-->H~ /\ x e. H~)) -> (y .ih (t` x)) = (*` ((t` x) .ih y)))
116, 10eqeq12d 1492 . . . . . . . . . . . . . . 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 438 . . . . . . . . . . . . . 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 6830 . . . . . . . . . . . . . . 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 8942 . . . . . . . . . . . . . . . . 17 |- ((x e. H~ /\ (u` y) e. H~) -> (x .ih (u` y)) e. CC)
1514, 4sylan2 453 . . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ (u:H~-->H~ /\ y e. H~)) -> (x .ih (u` y)) e. CC)
1615adantll 394 . . . . . . . . . . . . . . 15 |- (((t:H~-->H~ /\ x e. H~) /\ (u:H~-->H~ /\ y e. H~)) -> (x .ih (u` y)) e. CC)
17 hiclt 8942 . . . . . . . . . . . . . . . . 17 |- (((t` x) e. H~ /\ y e. H~) -> ((t` x) .ih y) e. CC)
1817, 8sylan 450 . . . . . . . . . . . . . . . 16 |- (((t:H~-->H~ /\ x e. H~) /\ y e. H~) -> ((t` x) .ih y) e. CC)
1918adantrl 396 . . . . . . . . . . . . . . 15 |- (((t:H~-->H~ /\ x e. H~) /\ (u:H~-->H~ /\ y e. H~)) -> ((t` x) .ih y) e. CC)
2013, 16, 19sylanc 473 . . . . . . . . . . . . . 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 531 . . . . . . . . . . . . 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 510 . . . . . . . . . . . 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 443 . . . . . . . . . . 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 1480 . . . . . . . . . . 11 |- (((u` y) .ih x) = (y .ih (t` x)) <-> (y .ih (t` x)) = ((u` y) .ih x))
2523, 24syl6bb 538 . . . . . . . . . 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 1662 . . . . . . . . 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 1662 . . . . . . . 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 1777 . . . . . . . 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 538 . . . . . . 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 647 . . . . . 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 779 . . . . . 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 779 . . . . . 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 2676 . . 3 |- {<.t, u>. | (u:H~-->H~ /\ t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (u` y)) = (