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 )
3 hoaddcl 
 |-  ( ( 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 ) ) ) )
15 14 adantrl 
 |-  ( ( ( 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 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ y e. ~H ) -> ( T ` y ) e. ~H )
18 17 ad2ant2rl 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( T ` y ) e. ~H )
19 ffvelcdm 
 |-  ( ( U : ~H --> ~H /\ y e. ~H ) -> ( U ` y ) e. ~H )
20 19 ad2ant2l 
 |-  ( ( ( 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 ) )
28 27 adantrr 
 |-  ( ( ( 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 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
30 29 ad2ant2r 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( T ` x ) e. ~H )
31 ffvelcdm 
 |-  ( ( U : ~H --> ~H /\ x e. ~H ) -> ( U ` x ) e. ~H )
32 31 ad2ant2lr 
 |-  ( ( ( 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 )