Metamath Proof Explorer

Theorem lnopmi

Description: The scalar product of a linear operator is a linear operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnopm.1 
|- T e. LinOp
Assertion lnopmi 
|- ( A e. CC -> ( A .op T ) e. LinOp )

Proof

Step Hyp Ref Expression
1 lnopm.1 
 |-  T e. LinOp
2 1 lnopfi 
 |-  T : ~H --> ~H
3 homulcl 
 |-  ( ( A e. CC /\ T : ~H --> ~H ) -> ( A .op T ) : ~H --> ~H )
4 2 3 mpan2 
 |-  ( A e. CC -> ( A .op T ) : ~H --> ~H )
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 homval 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ ( ( x .h y ) +h z ) e. ~H ) -> ( ( A .op T ) ` ( ( x .h y ) +h z ) ) = ( A .h ( T ` ( ( x .h y ) +h z ) ) ) )
9 2 8 mp3an2 
 |-  ( ( A e. CC /\ ( ( x .h y ) +h z ) e. ~H ) -> ( ( A .op T ) ` ( ( x .h y ) +h z ) ) = ( A .h ( T ` ( ( x .h y ) +h z ) ) ) )
10 7 9 sylan2 
 |-  ( ( A e. CC /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( A .op T ) ` ( ( x .h y ) +h z ) ) = ( A .h ( T ` ( ( x .h y ) +h z ) ) ) )
11 id 
 |-  ( A e. CC -> A e. CC )
12 2 ffvelcdmi 
 |-  ( y e. ~H -> ( T ` y ) e. ~H )
13 hvmulcl 
 |-  ( ( x e. CC /\ ( T ` y ) e. ~H ) -> ( x .h ( T ` y ) ) e. ~H )
14 12 13 sylan2 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h ( T ` y ) ) e. ~H )
15 2 ffvelcdmi 
 |-  ( z e. ~H -> ( T ` z ) e. ~H )
16 ax-hvdistr1 
 |-  ( ( A e. CC /\ ( x .h ( T ` y ) ) e. ~H /\ ( T ` z ) e. ~H ) -> ( A .h ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) = ( ( A .h ( x .h ( T ` y ) ) ) +h ( A .h ( T ` z ) ) ) )
17 11 14 15 16 syl3an 
 |-  ( ( A e. CC /\ ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( A .h ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) = ( ( A .h ( x .h ( T ` y ) ) ) +h ( A .h ( T ` z ) ) ) )
18 17 3expb 
 |-  ( ( A e. CC /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( A .h ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) = ( ( A .h ( x .h ( T ` y ) ) ) +h ( A .h ( T ` z ) ) ) )
19 1 lnopli 
 |-  ( ( x e. CC /\ y e. ~H /\ z e. ~H ) -> ( T ` ( ( x .h y ) +h z ) ) = ( ( x .h ( T ` y ) ) +h ( T ` z ) ) )
20 19 3expa 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( T ` ( ( x .h y ) +h z ) ) = ( ( x .h ( T ` y ) ) +h ( T ` z ) ) )
21 20 oveq2d 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( A .h ( T ` ( ( x .h y ) +h z ) ) ) = ( A .h ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) )
22 21 adantl 
 |-  ( ( A e. CC /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( A .h ( T ` ( ( x .h y ) +h z ) ) ) = ( A .h ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) )
23 homval 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ y e. ~H ) -> ( ( A .op T ) ` y ) = ( A .h ( T ` y ) ) )
24 2 23 mp3an2 
 |-  ( ( A e. CC /\ y e. ~H ) -> ( ( A .op T ) ` y ) = ( A .h ( T ` y ) ) )
25 24 adantrl 
 |-  ( ( A e. CC /\ ( x e. CC /\ y e. ~H ) ) -> ( ( A .op T ) ` y ) = ( A .h ( T ` y ) ) )
26 25 oveq2d 
 |-  ( ( A e. CC /\ ( x e. CC /\ y e. ~H ) ) -> ( x .h ( ( A .op T ) ` y ) ) = ( x .h ( A .h ( T ` y ) ) ) )
27 hvmulcom 
 |-  ( ( A e. CC /\ x e. CC /\ ( T ` y ) e. ~H ) -> ( A .h ( x .h ( T ` y ) ) ) = ( x .h ( A .h ( T ` y ) ) ) )
28 12 27 syl3an3 
 |-  ( ( A e. CC /\ x e. CC /\ y e. ~H ) -> ( A .h ( x .h ( T ` y ) ) ) = ( x .h ( A .h ( T ` y ) ) ) )
29 28 3expb 
 |-  ( ( A e. CC /\ ( x e. CC /\ y e. ~H ) ) -> ( A .h ( x .h ( T ` y ) ) ) = ( x .h ( A .h ( T ` y ) ) ) )
30 26 29 eqtr4d 
 |-  ( ( A e. CC /\ ( x e. CC /\ y e. ~H ) ) -> ( x .h ( ( A .op T ) ` y ) ) = ( A .h ( x .h ( T ` y ) ) ) )
31 homval 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ z e. ~H ) -> ( ( A .op T ) ` z ) = ( A .h ( T ` z ) ) )
32 2 31 mp3an2 
 |-  ( ( A e. CC /\ z e. ~H ) -> ( ( A .op T ) ` z ) = ( A .h ( T ` z ) ) )
33 30 32 oveqan12d 
 |-  ( ( ( A e. CC /\ ( x e. CC /\ y e. ~H ) ) /\ ( A e. CC /\ z e. ~H ) ) -> ( ( x .h ( ( A .op T ) ` y ) ) +h ( ( A .op T ) ` z ) ) = ( ( A .h ( x .h ( T ` y ) ) ) +h ( A .h ( T ` z ) ) ) )
34 33 anandis 
 |-  ( ( A e. CC /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( x .h ( ( A .op T ) ` y ) ) +h ( ( A .op T ) ` z ) ) = ( ( A .h ( x .h ( T ` y ) ) ) +h ( A .h ( T ` z ) ) ) )
35 18 22 34 3eqtr4rd 
 |-  ( ( A e. CC /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( x .h ( ( A .op T ) ` y ) ) +h ( ( A .op T ) ` z ) ) = ( A .h ( T ` ( ( x .h y ) +h z ) ) ) )
36 10 35 eqtr4d 
 |-  ( ( A e. CC /\ ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) ) -> ( ( A .op T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( A .op T ) ` y ) ) +h ( ( A .op T ) ` z ) ) )
37 36 exp32 
 |-  ( A e. CC -> ( ( x e. CC /\ y e. ~H ) -> ( z e. ~H -> ( ( A .op T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( A .op T ) ` y ) ) +h ( ( A .op T ) ` z ) ) ) ) )
38 37 ralrimdv 
 |-  ( A e. CC -> ( ( x e. CC /\ y e. ~H ) -> A. z e. ~H ( ( A .op T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( A .op T ) ` y ) ) +h ( ( A .op T ) ` z ) ) ) )
39 38 ralrimivv 
 |-  ( A e. CC -> A. x e. CC A. y e. ~H A. z e. ~H ( ( A .op T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( A .op T ) ` y ) ) +h ( ( A .op T ) ` z ) ) )
40 ellnop 
 |-  ( ( A .op T ) e. LinOp <-> ( ( A .op T ) : ~H --> ~H /\ A. x e. CC A. y e. ~H A. z e. ~H ( ( A .op T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( A .op T ) ` y ) ) +h ( ( A .op T ) ` z ) ) ) )
41 4 39 40 sylanbrc 
 |-  ( A e. CC -> ( A .op T ) e. LinOp )