Metamath Proof Explorer


Theorem adj2

Description: Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adj2 TdomadjhABTAihB=AihadjhTB

Proof

Step Hyp Ref Expression
1 adj1 TdomadjhBABihTA=adjhTBihA
2 simp2 TdomadjhBAB
3 dmadjop TdomadjhT:
4 3 ffvelrnda TdomadjhATA
5 4 3adant2 TdomadjhBATA
6 ax-his1 BTABihTA=TAihB
7 2 5 6 syl2anc TdomadjhBABihTA=TAihB
8 adjcl TdomadjhBadjhTB
9 8 3adant3 TdomadjhBAadjhTB
10 simp3 TdomadjhBAA
11 ax-his1 adjhTBAadjhTBihA=AihadjhTB
12 9 10 11 syl2anc TdomadjhBAadjhTBihA=AihadjhTB
13 1 7 12 3eqtr3d TdomadjhBATAihB=AihadjhTB
14 hicl TABTAihB
15 5 2 14 syl2anc TdomadjhBATAihB
16 hicl AadjhTBAihadjhTB
17 10 9 16 syl2anc TdomadjhBAAihadjhTB
18 cj11 TAihBAihadjhTBTAihB=AihadjhTBTAihB=AihadjhTB
19 15 17 18 syl2anc TdomadjhBATAihB=AihadjhTBTAihB=AihadjhTB
20 13 19 mpbid TdomadjhBATAihB=AihadjhTB
21 20 3com23 TdomadjhABTAihB=AihadjhTB