Metamath Proof Explorer

Theorem lnophsi

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

Ref Expression
Hypotheses lnopco.1 
|- S e. LinOp
lnopco.2 
|- T e. LinOp
Assertion lnophsi 
|- ( S +op 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 hoaddcli 
 |-  ( S +op T ) : ~H --> ~H
6 hvmulcl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h y ) e. ~H )
7 1 lnopaddi 
 |-  ( ( ( x .h y ) e. ~H /\ z e. ~H ) -> ( S ` ( ( x .h y ) +h z ) ) = ( ( S ` ( x .h y ) ) +h ( S ` z ) ) )
8 2 lnopaddi 
 |-  ( ( ( x .h y ) e. ~H /\ z e. ~H ) -> ( T ` ( ( x .h y ) +h z ) ) = ( ( T ` ( x .h y ) ) +h ( T ` z ) ) )
9 7 8 oveq12d 
 |-  ( ( ( x .h y ) e. ~H /\ z e. ~H ) -> ( ( S ` ( ( x .h y ) +h z ) ) +h ( T ` ( ( x .h y ) +h z ) ) ) = ( ( ( S ` ( x .h y ) ) +h ( S ` z ) ) +h ( ( T ` ( x .h y ) ) +h ( T ` z ) ) ) )
10 6 9 sylan 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( S ` ( ( x .h y ) +h z ) ) +h ( T ` ( ( x .h y ) +h z ) ) ) = ( ( ( S ` ( x .h y ) ) +h ( S ` z ) ) +h ( ( T ` ( x .h y ) ) +h ( T ` z ) ) ) )
11 3 ffvelrni 
 |-  ( ( x .h y ) e. ~H -> ( S ` ( x .h y ) ) e. ~H )
12 6 11 syl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( S ` ( x .h y ) ) e. ~H )
13 3 ffvelrni 
 |-  ( z e. ~H -> ( S ` z ) e. ~H )
14 12 13 anim12i 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( S ` ( x .h y ) ) e. ~H /\ ( S ` z ) e. ~H ) )
15 4 ffvelrni 
 |-  ( ( x .h y ) e. ~H -> ( T ` ( x .h y ) ) e. ~H )
16 6 15 syl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( T ` ( x .h y ) ) e. ~H )
17 4 ffvelrni 
 |-  ( z e. ~H -> ( T ` z ) e. ~H )
18 16 17 anim12i 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( T ` ( x .h y ) ) e. ~H /\ ( T ` z ) e. ~H ) )
19 hvadd4 
 |-  ( ( ( ( S ` ( x .h y ) ) e. ~H /\ ( S ` z ) e. ~H ) /\ ( ( T ` ( x .h y ) ) e. ~H /\ ( T ` z ) e. ~H ) ) -> ( ( ( S ` ( x .h y ) ) +h ( S ` z ) ) +h ( ( T ` ( x .h y ) ) +h ( T ` z ) ) ) = ( ( ( S ` ( x .h y ) ) +h ( T ` ( x .h y ) ) ) +h ( ( S ` z ) +h ( T ` z ) ) ) )
20 14 18 19 syl2anc 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( ( S ` ( x .h y ) ) +h ( S ` z ) ) +h ( ( T ` ( x .h y ) ) +h ( T ` z ) ) ) = ( ( ( S ` ( x .h y ) ) +h ( T ` ( x .h y ) ) ) +h ( ( S ` z ) +h ( T ` z ) ) ) )
21 10 20 eqtrd 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( S ` ( ( x .h y ) +h z ) ) +h ( T ` ( ( x .h y ) +h z ) ) ) = ( ( ( S ` ( x .h y ) ) +h ( T ` ( x .h y ) ) ) +h ( ( S ` z ) +h ( T ` z ) ) ) )
22 hvaddcl 
 |-  ( ( ( x .h y ) e. ~H /\ z e. ~H ) -> ( ( x .h y ) +h z ) e. ~H )
23 6 22 sylan 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( x .h y ) +h z ) e. ~H )
24 hosval 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ ( ( x .h y ) +h z ) e. ~H ) -> ( ( S +op T ) ` ( ( x .h y ) +h z ) ) = ( ( S ` ( ( x .h y ) +h z ) ) +h ( T ` ( ( x .h y ) +h z ) ) ) )
25 3 4 24 mp3an12 
 |-  ( ( ( x .h y ) +h z ) e. ~H -> ( ( S +op T ) ` ( ( x .h y ) +h z ) ) = ( ( S ` ( ( x .h y ) +h z ) ) +h ( T ` ( ( x .h y ) +h z ) ) ) )
26 23 25 syl 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( S +op T ) ` ( ( x .h y ) +h z ) ) = ( ( S ` ( ( x .h y ) +h z ) ) +h ( T ` ( ( x .h y ) +h z ) ) ) )
27 3 ffvelrni 
 |-  ( y e. ~H -> ( S ` y ) e. ~H )
28 4 ffvelrni 
 |-  ( y e. ~H -> ( T ` y ) e. ~H )
29 27 28 jca 
 |-  ( y e. ~H -> ( ( S ` y ) e. ~H /\ ( T ` y ) e. ~H ) )
30 ax-hvdistr1 
 |-  ( ( x e. CC /\ ( S ` y ) e. ~H /\ ( T ` y ) e. ~H ) -> ( x .h ( ( S ` y ) +h ( T ` y ) ) ) = ( ( x .h ( S ` y ) ) +h ( x .h ( T ` y ) ) ) )
31 30 3expb 
 |-  ( ( x e. CC /\ ( ( S ` y ) e. ~H /\ ( T ` y ) e. ~H ) ) -> ( x .h ( ( S ` y ) +h ( T ` y ) ) ) = ( ( x .h ( S ` y ) ) +h ( x .h ( T ` y ) ) ) )
32 29 31 sylan2 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h ( ( S ` y ) +h ( T ` y ) ) ) = ( ( x .h ( S ` y ) ) +h ( x .h ( T ` y ) ) ) )
33 hosval 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ y e. ~H ) -> ( ( S +op T ) ` y ) = ( ( S ` y ) +h ( T ` y ) ) )
34 3 4 33 mp3an12 
 |-  ( y e. ~H -> ( ( S +op T ) ` y ) = ( ( S ` y ) +h ( T ` y ) ) )
35 34 oveq2d 
 |-  ( y e. ~H -> ( x .h ( ( S +op T ) ` y ) ) = ( x .h ( ( S ` y ) +h ( T ` y ) ) ) )
36 35 adantl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h ( ( S +op T ) ` y ) ) = ( x .h ( ( S ` y ) +h ( T ` y ) ) ) )
37 1 lnopmuli 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( S ` ( x .h y ) ) = ( x .h ( S ` y ) ) )
38 2 lnopmuli 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( T ` ( x .h y ) ) = ( x .h ( T ` y ) ) )
39 37 38 oveq12d 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( ( S ` ( x .h y ) ) +h ( T ` ( x .h y ) ) ) = ( ( x .h ( S ` y ) ) +h ( x .h ( T ` y ) ) ) )
40 32 36 39 3eqtr4d 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h ( ( S +op T ) ` y ) ) = ( ( S ` ( x .h y ) ) +h ( T ` ( x .h y ) ) ) )
41 hosval 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ z e. ~H ) -> ( ( S +op T ) ` z ) = ( ( S ` z ) +h ( T ` z ) ) )
42 3 4 41 mp3an12 
 |-  ( z e. ~H -> ( ( S +op T ) ` z ) = ( ( S ` z ) +h ( T ` z ) ) )
43 40 42 oveqan12d 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( x .h ( ( S +op T ) ` y ) ) +h ( ( S +op T ) ` z ) ) = ( ( ( S ` ( x .h y ) ) +h ( T ` ( x .h y ) ) ) +h ( ( S ` z ) +h ( T ` z ) ) ) )
44 21 26 43 3eqtr4d 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( S +op T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( S +op T ) ` y ) ) +h ( ( S +op T ) ` z ) ) )
45 44 ralrimiva 
 |-  ( ( x e. CC /\ y e. ~H ) -> A. z e. ~H ( ( S +op T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( S +op T ) ` y ) ) +h ( ( S +op T ) ` z ) ) )
46 45 rgen2 
 |-  A. x e. CC A. y e. ~H A. z e. ~H ( ( S +op T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( S +op T ) ` y ) ) +h ( ( S +op T ) ` z ) )
47 ellnop 
 |-  ( ( S +op T ) e. LinOp <-> ( ( S +op T ) : ~H --> ~H /\ A. x e. CC A. y e. ~H A. z e. ~H ( ( S +op T ) ` ( ( x .h y ) +h z ) ) = ( ( x .h ( ( S +op T ) ` y ) ) +h ( ( S +op T ) ` z ) ) ) )
48 5 46 47 mpbir2an 
 |-  ( S +op T ) e. LinOp