Metamath Proof Explorer

Theorem unoplin

Description: A unitary operator is linear. Theorem in AkhiezerGlazman p. 72. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion unoplin 
|- ( T e. UniOp -> T e. LinOp )

Proof

Step Hyp Ref Expression
1 unopf1o 
 |-  ( T e. UniOp -> T : ~H -1-1-onto-> ~H )
2 f1of 
 |-  ( T : ~H -1-1-onto-> ~H -> T : ~H --> ~H )
3 1 2 syl 
 |-  ( T e. UniOp -> T : ~H --> ~H )
4 simplll 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> T e. UniOp )
5 hvmulcl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h y ) e. ~H )
6 hvaddcl 
 |-  ( ( ( x .h y ) e. ~H /\ z e. ~H ) -> ( ( x .h y ) +h z ) e. ~H )
7 5 6 sylan 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( x .h y ) +h z ) e. ~H )
8 7 adantll 
 |-  ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) -> ( ( x .h y ) +h z ) e. ~H )
9 8 adantr 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> ( ( x .h y ) +h z ) e. ~H )
10 simpr 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> w e. ~H )
11 unopadj 
 |-  ( ( T e. UniOp /\ ( ( x .h y ) +h z ) e. ~H /\ w e. ~H ) -> ( ( T ` ( ( x .h y ) +h z ) ) .ih w ) = ( ( ( x .h y ) +h z ) .ih ( `' T ` w ) ) )
12 4 9 10 11 syl3anc 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> ( ( T ` ( ( x .h y ) +h z ) ) .ih w ) = ( ( ( x .h y ) +h z ) .ih ( `' T ` w ) ) )
13 simprl 
 |-  ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) -> x e. CC )
14 13 ad2antrr 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> x e. CC )
15 simprr 
 |-  ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) -> y e. ~H )
16 15 ad2antrr 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> y e. ~H )
17 simplr 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> z e. ~H )
18 cnvunop 
 |-  ( T e. UniOp -> `' T e. UniOp )
19 unopf1o 
 |-  ( `' T e. UniOp -> `' T : ~H -1-1-onto-> ~H )
20 f1of 
 |-  ( `' T : ~H -1-1-onto-> ~H -> `' T : ~H --> ~H )
21 18 19 20 3syl 
 |-  ( T e. UniOp -> `' T : ~H --> ~H )
22 21 ffvelcdmda 
 |-  ( ( T e. UniOp /\ w e. ~H ) -> ( `' T ` w ) e. ~H )
23 22 adantlr 
 |-  ( ( ( T e. UniOp /\ z e. ~H ) /\ w e. ~H ) -> ( `' T ` w ) e. ~H )
24 23 adantllr 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> ( `' T ` w ) e. ~H )
25 hiassdi 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ ( z e. ~H /\ ( `' T ` w ) e. ~H ) ) -> ( ( ( x .h y ) +h z ) .ih ( `' T ` w ) ) = ( ( x x. ( y .ih ( `' T ` w ) ) ) + ( z .ih ( `' T ` w ) ) ) )
26 14 16 17 24 25 syl22anc 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> ( ( ( x .h y ) +h z ) .ih ( `' T ` w ) ) = ( ( x x. ( y .ih ( `' T ` w ) ) ) + ( z .ih ( `' T ` w ) ) ) )
27 3 ffvelcdmda 
 |-  ( ( T e. UniOp /\ y e. ~H ) -> ( T ` y ) e. ~H )
28 27 adantrl 
 |-  ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) -> ( T ` y ) e. ~H )
29 28 ad2antrr 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> ( T ` y ) e. ~H )
30 3 ffvelcdmda 
 |-  ( ( T e. UniOp /\ z e. ~H ) -> ( T ` z ) e. ~H )
31 30 adantr 
 |-  ( ( ( T e. UniOp /\ z e. ~H ) /\ w e. ~H ) -> ( T ` z ) e. ~H )
32 31 adantllr 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> ( T ` z ) e. ~H )
33 hiassdi 
 |-  ( ( ( x e. CC /\ ( T ` y ) e. ~H ) /\ ( ( T ` z ) e. ~H /\ w e. ~H ) ) -> ( ( ( x .h ( T ` y ) ) +h ( T ` z ) ) .ih w ) = ( ( x x. ( ( T ` y ) .ih w ) ) + ( ( T ` z ) .ih w ) ) )
34 14 29 32 10 33 syl22anc 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> ( ( ( x .h ( T ` y ) ) +h ( T ` z ) ) .ih w ) = ( ( x x. ( ( T ` y ) .ih w ) ) + ( ( T ` z ) .ih w ) ) )
35 unopadj 
 |-  ( ( T e. UniOp /\ y e. ~H /\ w e. ~H ) -> ( ( T ` y ) .ih w ) = ( y .ih ( `' T ` w ) ) )
36 35 3expa 
 |-  ( ( ( T e. UniOp /\ y e. ~H ) /\ w e. ~H ) -> ( ( T ` y ) .ih w ) = ( y .ih ( `' T ` w ) ) )
37 36 oveq2d 
 |-  ( ( ( T e. UniOp /\ y e. ~H ) /\ w e. ~H ) -> ( x x. ( ( T ` y ) .ih w ) ) = ( x x. ( y .ih ( `' T ` w ) ) ) )
38 37 adantlrl 
 |-  ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ w e. ~H ) -> ( x x. ( ( T ` y ) .ih w ) ) = ( x x. ( y .ih ( `' T ` w ) ) ) )
39 38 adantlr 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> ( x x. ( ( T ` y ) .ih w ) ) = ( x x. ( y .ih ( `' T ` w ) ) ) )
40 unopadj 
 |-  ( ( T e. UniOp /\ z e. ~H /\ w e. ~H ) -> ( ( T ` z ) .ih w ) = ( z .ih ( `' T ` w ) ) )
41 40 3expa 
 |-  ( ( ( T e. UniOp /\ z e. ~H ) /\ w e. ~H ) -> ( ( T ` z ) .ih w ) = ( z .ih ( `' T ` w ) ) )
42 41 adantllr 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> ( ( T ` z ) .ih w ) = ( z .ih ( `' T ` w ) ) )
43 39 42 oveq12d 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> ( ( x x. ( ( T ` y ) .ih w ) ) + ( ( T ` z ) .ih w ) ) = ( ( x x. ( y .ih ( `' T ` w ) ) ) + ( z .ih ( `' T ` w ) ) ) )
44 34 43 eqtr2d 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> ( ( x x. ( y .ih ( `' T ` w ) ) ) + ( z .ih ( `' T ` w ) ) ) = ( ( ( x .h ( T ` y ) ) +h ( T ` z ) ) .ih w ) )
45 12 26 44 3eqtrd 
 |-  ( ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) /\ w e. ~H ) -> ( ( T ` ( ( x .h y ) +h z ) ) .ih w ) = ( ( ( x .h ( T ` y ) ) +h ( T ` z ) ) .ih w ) )
46 45 ralrimiva 
 |-  ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) -> A. w e. ~H ( ( T ` ( ( x .h y ) +h z ) ) .ih w ) = ( ( ( x .h ( T ` y ) ) +h ( T ` z ) ) .ih w ) )
47 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ ( ( x .h y ) +h z ) e. ~H ) -> ( T ` ( ( x .h y ) +h z ) ) e. ~H )
48 7 47 sylan2 
 |-  ( ( T : ~H --> ~H /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( T ` ( ( x .h y ) +h z ) ) e. ~H )
49 48 anassrs 
 |-  ( ( ( T : ~H --> ~H /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) -> ( T ` ( ( x .h y ) +h z ) ) e. ~H )
50 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ y e. ~H ) -> ( T ` y ) e. ~H )
51 hvmulcl 
 |-  ( ( x e. CC /\ ( T ` y ) e. ~H ) -> ( x .h ( T ` y ) ) e. ~H )
52 50 51 sylan2 
 |-  ( ( x e. CC /\ ( T : ~H --> ~H /\ y e. ~H ) ) -> ( x .h ( T ` y ) ) e. ~H )
53 52 an12s 
 |-  ( ( T : ~H --> ~H /\ ( x e. CC /\ y e. ~H ) ) -> ( x .h ( T ` y ) ) e. ~H )
54 53 adantr 
 |-  ( ( ( T : ~H --> ~H /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) -> ( x .h ( T ` y ) ) e. ~H )
55 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ z e. ~H ) -> ( T ` z ) e. ~H )
56 55 adantlr 
 |-  ( ( ( T : ~H --> ~H /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) -> ( T ` z ) e. ~H )
57 hvaddcl 
 |-  ( ( ( x .h ( T ` y ) ) e. ~H /\ ( T ` z ) e. ~H ) -> ( ( x .h ( T ` y ) ) +h ( T ` z ) ) e. ~H )
58 54 56 57 syl2anc 
 |-  ( ( ( T : ~H --> ~H /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) -> ( ( x .h ( T ` y ) ) +h ( T ` z ) ) e. ~H )
59 hial2eq 
 |-  ( ( ( T ` ( ( x .h y ) +h z ) ) e. ~H /\ ( ( x .h ( T ` y ) ) +h ( T ` z ) ) e. ~H ) -> ( A. w e. ~H ( ( T ` ( ( x .h y ) +h z ) ) .ih w ) = ( ( ( x .h ( T ` y ) ) +h ( T ` z ) ) .ih w ) <-> ( T ` ( ( x .h y ) +h z ) ) = ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) )
60 49 58 59 syl2anc 
 |-  ( ( ( T : ~H --> ~H /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) -> ( A. w e. ~H ( ( T ` ( ( x .h y ) +h z ) ) .ih w ) = ( ( ( x .h ( T ` y ) ) +h ( T ` z ) ) .ih w ) <-> ( T ` ( ( x .h y ) +h z ) ) = ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) )
61 3 60 sylanl1 
 |-  ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) -> ( A. w e. ~H ( ( T ` ( ( x .h y ) +h z ) ) .ih w ) = ( ( ( x .h ( T ` y ) ) +h ( T ` z ) ) .ih w ) <-> ( T ` ( ( x .h y ) +h z ) ) = ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) )
62 46 61 mpbid 
 |-  ( ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) /\ z e. ~H ) -> ( T ` ( ( x .h y ) +h z ) ) = ( ( x .h ( T ` y ) ) +h ( T ` z ) ) )
63 62 ralrimiva 
 |-  ( ( T e. UniOp /\ ( x e. CC /\ y e. ~H ) ) -> A. z e. ~H ( T ` ( ( x .h y ) +h z ) ) = ( ( x .h ( T ` y ) ) +h ( T ` z ) ) )
64 63 ralrimivva 
 |-  ( T e. UniOp -> A. x e. CC A. y e. ~H A. z e. ~H ( T ` ( ( x .h y ) +h z ) ) = ( ( x .h ( T ` y ) ) +h ( T ` z ) ) )
65 ellnop 
 |-  ( T e. LinOp <-> ( T : ~H --> ~H /\ A. x e. CC A. y e. ~H A. z e. ~H ( T ` ( ( x .h y ) +h z ) ) = ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) )
66 3 64 65 sylanbrc 
 |-  ( T e. UniOp -> T e. LinOp )