Metamath Proof Explorer

Theorem hmoplin

Description: A Hermitian operator is linear. (Contributed by NM, 24-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion hmoplin 
|- ( T e. HrmOp -> T e. LinOp )

Proof

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