# Metamath Proof Explorer

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
|- ( ( A e. CC /\ T e. dom adjh ) -> ( adjh ` ( A .op T ) ) = ( ( * ` A ) .op ( adjh ` T ) ) )

### Proof

Step Hyp Ref Expression
|-  ( 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 )
|-  ( ( 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 )
|-  ( ( 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 ) ) )
|-  ( ( ( 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 ffvelrnda
|-  ( ( 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 )
|-  ( ( T e. dom adjh /\ y e. ~H ) -> ( ( adjh ` T ) ` y ) e. ~H )
|-  ( ( ( 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 ) ) )
|-  ( ( ( 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 ) ) )