Metamath Proof Explorer

Theorem hmopco

Description: The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopco 
|- ( ( T e. HrmOp /\ U e. HrmOp /\ ( T o. U ) = ( U o. T ) ) -> ( T o. 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 fco 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T o. U ) : ~H --> ~H )
4 1 2 3 syl2an 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T o. U ) : ~H --> ~H )
5 4 3adant3 
 |-  ( ( T e. HrmOp /\ U e. HrmOp /\ ( T o. U ) = ( U o. T ) ) -> ( T o. U ) : ~H --> ~H )
6 fvco3 
 |-  ( ( U : ~H --> ~H /\ y e. ~H ) -> ( ( T o. U ) ` y ) = ( T ` ( U ` y ) ) )
7 2 6 sylan 
 |-  ( ( U e. HrmOp /\ y e. ~H ) -> ( ( T o. U ) ` y ) = ( T ` ( U ` y ) ) )
8 7 oveq2d 
 |-  ( ( U e. HrmOp /\ y e. ~H ) -> ( x .ih ( ( T o. U ) ` y ) ) = ( x .ih ( T ` ( U ` y ) ) ) )
9 8 ad2ant2l 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( T o. U ) ` y ) ) = ( x .ih ( T ` ( U ` y ) ) ) )
10 simpll 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> T e. HrmOp )
11 simprl 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> x e. ~H )
12 2 ffvelcdmda 
 |-  ( ( U e. HrmOp /\ y e. ~H ) -> ( U ` y ) e. ~H )
13 12 ad2ant2l 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( U ` y ) e. ~H )
14 hmop 
 |-  ( ( T e. HrmOp /\ x e. ~H /\ ( U ` y ) e. ~H ) -> ( x .ih ( T ` ( U ` y ) ) ) = ( ( T ` x ) .ih ( U ` y ) ) )
15 10 11 13 14 syl3anc 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( T ` ( U ` y ) ) ) = ( ( T ` x ) .ih ( U ` y ) ) )
16 simplr 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> U e. HrmOp )
17 1 ffvelcdmda 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( T ` x ) e. ~H )
18 17 ad2ant2r 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( T ` x ) e. ~H )
19 simprr 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> y e. ~H )
20 hmop 
 |-  ( ( U e. HrmOp /\ ( T ` x ) e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih ( U ` y ) ) = ( ( U ` ( T ` x ) ) .ih y ) )
21 16 18 19 20 syl3anc 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) .ih ( U ` y ) ) = ( ( U ` ( T ` x ) ) .ih y ) )
22 9 15 21 3eqtrd 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( T o. U ) ` y ) ) = ( ( U ` ( T ` x ) ) .ih y ) )
23 fvco3 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( ( U o. T ) ` x ) = ( U ` ( T ` x ) ) )
24 1 23 sylan 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( U o. T ) ` x ) = ( U ` ( T ` x ) ) )
25 24 oveq1d 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( ( U o. T ) ` x ) .ih y ) = ( ( U ` ( T ` x ) ) .ih y ) )
26 25 ad2ant2r 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( U o. T ) ` x ) .ih y ) = ( ( U ` ( T ` x ) ) .ih y ) )
27 22 26 eqtr4d 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( T o. U ) ` y ) ) = ( ( ( U o. T ) ` x ) .ih y ) )
28 27 3adantl3 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp /\ ( T o. U ) = ( U o. T ) ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( T o. U ) ` y ) ) = ( ( ( U o. T ) ` x ) .ih y ) )
29 fveq1 
 |-  ( ( T o. U ) = ( U o. T ) -> ( ( T o. U ) ` x ) = ( ( U o. T ) ` x ) )
30 29 oveq1d 
 |-  ( ( T o. U ) = ( U o. T ) -> ( ( ( T o. U ) ` x ) .ih y ) = ( ( ( U o. T ) ` x ) .ih y ) )
31 30 3ad2ant3 
 |-  ( ( T e. HrmOp /\ U e. HrmOp /\ ( T o. U ) = ( U o. T ) ) -> ( ( ( T o. U ) ` x ) .ih y ) = ( ( ( U o. T ) ` x ) .ih y ) )
32 31 adantr 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp /\ ( T o. U ) = ( U o. T ) ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( T o. U ) ` x ) .ih y ) = ( ( ( U o. T ) ` x ) .ih y ) )
33 28 32 eqtr4d 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp /\ ( T o. U ) = ( U o. T ) ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( T o. U ) ` y ) ) = ( ( ( T o. U ) ` x ) .ih y ) )
34 33 ralrimivva 
 |-  ( ( T e. HrmOp /\ U e. HrmOp /\ ( T o. U ) = ( U o. T ) ) -> A. x e. ~H A. y e. ~H ( x .ih ( ( T o. U ) ` y ) ) = ( ( ( T o. U ) ` x ) .ih y ) )
35 elhmop 
 |-  ( ( T o. U ) e. HrmOp <-> ( ( T o. U ) : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( ( T o. U ) ` y ) ) = ( ( ( T o. U ) ` x ) .ih y ) ) )
36 5 34 35 sylanbrc 
 |-  ( ( T e. HrmOp /\ U e. HrmOp /\ ( T o. U ) = ( U o. T ) ) -> ( T o. U ) e. HrmOp )