Metamath Proof Explorer


Theorem dfadj2

Description: Alternate definition of the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion dfadj2 adj h = t u | t : u : x y x ih t y = u x ih y

Proof

Step Hyp Ref Expression
1 df-adjh adj h = t u | t : u : x y t x ih y = x ih u y
2 adjsym t : u : x y x ih t y = u x ih y x y x ih u y = t x ih y
3 eqcom t x ih y = x ih u y x ih u y = t x ih y
4 3 2ralbii x y t x ih y = x ih u y x y x ih u y = t x ih y
5 2 4 syl6rbbr t : u : x y t x ih y = x ih u y x y x ih t y = u x ih y
6 5 pm5.32i t : u : x y t x ih y = x ih u y t : u : x y x ih t y = u x ih y
7 df-3an t : u : x y t x ih y = x ih u y t : u : x y t x ih y = x ih u y
8 df-3an t : u : x y x ih t y = u x ih y t : u : x y x ih t y = u x ih y
9 6 7 8 3bitr4i t : u : x y t x ih y = x ih u y t : u : x y x ih t y = u x ih y
10 9 opabbii t u | t : u : x y t x ih y = x ih u y = t u | t : u : x y x ih t y = u x ih y
11 1 10 eqtri adj h = t u | t : u : x y x ih t y = u x ih y