Metamath Proof Explorer

Theorem adjcoi

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
Assertion adjcoi 
|- ( 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
3 adjbdln 
 |-  ( 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
6 adjbdln 
 |-  ( 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 ) ) ) )
11 10 adantl 
 |-  ( ( 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 ) )
18 17 adantr 
 |-  ( ( 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 )
20 bdopadj 
 |-  ( S e. BndLinOp -> S e. dom adjh )
21 1 20 ax-mp 
 |-  S e. dom adjh
22 adj2 
 |-  ( ( 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 )
26 bdopadj 
 |-  ( T e. BndLinOp -> T e. dom adjh )
27 2 26 ax-mp 
 |-  T e. dom adjh
28 adj2 
 |-  ( ( 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
33 bdopadj 
 |-  ( ( S o. T ) e. BndLinOp -> ( S o. T ) e. dom adjh )
34 32 33 ax-mp 
 |-  ( S o. T ) e. dom adjh
35 adj2 
 |-  ( ( ( 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 ) )
39 adjbdln 
 |-  ( ( S o. T ) e. BndLinOp -> ( adjh ` ( S o. T ) ) e. BndLinOp )
40 bdopf 
 |-  ( ( adjh ` ( S o. T ) ) e. BndLinOp -> ( adjh ` ( S o. T ) ) : ~H --> ~H )
41 32 39 40 mp2b 
 |-  ( adjh ` ( S o. T ) ) : ~H --> ~H
42 5 8 hocofi 
 |-  ( ( adjh ` T ) o. ( adjh ` S ) ) : ~H --> ~H
43 hoeq2 
 |-  ( ( ( 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 ) ) ) )
44 41 42 43 mp2an 
 |-  ( 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 ) ) )
45 38 44 mpbi 
 |-  ( adjh ` ( S o. T ) ) = ( ( adjh ` T ) o. ( adjh ` S ) )