This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 ) |
| 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 ) |