# 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 )`
` |-  ( ( ( 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 ffvelrni
` |-  ( 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 ffvelrni
` |-  ( 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 ) ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 )`