Metamath Proof Explorer

Theorem adjmul

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.)

Ref Expression
Assertion adjmul 
|- ( ( A e. CC /\ T e. dom adjh ) -> ( adjh ` ( A .op T ) ) = ( ( * ` A ) .op ( adjh ` T ) ) )

Proof

Step Hyp Ref Expression
1 dmadjop 
 |-  ( T e. dom adjh -> T : ~H --> ~H )
2 homulcl 
 |-  ( ( A e. CC /\ T : ~H --> ~H ) -> ( A .op T ) : ~H --> ~H )
3 1 2 sylan2 
 |-  ( ( A e. CC /\ T e. dom adjh ) -> ( A .op T ) : ~H --> ~H )
4 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
5 dmadjrn 
 |-  ( T e. dom adjh -> ( adjh ` T ) e. dom adjh )
6 dmadjop 
 |-  ( ( adjh ` T ) e. dom adjh -> ( adjh ` T ) : ~H --> ~H )
7 5 6 syl 
 |-  ( T e. dom adjh -> ( adjh ` T ) : ~H --> ~H )
8 homulcl 
 |-  ( ( ( * ` A ) e. CC /\ ( adjh ` T ) : ~H --> ~H ) -> ( ( * ` A ) .op ( adjh ` T ) ) : ~H --> ~H )
9 4 7 8 syl2an 
 |-  ( ( A e. CC /\ T e. dom adjh ) -> ( ( * ` A ) .op ( adjh ` T ) ) : ~H --> ~H )
10 adj2 
 |-  ( ( T e. dom adjh /\ x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih y ) = ( x .ih ( ( adjh ` T ) ` y ) ) )
11 10 3expb 
 |-  ( ( T e. dom adjh /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) .ih y ) = ( x .ih ( ( adjh ` T ) ` y ) ) )
12 11 adantll 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) .ih y ) = ( x .ih ( ( adjh ` T ) ` y ) ) )
13 12 oveq2d 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( A x. ( ( T ` x ) .ih y ) ) = ( A x. ( x .ih ( ( adjh ` T ) ` y ) ) ) )
14 1 ffvelcdmda 
 |-  ( ( T e. dom adjh /\ x e. ~H ) -> ( T ` x ) e. ~H )
15 ax-his3 
 |-  ( ( A e. CC /\ ( T ` x ) e. ~H /\ y e. ~H ) -> ( ( A .h ( T ` x ) ) .ih y ) = ( A x. ( ( T ` x ) .ih y ) ) )
16 14 15 syl3an2 
 |-  ( ( A e. CC /\ ( T e. dom adjh /\ x e. ~H ) /\ y e. ~H ) -> ( ( A .h ( T ` x ) ) .ih y ) = ( A x. ( ( T ` x ) .ih y ) ) )
17 16 3exp 
 |-  ( A e. CC -> ( ( T e. dom adjh /\ x e. ~H ) -> ( y e. ~H -> ( ( A .h ( T ` x ) ) .ih y ) = ( A x. ( ( T ` x ) .ih y ) ) ) ) )
18 17 expd 
 |-  ( A e. CC -> ( T e. dom adjh -> ( x e. ~H -> ( y e. ~H -> ( ( A .h ( T ` x ) ) .ih y ) = ( A x. ( ( T ` x ) .ih y ) ) ) ) ) )
19 18 imp43 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( A .h ( T ` x ) ) .ih y ) = ( A x. ( ( T ` x ) .ih y ) ) )
20 simpll 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> A e. CC )
21 simprl 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> x e. ~H )
22 adjcl 
 |-  ( ( T e. dom adjh /\ y e. ~H ) -> ( ( adjh ` T ) ` y ) e. ~H )
23 22 ad2ant2l 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( adjh ` T ) ` y ) e. ~H )
24 his52 
 |-  ( ( A e. CC /\ x e. ~H /\ ( ( adjh ` T ) ` y ) e. ~H ) -> ( x .ih ( ( * ` A ) .h ( ( adjh ` T ) ` y ) ) ) = ( A x. ( x .ih ( ( adjh ` T ) ` y ) ) ) )
25 20 21 23 24 syl3anc 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( * ` A ) .h ( ( adjh ` T ) ` y ) ) ) = ( A x. ( x .ih ( ( adjh ` T ) ` y ) ) ) )
26 13 19 25 3eqtr4d 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( A .h ( T ` x ) ) .ih y ) = ( x .ih ( ( * ` A ) .h ( ( adjh ` T ) ` y ) ) ) )
27 homval 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
28 1 27 syl3an2 
 |-  ( ( A e. CC /\ T e. dom adjh /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
29 28 3expa 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
30 29 adantrr 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
31 30 oveq1d 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( A .op T ) ` x ) .ih y ) = ( ( A .h ( T ` x ) ) .ih y ) )
32 id 
 |-  ( y e. ~H -> y e. ~H )
33 homval 
 |-  ( ( ( * ` A ) e. CC /\ ( adjh ` T ) : ~H --> ~H /\ y e. ~H ) -> ( ( ( * ` A ) .op ( adjh ` T ) ) ` y ) = ( ( * ` A ) .h ( ( adjh ` T ) ` y ) ) )
34 4 7 32 33 syl3an 
 |-  ( ( A e. CC /\ T e. dom adjh /\ y e. ~H ) -> ( ( ( * ` A ) .op ( adjh ` T ) ) ` y ) = ( ( * ` A ) .h ( ( adjh ` T ) ` y ) ) )
35 34 3expa 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ y e. ~H ) -> ( ( ( * ` A ) .op ( adjh ` T ) ) ` y ) = ( ( * ` A ) .h ( ( adjh ` T ) ` y ) ) )
36 35 adantrl 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( * ` A ) .op ( adjh ` T ) ) ` y ) = ( ( * ` A ) .h ( ( adjh ` T ) ` y ) ) )
37 36 oveq2d 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( ( * ` A ) .op ( adjh ` T ) ) ` y ) ) = ( x .ih ( ( * ` A ) .h ( ( adjh ` T ) ` y ) ) ) )
38 26 31 37 3eqtr4d 
 |-  ( ( ( A e. CC /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( A .op T ) ` x ) .ih y ) = ( x .ih ( ( ( * ` A ) .op ( adjh ` T ) ) ` y ) ) )
39 38 ralrimivva 
 |-  ( ( A e. CC /\ T e. dom adjh ) -> A. x e. ~H A. y e. ~H ( ( ( A .op T ) ` x ) .ih y ) = ( x .ih ( ( ( * ` A ) .op ( adjh ` T ) ) ` y ) ) )
40 adjeq 
 |-  ( ( ( A .op T ) : ~H --> ~H /\ ( ( * ` A ) .op ( adjh ` T ) ) : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( ( A .op T ) ` x ) .ih y ) = ( x .ih ( ( ( * ` A ) .op ( adjh ` T ) ) ` y ) ) ) -> ( adjh ` ( A .op T ) ) = ( ( * ` A ) .op ( adjh ` T ) ) )
41 3 9 39 40 syl3anc 
 |-  ( ( A e. CC /\ T e. dom adjh ) -> ( adjh ` ( A .op T ) ) = ( ( * ` A ) .op ( adjh ` T ) ) )