# 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 ffvelrn
` |-  ( ( 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 ffvelrn
` |-  ( ( 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 )`