# Metamath Proof Explorer

Description: The adjoint of a composition of bounded linear operators. Theorem 3.11(viii) of Beran p. 106. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nmoptri.1
`|- S e. BndLinOp`
nmoptri.2
`|- T e. BndLinOp`
`|- ( adjh ` ( S o. T ) ) = ( ( adjh ` T ) o. ( adjh ` S ) )`

### Proof

Step Hyp Ref Expression
1 nmoptri.1
` |-  S e. BndLinOp`
2 nmoptri.2
` |-  T e. BndLinOp`
` |-  ( T e. BndLinOp -> ( adjh ` T ) e. BndLinOp )`
4 bdopf
` |-  ( ( adjh ` T ) e. BndLinOp -> ( adjh ` T ) : ~H --> ~H )`
5 2 3 4 mp2b
` |-  ( adjh ` T ) : ~H --> ~H`
` |-  ( S e. BndLinOp -> ( adjh ` S ) e. BndLinOp )`
7 bdopf
` |-  ( ( adjh ` S ) e. BndLinOp -> ( adjh ` S ) : ~H --> ~H )`
8 1 6 7 mp2b
` |-  ( adjh ` S ) : ~H --> ~H`
9 5 8 hocoi
` |-  ( y e. ~H -> ( ( ( adjh ` T ) o. ( adjh ` S ) ) ` y ) = ( ( adjh ` T ) ` ( ( adjh ` S ) ` y ) ) )`
10 9 oveq2d
` |-  ( y e. ~H -> ( x .ih ( ( ( adjh ` T ) o. ( adjh ` S ) ) ` y ) ) = ( x .ih ( ( adjh ` T ) ` ( ( adjh ` S ) ` y ) ) ) )`
` |-  ( ( x e. ~H /\ y e. ~H ) -> ( x .ih ( ( ( adjh ` T ) o. ( adjh ` S ) ) ` y ) ) = ( x .ih ( ( adjh ` T ) ` ( ( adjh ` S ) ` y ) ) ) )`
12 bdopf
` |-  ( S e. BndLinOp -> S : ~H --> ~H )`
13 1 12 ax-mp
` |-  S : ~H --> ~H`
14 bdopf
` |-  ( T e. BndLinOp -> T : ~H --> ~H )`
15 2 14 ax-mp
` |-  T : ~H --> ~H`
16 13 15 hocoi
` |-  ( x e. ~H -> ( ( S o. T ) ` x ) = ( S ` ( T ` x ) ) )`
17 16 oveq1d
` |-  ( x e. ~H -> ( ( ( S o. T ) ` x ) .ih y ) = ( ( S ` ( T ` x ) ) .ih y ) )`
` |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( S o. T ) ` x ) .ih y ) = ( ( S ` ( T ` x ) ) .ih y ) )`
19 15 ffvelrni
` |-  ( x e. ~H -> ( T ` x ) e. ~H )`
` |-  ( S e. BndLinOp -> S e. dom adjh )`
21 1 20 ax-mp
` |-  S e. dom adjh`
` |-  ( ( S e. dom adjh /\ ( T ` x ) e. ~H /\ y e. ~H ) -> ( ( S ` ( T ` x ) ) .ih y ) = ( ( T ` x ) .ih ( ( adjh ` S ) ` y ) ) )`
23 21 22 mp3an1
` |-  ( ( ( T ` x ) e. ~H /\ y e. ~H ) -> ( ( S ` ( T ` x ) ) .ih y ) = ( ( T ` x ) .ih ( ( adjh ` S ) ` y ) ) )`
24 19 23 sylan
` |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( S ` ( T ` x ) ) .ih y ) = ( ( T ` x ) .ih ( ( adjh ` S ) ` y ) ) )`
25 8 ffvelrni
` |-  ( y e. ~H -> ( ( adjh ` S ) ` y ) e. ~H )`
` |-  ( T e. BndLinOp -> T e. dom adjh )`
27 2 26 ax-mp
` |-  T e. dom adjh`
` |-  ( ( T e. dom adjh /\ x e. ~H /\ ( ( adjh ` S ) ` y ) e. ~H ) -> ( ( T ` x ) .ih ( ( adjh ` S ) ` y ) ) = ( x .ih ( ( adjh ` T ) ` ( ( adjh ` S ) ` y ) ) ) )`
29 27 28 mp3an1
` |-  ( ( x e. ~H /\ ( ( adjh ` S ) ` y ) e. ~H ) -> ( ( T ` x ) .ih ( ( adjh ` S ) ` y ) ) = ( x .ih ( ( adjh ` T ) ` ( ( adjh ` S ) ` y ) ) ) )`
30 25 29 sylan2
` |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih ( ( adjh ` S ) ` y ) ) = ( x .ih ( ( adjh ` T ) ` ( ( adjh ` S ) ` y ) ) ) )`
31 18 24 30 3eqtrd
` |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( S o. T ) ` x ) .ih y ) = ( x .ih ( ( adjh ` T ) ` ( ( adjh ` S ) ` y ) ) ) )`
32 1 2 bdopcoi
` |-  ( S o. T ) e. BndLinOp`
` |-  ( ( S o. T ) e. BndLinOp -> ( S o. T ) e. dom adjh )`
34 32 33 ax-mp
` |-  ( S o. T ) e. dom adjh`
` |-  ( ( ( S o. T ) e. dom adjh /\ x e. ~H /\ y e. ~H ) -> ( ( ( S o. T ) ` x ) .ih y ) = ( x .ih ( ( adjh ` ( S o. T ) ) ` y ) ) )`
36 34 35 mp3an1
` |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( S o. T ) ` x ) .ih y ) = ( x .ih ( ( adjh ` ( S o. T ) ) ` y ) ) )`
37 11 31 36 3eqtr2rd
` |-  ( ( x e. ~H /\ y e. ~H ) -> ( x .ih ( ( adjh ` ( S o. T ) ) ` y ) ) = ( x .ih ( ( ( adjh ` T ) o. ( adjh ` S ) ) ` y ) ) )`
38 37 rgen2
` |-  A. x e. ~H A. y e. ~H ( x .ih ( ( adjh ` ( S o. T ) ) ` y ) ) = ( x .ih ( ( ( adjh ` T ) o. ( adjh ` S ) ) ` y ) )`
` |-  ( ( S o. T ) e. BndLinOp -> ( adjh ` ( S o. T ) ) e. BndLinOp )`
` |-  ( ( adjh ` ( S o. T ) ) e. BndLinOp -> ( adjh ` ( S o. T ) ) : ~H --> ~H )`
` |-  ( adjh ` ( S o. T ) ) : ~H --> ~H`
` |-  ( ( adjh ` T ) o. ( adjh ` S ) ) : ~H --> ~H`
` |-  ( ( ( adjh ` ( S o. T ) ) : ~H --> ~H /\ ( ( adjh ` T ) o. ( adjh ` S ) ) : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( ( adjh ` ( S o. T ) ) ` y ) ) = ( x .ih ( ( ( adjh ` T ) o. ( adjh ` S ) ) ` y ) ) <-> ( adjh ` ( S o. T ) ) = ( ( adjh ` T ) o. ( adjh ` S ) ) ) )`
` |-  ( A. x e. ~H A. y e. ~H ( x .ih ( ( adjh ` ( S o. T ) ) ` y ) ) = ( x .ih ( ( ( adjh ` T ) o. ( adjh ` S ) ) ` y ) ) <-> ( adjh ` ( S o. T ) ) = ( ( adjh ` T ) o. ( adjh ` S ) ) )`
` |-  ( adjh ` ( S o. T ) ) = ( ( adjh ` T ) o. ( adjh ` S ) )`