# 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}\in \mathrm{LinOp}$
lnopco.2 ${⊢}{T}\in \mathrm{LinOp}$
Assertion lnophsi ${⊢}{S}{+}_{\mathrm{op}}{T}\in \mathrm{LinOp}$

### Proof

Step Hyp Ref Expression
1 lnopco.1 ${⊢}{S}\in \mathrm{LinOp}$
2 lnopco.2 ${⊢}{T}\in \mathrm{LinOp}$
3 1 lnopfi ${⊢}{S}:ℋ⟶ℋ$
4 2 lnopfi ${⊢}{T}:ℋ⟶ℋ$
5 3 4 hoaddcli ${⊢}\left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
6 hvmulcl ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{ℎ}{y}\in ℋ$
7 1 lnopaddi ${⊢}\left({x}{\cdot }_{ℎ}{y}\in ℋ\wedge {z}\in ℋ\right)\to {S}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={S}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{S}\left({z}\right)$
8 2 lnopaddi ${⊢}\left({x}{\cdot }_{ℎ}{y}\in ℋ\wedge {z}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={T}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{T}\left({z}\right)$
9 7 8 oveq12d ${⊢}\left({x}{\cdot }_{ℎ}{y}\in ℋ\wedge {z}\in ℋ\right)\to {S}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){+}_{ℎ}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({S}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{S}\left({z}\right)\right){+}_{ℎ}\left({T}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{T}\left({z}\right)\right)$
10 6 9 sylan ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to {S}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){+}_{ℎ}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({S}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{S}\left({z}\right)\right){+}_{ℎ}\left({T}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{T}\left({z}\right)\right)$
11 3 ffvelrni ${⊢}{x}{\cdot }_{ℎ}{y}\in ℋ\to {S}\left({x}{\cdot }_{ℎ}{y}\right)\in ℋ$
12 6 11 syl ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {S}\left({x}{\cdot }_{ℎ}{y}\right)\in ℋ$
13 3 ffvelrni ${⊢}{z}\in ℋ\to {S}\left({z}\right)\in ℋ$
14 12 13 anim12i ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({S}\left({x}{\cdot }_{ℎ}{y}\right)\in ℋ\wedge {S}\left({z}\right)\in ℋ\right)$
15 4 ffvelrni ${⊢}{x}{\cdot }_{ℎ}{y}\in ℋ\to {T}\left({x}{\cdot }_{ℎ}{y}\right)\in ℋ$
16 6 15 syl ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {T}\left({x}{\cdot }_{ℎ}{y}\right)\in ℋ$
17 4 ffvelrni ${⊢}{z}\in ℋ\to {T}\left({z}\right)\in ℋ$
18 16 17 anim12i ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({T}\left({x}{\cdot }_{ℎ}{y}\right)\in ℋ\wedge {T}\left({z}\right)\in ℋ\right)$
19 hvadd4 ${⊢}\left(\left({S}\left({x}{\cdot }_{ℎ}{y}\right)\in ℋ\wedge {S}\left({z}\right)\in ℋ\right)\wedge \left({T}\left({x}{\cdot }_{ℎ}{y}\right)\in ℋ\wedge {T}\left({z}\right)\in ℋ\right)\right)\to \left({S}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{S}\left({z}\right)\right){+}_{ℎ}\left({T}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{T}\left({z}\right)\right)=\left({S}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{T}\left({x}{\cdot }_{ℎ}{y}\right)\right){+}_{ℎ}\left({S}\left({z}\right){+}_{ℎ}{T}\left({z}\right)\right)$
20 14 18 19 syl2anc ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({S}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{S}\left({z}\right)\right){+}_{ℎ}\left({T}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{T}\left({z}\right)\right)=\left({S}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{T}\left({x}{\cdot }_{ℎ}{y}\right)\right){+}_{ℎ}\left({S}\left({z}\right){+}_{ℎ}{T}\left({z}\right)\right)$
21 10 20 eqtrd ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to {S}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){+}_{ℎ}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({S}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{T}\left({x}{\cdot }_{ℎ}{y}\right)\right){+}_{ℎ}\left({S}\left({z}\right){+}_{ℎ}{T}\left({z}\right)\right)$
22 hvaddcl ${⊢}\left({x}{\cdot }_{ℎ}{y}\in ℋ\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ$
23 6 22 sylan ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ$
24 hosval ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={S}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){+}_{ℎ}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)$
25 3 4 24 mp3an12 ${⊢}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ\to \left({S}{+}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={S}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){+}_{ℎ}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)$
26 23 25 syl ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={S}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){+}_{ℎ}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)$
27 3 ffvelrni ${⊢}{y}\in ℋ\to {S}\left({y}\right)\in ℋ$
28 4 ffvelrni ${⊢}{y}\in ℋ\to {T}\left({y}\right)\in ℋ$
29 27 28 jca ${⊢}{y}\in ℋ\to \left({S}\left({y}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)$
30 ax-hvdistr1 ${⊢}\left({x}\in ℂ\wedge {S}\left({y}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)\to {x}{\cdot }_{ℎ}\left({S}\left({y}\right){+}_{ℎ}{T}\left({y}\right)\right)=\left({x}{\cdot }_{ℎ}{S}\left({y}\right)\right){+}_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)$
31 30 3expb ${⊢}\left({x}\in ℂ\wedge \left({S}\left({y}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)\right)\to {x}{\cdot }_{ℎ}\left({S}\left({y}\right){+}_{ℎ}{T}\left({y}\right)\right)=\left({x}{\cdot }_{ℎ}{S}\left({y}\right)\right){+}_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)$
32 29 31 sylan2 ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{ℎ}\left({S}\left({y}\right){+}_{ℎ}{T}\left({y}\right)\right)=\left({x}{\cdot }_{ℎ}{S}\left({y}\right)\right){+}_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)$
33 hosval ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({y}\right)={S}\left({y}\right){+}_{ℎ}{T}\left({y}\right)$
34 3 4 33 mp3an12 ${⊢}{y}\in ℋ\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({y}\right)={S}\left({y}\right){+}_{ℎ}{T}\left({y}\right)$
35 34 oveq2d ${⊢}{y}\in ℋ\to {x}{\cdot }_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({y}\right)={x}{\cdot }_{ℎ}\left({S}\left({y}\right){+}_{ℎ}{T}\left({y}\right)\right)$
36 35 adantl ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({y}\right)={x}{\cdot }_{ℎ}\left({S}\left({y}\right){+}_{ℎ}{T}\left({y}\right)\right)$
37 1 lnopmuli ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {S}\left({x}{\cdot }_{ℎ}{y}\right)={x}{\cdot }_{ℎ}{S}\left({y}\right)$
38 2 lnopmuli ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {T}\left({x}{\cdot }_{ℎ}{y}\right)={x}{\cdot }_{ℎ}{T}\left({y}\right)$
39 37 38 oveq12d ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {S}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{T}\left({x}{\cdot }_{ℎ}{y}\right)=\left({x}{\cdot }_{ℎ}{S}\left({y}\right)\right){+}_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)$
40 32 36 39 3eqtr4d ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({y}\right)={S}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{T}\left({x}{\cdot }_{ℎ}{y}\right)$
41 hosval ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {z}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({z}\right)={S}\left({z}\right){+}_{ℎ}{T}\left({z}\right)$
42 3 4 41 mp3an12 ${⊢}{z}\in ℋ\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({z}\right)={S}\left({z}\right){+}_{ℎ}{T}\left({z}\right)$
43 40 42 oveqan12d ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({z}\right)=\left({S}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{T}\left({x}{\cdot }_{ℎ}{y}\right)\right){+}_{ℎ}\left({S}\left({z}\right){+}_{ℎ}{T}\left({z}\right)\right)$
44 21 26 43 3eqtr4d ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({z}\right)$
45 44 ralrimiva ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({S}{+}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({z}\right)$
46 45 rgen2 ${⊢}\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({S}{+}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({z}\right)$
47 ellnop ${⊢}{S}{+}_{\mathrm{op}}{T}\in \mathrm{LinOp}↔\left(\left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({S}{+}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({z}\right)\right)$
48 5 46 47 mpbir2an ${⊢}{S}{+}_{\mathrm{op}}{T}\in \mathrm{LinOp}$