Metamath Proof Explorer

Theorem adjlnop

Description: The adjoint of an operator is linear. Proposition 1 of AkhiezerGlazman p. 80. (Contributed by NM, 17-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion adjlnop 
|- ( T e. dom adjh -> ( adjh ` T ) e. LinOp )

Proof

Step Hyp Ref Expression
1 dmadjrn 
 |-  ( T e. dom adjh -> ( adjh ` T ) e. dom adjh )
2 dmadjop 
 |-  ( ( adjh ` T ) e. dom adjh -> ( adjh ` T ) : ~H --> ~H )
3 1 2 syl 
 |-  ( T e. dom adjh -> ( adjh ` T ) : ~H --> ~H )
4 simp2 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> w e. ~H )
5 adjcl 
 |-  ( ( T e. dom adjh /\ y e. ~H ) -> ( ( adjh ` T ) ` y ) e. ~H )
6 hvmulcl 
 |-  ( ( x e. CC /\ ( ( adjh ` T ) ` y ) e. ~H ) -> ( x .h ( ( adjh ` T ) ` y ) ) e. ~H )
7 5 6 sylan2 
 |-  ( ( x e. CC /\ ( T e. dom adjh /\ y e. ~H ) ) -> ( x .h ( ( adjh ` T ) ` y ) ) e. ~H )
8 7 an12s 
 |-  ( ( T e. dom adjh /\ ( x e. CC /\ y e. ~H ) ) -> ( x .h ( ( adjh ` T ) ` y ) ) e. ~H )
9 8 adantrr 
 |-  ( ( T e. dom adjh /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( x .h ( ( adjh ` T ) ` y ) ) e. ~H )
10 9 3adant2 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( x .h ( ( adjh ` T ) ` y ) ) e. ~H )
11 adjcl 
 |-  ( ( T e. dom adjh /\ z e. ~H ) -> ( ( adjh ` T ) ` z ) e. ~H )
12 11 adantrl 
 |-  ( ( T e. dom adjh /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( adjh ` T ) ` z ) e. ~H )
13 12 3adant2 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( adjh ` T ) ` z ) e. ~H )
14 his7 
 |-  ( ( w e. ~H /\ ( x .h ( ( adjh ` T ) ` y ) ) e. ~H /\ ( ( adjh ` T ) ` z ) e. ~H ) -> ( w .ih ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) = ( ( w .ih ( x .h ( ( adjh ` T ) ` y ) ) ) + ( w .ih ( ( adjh ` T ) ` z ) ) ) )
15 4 10 13 14 syl3anc 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( w .ih ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) = ( ( w .ih ( x .h ( ( adjh ` T ) ` y ) ) ) + ( w .ih ( ( adjh ` T ) ` z ) ) ) )
16 adj2 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ y e. ~H ) -> ( ( T ` w ) .ih y ) = ( w .ih ( ( adjh ` T ) ` y ) ) )
17 16 3adant3l 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> ( ( T ` w ) .ih y ) = ( w .ih ( ( adjh ` T ) ` y ) ) )
18 17 oveq2d 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> ( ( * ` x ) x. ( ( T ` w ) .ih y ) ) = ( ( * ` x ) x. ( w .ih ( ( adjh ` T ) ` y ) ) ) )
19 simp3l 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> x e. CC )
20 dmadjop 
 |-  ( T e. dom adjh -> T : ~H --> ~H )
21 20 ffvelcdmda 
 |-  ( ( T e. dom adjh /\ w e. ~H ) -> ( T ` w ) e. ~H )
22 21 3adant3 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> ( T ` w ) e. ~H )
23 simp3r 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> y e. ~H )
24 his5 
 |-  ( ( x e. CC /\ ( T ` w ) e. ~H /\ y e. ~H ) -> ( ( T ` w ) .ih ( x .h y ) ) = ( ( * ` x ) x. ( ( T ` w ) .ih y ) ) )
25 19 22 23 24 syl3anc 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> ( ( T ` w ) .ih ( x .h y ) ) = ( ( * ` x ) x. ( ( T ` w ) .ih y ) ) )
26 simp2 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> w e. ~H )
27 5 adantrl 
 |-  ( ( T e. dom adjh /\ ( x e. CC /\ y e. ~H ) ) -> ( ( adjh ` T ) ` y ) e. ~H )
28 27 3adant2 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> ( ( adjh ` T ) ` y ) e. ~H )
29 his5 
 |-  ( ( x e. CC /\ w e. ~H /\ ( ( adjh ` T ) ` y ) e. ~H ) -> ( w .ih ( x .h ( ( adjh ` T ) ` y ) ) ) = ( ( * ` x ) x. ( w .ih ( ( adjh ` T ) ` y ) ) ) )
30 19 26 28 29 syl3anc 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> ( w .ih ( x .h ( ( adjh ` T ) ` y ) ) ) = ( ( * ` x ) x. ( w .ih ( ( adjh ` T ) ` y ) ) ) )
31 18 25 30 3eqtr4d 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> ( ( T ` w ) .ih ( x .h y ) ) = ( w .ih ( x .h ( ( adjh ` T ) ` y ) ) ) )
32 31 3adant3r 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( T ` w ) .ih ( x .h y ) ) = ( w .ih ( x .h ( ( adjh ` T ) ` y ) ) ) )
33 adj2 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ z e. ~H ) -> ( ( T ` w ) .ih z ) = ( w .ih ( ( adjh ` T ) ` z ) ) )
34 33 3adant3l 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( T ` w ) .ih z ) = ( w .ih ( ( adjh ` T ) ` z ) ) )
35 32 34 oveq12d 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( ( T ` w ) .ih ( x .h y ) ) + ( ( T ` w ) .ih z ) ) = ( ( w .ih ( x .h ( ( adjh ` T ) ` y ) ) ) + ( w .ih ( ( adjh ` T ) ` z ) ) ) )
36 21 3adant3 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( T ` w ) e. ~H )
37 hvmulcl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h y ) e. ~H )
38 37 adantr 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( x .h y ) e. ~H )
39 38 3ad2ant3 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( x .h y ) e. ~H )
40 simp3r 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> z e. ~H )
41 his7 
 |-  ( ( ( T ` w ) e. ~H /\ ( x .h y ) e. ~H /\ z e. ~H ) -> ( ( T ` w ) .ih ( ( x .h y ) +h z ) ) = ( ( ( T ` w ) .ih ( x .h y ) ) + ( ( T ` w ) .ih z ) ) )
42 36 39 40 41 syl3anc 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( T ` w ) .ih ( ( x .h y ) +h z ) ) = ( ( ( T ` w ) .ih ( x .h y ) ) + ( ( T ` w ) .ih z ) ) )
43 hvaddcl 
 |-  ( ( ( x .h y ) e. ~H /\ z e. ~H ) -> ( ( x .h y ) +h z ) e. ~H )
44 37 43 sylan 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( x .h y ) +h z ) e. ~H )
45 adj2 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x .h y ) +h z ) e. ~H ) -> ( ( T ` w ) .ih ( ( x .h y ) +h z ) ) = ( w .ih ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) ) )
46 44 45 syl3an3 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( T ` w ) .ih ( ( x .h y ) +h z ) ) = ( w .ih ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) ) )
47 42 46 eqtr3d 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( ( T ` w ) .ih ( x .h y ) ) + ( ( T ` w ) .ih z ) ) = ( w .ih ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) ) )
48 15 35 47 3eqtr2rd 
 |-  ( ( T e. dom adjh /\ w e. ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( w .ih ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) ) = ( w .ih ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) )
49 48 3com23 
 |-  ( ( T e. dom adjh /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) /\ w e. ~H ) -> ( w .ih ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) ) = ( w .ih ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) )
50 49 3expa 
 |-  ( ( ( T e. dom adjh /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) /\ w e. ~H ) -> ( w .ih ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) ) = ( w .ih ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) )
51 50 ralrimiva 
 |-  ( ( T e. dom adjh /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> A. w e. ~H ( w .ih ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) ) = ( w .ih ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) )
52 adjcl 
 |-  ( ( T e. dom adjh /\ ( ( x .h y ) +h z ) e. ~H ) -> ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) e. ~H )
53 44 52 sylan2 
 |-  ( ( T e. dom adjh /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) e. ~H )
54 hvaddcl 
 |-  ( ( ( x .h ( ( adjh ` T ) ` y ) ) e. ~H /\ ( ( adjh ` T ) ` z ) e. ~H ) -> ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) e. ~H )
55 8 11 54 syl2an 
 |-  ( ( ( T e. dom adjh /\ ( x e. CC /\ y e. ~H ) ) /\ ( T e. dom adjh /\ z e. ~H ) ) -> ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) e. ~H )
56 55 anandis 
 |-  ( ( T e. dom adjh /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) e. ~H )
57 hial2eq2 
 |-  ( ( ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) e. ~H /\ ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) e. ~H ) -> ( A. w e. ~H ( w .ih ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) ) = ( w .ih ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) <-> ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) )
58 53 56 57 syl2anc 
 |-  ( ( T e. dom adjh /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( A. w e. ~H ( w .ih ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) ) = ( w .ih ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) <-> ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) )
59 51 58 mpbid 
 |-  ( ( T e. dom adjh /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) )
60 59 exp32 
 |-  ( T e. dom adjh -> ( ( x e. CC /\ y e. ~H ) -> ( z e. ~H -> ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) ) )
61 60 ralrimdv 
 |-  ( T e. dom adjh -> ( ( x e. CC /\ y e. ~H ) -> A. z e. ~H ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) )
62 61 ralrimivv 
 |-  ( T e. dom adjh -> A. x e. CC A. y e. ~H A. z e. ~H ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) )
63 ellnop 
 |-  ( ( adjh ` T ) e. LinOp <-> ( ( adjh ` T ) : ~H --> ~H /\ A. x e. CC A. y e. ~H A. z e. ~H ( ( adjh ` T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( adjh ` T ) ` y ) ) +h ( ( adjh ` T ) ` z ) ) ) )
64 3 62 63 sylanbrc 
 |-  ( T e. dom adjh -> ( adjh ` T ) e. LinOp )