Metamath Proof Explorer

Theorem lnopcoi

Description: The composition of two linear operators is linear. (Contributed by NM, 8-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses lnopco.1 
|- S e. LinOp
lnopco.2 
|- T e. LinOp
Assertion lnopcoi 
|- ( S o. T ) e. LinOp

Proof

Step Hyp Ref Expression
1 lnopco.1 
 |-  S e. LinOp
2 lnopco.2 
 |-  T e. LinOp
3 1 lnopfi 
 |-  S : ~H --> ~H
4 2 lnopfi 
 |-  T : ~H --> ~H
5 3 4 hocofi 
 |-  ( S o. T ) : ~H --> ~H
6 2 lnopli 
 |-  ( ( x e. CC /\ y e. ~H /\ z e. ~H ) -> ( T ` ( ( x .h y ) +h z ) ) = ( ( x .h ( T ` y ) ) +h ( T ` z ) ) )
7 6 fveq2d 
 |-  ( ( x e. CC /\ y e. ~H /\ z e. ~H ) -> ( S ` ( T ` ( ( x .h y ) +h z ) ) ) = ( S ` ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) )
8 id 
 |-  ( x e. CC -> x e. CC )
9 4 ffvelrni 
 |-  ( y e. ~H -> ( T ` y ) e. ~H )
10 4 ffvelrni 
 |-  ( z e. ~H -> ( T ` z ) e. ~H )
11 1 lnopli 
 |-  ( ( x e. CC /\ ( T ` y ) e. ~H /\ ( T ` z ) e. ~H ) -> ( S ` ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) = ( ( x .h ( S ` ( T ` y ) ) ) +h ( S ` ( T ` z ) ) ) )
12 8 9 10 11 syl3an 
 |-  ( ( x e. CC /\ y e. ~H /\ z e. ~H ) -> ( S ` ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) = ( ( x .h ( S ` ( T ` y ) ) ) +h ( S ` ( T ` z ) ) ) )
13 7 12 eqtrd 
 |-  ( ( x e. CC /\ y e. ~H /\ z e. ~H ) -> ( S ` ( T ` ( ( x .h y ) +h z ) ) ) = ( ( x .h ( S ` ( T ` y ) ) ) +h ( S ` ( T ` z ) ) ) )
14 13 3expa 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( S ` ( T ` ( ( x .h y ) +h z ) ) ) = ( ( x .h ( S ` ( T ` y ) ) ) +h ( S ` ( T ` z ) ) ) )
15 hvmulcl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h y ) e. ~H )
16 hvaddcl 
 |-  ( ( ( x .h y ) e. ~H /\ z e. ~H ) -> ( ( x .h y ) +h z ) e. ~H )
17 15 16 sylan 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( x .h y ) +h z ) e. ~H )
18 3 4 hocoi 
 |-  ( ( ( x .h y ) +h z ) e. ~H -> ( ( S o. T ) ` ( ( x .h y ) +h z ) ) = ( S ` ( T ` ( ( x .h y ) +h z ) ) ) )
19 17 18 syl 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( S o. T ) ` ( ( x .h y ) +h z ) ) = ( S ` ( T ` ( ( x .h y ) +h z ) ) ) )
20 3 4 hocoi 
 |-  ( y e. ~H -> ( ( S o. T ) ` y ) = ( S ` ( T ` y ) ) )
21 20 oveq2d 
 |-  ( y e. ~H -> ( x .h ( ( S o. T ) ` y ) ) = ( x .h ( S ` ( T ` y ) ) ) )
22 21 adantl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h ( ( S o. T ) ` y ) ) = ( x .h ( S ` ( T ` y ) ) ) )
23 3 4 hocoi 
 |-  ( z e. ~H -> ( ( S o. T ) ` z ) = ( S ` ( T ` z ) ) )
24 22 23 oveqan12d 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( x .h ( ( S o. T ) ` y ) ) +h ( ( S o. T ) ` z ) ) = ( ( x .h ( S ` ( T ` y ) ) ) +h ( S ` ( T ` z ) ) ) )
25 14 19 24 3eqtr4d 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( S o. T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( S o. T ) ` y ) ) +h ( ( S o. T ) ` z ) ) )
26 25 3impa 
 |-  ( ( x e. CC /\ y e. ~H /\ z e. ~H ) -> ( ( S o. T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( S o. T ) ` y ) ) +h ( ( S o. T ) ` z ) ) )
27 26 rgen3 
 |-  A. x e. CC A. y e. ~H A. z e. ~H ( ( S o. T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( S o. T ) ` y ) ) +h ( ( S o. T ) ` z ) )
28 ellnop 
 |-  ( ( S o. T ) e. LinOp <-> ( ( S o. T ) : ~H --> ~H /\ A. x e. CC A. y e. ~H A. z e. ~H ( ( S o. T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( S o. T ) ` y ) ) +h ( ( S o. T ) ` z ) ) ) )
29 5 27 28 mpbir2an 
 |-  ( S o. T ) e. LinOp