Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  adjmul Unicode version

 Description: The adjoint of the scalar product of an operator. Theorem 3.11(ii) of [Beran] p. 106. (Contributed by NM, 21-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmadjop 22468 . . 3
2 homulcl 22339 . . 3
31, 2sylan2 460 . 2
4 cjcl 11590 . . 3
5 dmadjrn 22475 . . . 4
6 dmadjop 22468 . . . 4
75, 6syl 15 . . 3
8 homulcl 22339 . . 3
94, 7, 8syl2an 463 . 2
10 adj2 22514 . . . . . . . 8
11103expb 1152 . . . . . . 7
1211adantll 694 . . . . . 6
1312oveq2d 5874 . . . . 5
14 ffvelrn 5663 . . . . . . . . . 10
151, 14sylan 457 . . . . . . . . 9
16 ax-his3 21663 . . . . . . . . 9
1715, 16syl3an2 1216 . . . . . . . 8
18173exp 1150 . . . . . . 7
1918exp3a 425 . . . . . 6
2019imp43 578 . . . . 5
21 simpll 730 . . . . . 6
22 simprl 732 . . . . . 6
23 adjcl 22512 . . . . . . 7
2423ad2ant2l 726 . . . . . 6
25 his52 21666 . . . . . 6
2621, 22, 24, 25syl3anc 1182 . . . . 5
2713, 20, 263eqtr4d 2325 . . . 4
28 homval 22321 . . . . . . . 8
291, 28syl3an2 1216 . . . . . . 7
30293expa 1151 . . . . . 6
3130adantrr 697 . . . . 5
3231oveq1d 5873 . . . 4
33 id 19 . . . . . . . 8
34 homval 22321 . . . . . . . 8
354, 7, 33, 34syl3an 1224 . . . . . . 7
36353expa 1151 . . . . . 6
3736adantrl 696 . . . . 5
3837oveq2d 5874 . . . 4
3927, 32, 383eqtr4d 2325 . . 3
4039ralrimivva 2635 . 2