# Metamath Proof Explorer

## Theorem hmops

Description: The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion hmops
`|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T +op U ) e. HrmOp )`

### Proof

Step Hyp Ref Expression
1 hmopf
` |-  ( T e. HrmOp -> T : ~H --> ~H )`
2 hmopf
` |-  ( U e. HrmOp -> U : ~H --> ~H )`
` |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op U ) : ~H --> ~H )`
4 1 2 3 syl2an
` |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T +op U ) : ~H --> ~H )`
5 hmop
` |-  ( ( T e. HrmOp /\ x e. ~H /\ y e. ~H ) -> ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) )`
6 5 3expb
` |-  ( ( T e. HrmOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) )`
7 hmop
` |-  ( ( U e. HrmOp /\ x e. ~H /\ y e. ~H ) -> ( x .ih ( U ` y ) ) = ( ( U ` x ) .ih y ) )`
8 7 3expb
` |-  ( ( U e. HrmOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( U ` y ) ) = ( ( U ` x ) .ih y ) )`
9 6 8 oveqan12d
` |-  ( ( ( T e. HrmOp /\ ( x e. ~H /\ y e. ~H ) ) /\ ( U e. HrmOp /\ ( x e. ~H /\ y e. ~H ) ) ) -> ( ( x .ih ( T ` y ) ) + ( x .ih ( U ` y ) ) ) = ( ( ( T ` x ) .ih y ) + ( ( U ` x ) .ih y ) ) )`
10 9 anandirs
` |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( x .ih ( T ` y ) ) + ( x .ih ( U ` y ) ) ) = ( ( ( T ` x ) .ih y ) + ( ( U ` x ) .ih y ) ) )`
11 1 2 anim12i
` |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T : ~H --> ~H /\ U : ~H --> ~H ) )`
12 hosval
` |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H /\ y e. ~H ) -> ( ( T +op U ) ` y ) = ( ( T ` y ) +h ( U ` y ) ) )`
13 12 oveq2d
` |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H /\ y e. ~H ) -> ( x .ih ( ( T +op U ) ` y ) ) = ( x .ih ( ( T ` y ) +h ( U ` y ) ) ) )`
14 13 3expa
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ y e. ~H ) -> ( x .ih ( ( T +op U ) ` y ) ) = ( x .ih ( ( T ` y ) +h ( U ` y ) ) ) )`
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( T +op U ) ` y ) ) = ( x .ih ( ( T ` y ) +h ( U ` y ) ) ) )`
16 simprl
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> x e. ~H )`
17 ffvelrn
` |-  ( ( T : ~H --> ~H /\ y e. ~H ) -> ( T ` y ) e. ~H )`
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( T ` y ) e. ~H )`
19 ffvelrn
` |-  ( ( U : ~H --> ~H /\ y e. ~H ) -> ( U ` y ) e. ~H )`
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( U ` y ) e. ~H )`
21 his7
` |-  ( ( x e. ~H /\ ( T ` y ) e. ~H /\ ( U ` y ) e. ~H ) -> ( x .ih ( ( T ` y ) +h ( U ` y ) ) ) = ( ( x .ih ( T ` y ) ) + ( x .ih ( U ` y ) ) ) )`
22 16 18 20 21 syl3anc
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( T ` y ) +h ( U ` y ) ) ) = ( ( x .ih ( T ` y ) ) + ( x .ih ( U ` y ) ) ) )`
23 15 22 eqtrd
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( T +op U ) ` y ) ) = ( ( x .ih ( T ` y ) ) + ( x .ih ( U ` y ) ) ) )`
24 11 23 sylan
` |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( T +op U ) ` y ) ) = ( ( x .ih ( T ` y ) ) + ( x .ih ( U ` y ) ) ) )`
25 hosval
` |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H /\ x e. ~H ) -> ( ( T +op U ) ` x ) = ( ( T ` x ) +h ( U ` x ) ) )`
26 25 oveq1d
` |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H /\ x e. ~H ) -> ( ( ( T +op U ) ` x ) .ih y ) = ( ( ( T ` x ) +h ( U ` x ) ) .ih y ) )`
27 26 3expa
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( T +op U ) ` x ) .ih y ) = ( ( ( T ` x ) +h ( U ` x ) ) .ih y ) )`
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( T +op U ) ` x ) .ih y ) = ( ( ( T ` x ) +h ( U ` x ) ) .ih y ) )`
29 ffvelrn
` |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )`
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( T ` x ) e. ~H )`
31 ffvelrn
` |-  ( ( U : ~H --> ~H /\ x e. ~H ) -> ( U ` x ) e. ~H )`
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( U ` x ) e. ~H )`
33 simprr
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> y e. ~H )`
34 ax-his2
` |-  ( ( ( T ` x ) e. ~H /\ ( U ` x ) e. ~H /\ y e. ~H ) -> ( ( ( T ` x ) +h ( U ` x ) ) .ih y ) = ( ( ( T ` x ) .ih y ) + ( ( U ` x ) .ih y ) ) )`
35 30 32 33 34 syl3anc
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( T ` x ) +h ( U ` x ) ) .ih y ) = ( ( ( T ` x ) .ih y ) + ( ( U ` x ) .ih y ) ) )`
36 28 35 eqtrd
` |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( T +op U ) ` x ) .ih y ) = ( ( ( T ` x ) .ih y ) + ( ( U ` x ) .ih y ) ) )`
37 11 36 sylan
` |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( T +op U ) ` x ) .ih y ) = ( ( ( T ` x ) .ih y ) + ( ( U ` x ) .ih y ) ) )`
38 10 24 37 3eqtr4d
` |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( T +op U ) ` y ) ) = ( ( ( T +op U ) ` x ) .ih y ) )`
39 38 ralrimivva
` |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> A. x e. ~H A. y e. ~H ( x .ih ( ( T +op U ) ` y ) ) = ( ( ( T +op U ) ` x ) .ih y ) )`
40 elhmop
` |-  ( ( T +op U ) e. HrmOp <-> ( ( T +op U ) : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( ( T +op U ) ` y ) ) = ( ( ( T +op U ) ` x ) .ih y ) ) )`
41 4 39 40 sylanbrc
` |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T +op U ) e. HrmOp )`