This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hmopm

Description: The scalar product of a Hermitian operator with a real is Hermitian. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopm 
|- ( ( A e. RR /\ T e. HrmOp ) -> ( A .op T ) e. HrmOp )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
3 homulcl 
 |-  ( ( A e. CC /\ T : ~H --> ~H ) -> ( A .op T ) : ~H --> ~H )
4 1 2 3 syl2an 
 |-  ( ( A e. RR /\ T e. HrmOp ) -> ( A .op T ) : ~H --> ~H )
5 cjre 
 |-  ( A e. RR -> ( * ` A ) = A )
6 hmop 
 |-  ( ( T e. HrmOp /\ x e. ~H /\ y e. ~H ) -> ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) )
7 6 3expb 
 |-  ( ( T e. HrmOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) )
8 5 7 oveqan12d 
 |-  ( ( A e. RR /\ ( T e. HrmOp /\ ( x e. ~H /\ y e. ~H ) ) ) -> ( ( * ` A ) x. ( x .ih ( T ` y ) ) ) = ( A x. ( ( T ` x ) .ih y ) ) )
9 8 anassrs 
 |-  ( ( ( A e. RR /\ T e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( * ` A ) x. ( x .ih ( T ` y ) ) ) = ( A x. ( ( T ` x ) .ih y ) ) )
10 1 2 anim12i 
 |-  ( ( A e. RR /\ T e. HrmOp ) -> ( A e. CC /\ T : ~H --> ~H ) )
11 homval 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ y e. ~H ) -> ( ( A .op T ) ` y ) = ( A .h ( T ` y ) ) )
12 11 3expa 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ y e. ~H ) -> ( ( A .op T ) ` y ) = ( A .h ( T ` y ) ) )
13 12 adantrl 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( A .op T ) ` y ) = ( A .h ( T ` y ) ) )
14 13 oveq2d 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( A .op T ) ` y ) ) = ( x .ih ( A .h ( T ` y ) ) ) )
15 simpll 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> A e. CC )
16 simprl 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> x e. ~H )
17 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ y e. ~H ) -> ( T ` y ) e. ~H )
18 17 ad2ant2l 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( T ` y ) e. ~H )
19 his5 
 |-  ( ( A e. CC /\ x e. ~H /\ ( T ` y ) e. ~H ) -> ( x .ih ( A .h ( T ` y ) ) ) = ( ( * ` A ) x. ( x .ih ( T ` y ) ) ) )
20 15 16 18 19 syl3anc 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( A .h ( T ` y ) ) ) = ( ( * ` A ) x. ( x .ih ( T ` y ) ) ) )
21 14 20 eqtrd 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( A .op T ) ` y ) ) = ( ( * ` A ) x. ( x .ih ( T ` y ) ) ) )
22 10 21 sylan 
 |-  ( ( ( A e. RR /\ T e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( A .op T ) ` y ) ) = ( ( * ` A ) x. ( x .ih ( T ` y ) ) ) )
23 homval 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
24 23 3expa 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
25 24 adantrr 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
26 25 oveq1d 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( A .op T ) ` x ) .ih y ) = ( ( A .h ( T ` x ) ) .ih y ) )
27 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
28 27 ad2ant2lr 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( T ` x ) e. ~H )
29 simprr 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> y e. ~H )
30 ax-his3 
 |-  ( ( A e. CC /\ ( T ` x ) e. ~H /\ y e. ~H ) -> ( ( A .h ( T ` x ) ) .ih y ) = ( A x. ( ( T ` x ) .ih y ) ) )
31 15 28 29 30 syl3anc 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( A .h ( T ` x ) ) .ih y ) = ( A x. ( ( T ` x ) .ih y ) ) )
32 26 31 eqtrd 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( A .op T ) ` x ) .ih y ) = ( A x. ( ( T ` x ) .ih y ) ) )
33 10 32 sylan 
 |-  ( ( ( A e. RR /\ T e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( A .op T ) ` x ) .ih y ) = ( A x. ( ( T ` x ) .ih y ) ) )
34 9 22 33 3eqtr4d 
 |-  ( ( ( A e. RR /\ T e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( A .op T ) ` y ) ) = ( ( ( A .op T ) ` x ) .ih y ) )
35 34 ralrimivva 
 |-  ( ( A e. RR /\ T e. HrmOp ) -> A. x e. ~H A. y e. ~H ( x .ih ( ( A .op T ) ` y ) ) = ( ( ( A .op T ) ` x ) .ih y ) )
36 elhmop 
 |-  ( ( A .op T ) e. HrmOp <-> ( ( A .op T ) : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( ( A .op T ) ` y ) ) = ( ( ( A .op T ) ` x ) .ih y ) ) )
37 4 35 36 sylanbrc 
 |-  ( ( A e. RR /\ T e. HrmOp ) -> ( A .op T ) e. HrmOp )