# 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}\in \mathrm{LinOp}$
lnopco.2 ${⊢}{T}\in \mathrm{LinOp}$
Assertion lnopcoi ${⊢}{S}\circ {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 hocofi ${⊢}\left({S}\circ {T}\right):ℋ⟶ℋ$
6 2 lnopli ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\wedge {z}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)$
7 6 fveq2d ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\wedge {z}\in ℋ\right)\to {S}\left({T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)\right)={S}\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$
8 id ${⊢}{x}\in ℂ\to {x}\in ℂ$
9 4 ffvelrni ${⊢}{y}\in ℋ\to {T}\left({y}\right)\in ℋ$
10 4 ffvelrni ${⊢}{z}\in ℋ\to {T}\left({z}\right)\in ℋ$
11 1 lnopli ${⊢}\left({x}\in ℂ\wedge {T}\left({y}\right)\in ℋ\wedge {T}\left({z}\right)\in ℋ\right)\to {S}\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)=\left({x}{\cdot }_{ℎ}{S}\left({T}\left({y}\right)\right)\right){+}_{ℎ}{S}\left({T}\left({z}\right)\right)$
12 8 9 10 11 syl3an ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\wedge {z}\in ℋ\right)\to {S}\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)=\left({x}{\cdot }_{ℎ}{S}\left({T}\left({y}\right)\right)\right){+}_{ℎ}{S}\left({T}\left({z}\right)\right)$
13 7 12 eqtrd ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\wedge {z}\in ℋ\right)\to {S}\left({T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)\right)=\left({x}{\cdot }_{ℎ}{S}\left({T}\left({y}\right)\right)\right){+}_{ℎ}{S}\left({T}\left({z}\right)\right)$
14 13 3expa ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to {S}\left({T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)\right)=\left({x}{\cdot }_{ℎ}{S}\left({T}\left({y}\right)\right)\right){+}_{ℎ}{S}\left({T}\left({z}\right)\right)$
15 hvmulcl ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{ℎ}{y}\in ℋ$
16 hvaddcl ${⊢}\left({x}{\cdot }_{ℎ}{y}\in ℋ\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ$
17 15 16 sylan ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ$
18 3 4 hocoi ${⊢}\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ\to \left({S}\circ {T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={S}\left({T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)\right)$
19 17 18 syl ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({S}\circ {T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={S}\left({T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)\right)$
20 3 4 hocoi ${⊢}{y}\in ℋ\to \left({S}\circ {T}\right)\left({y}\right)={S}\left({T}\left({y}\right)\right)$
21 20 oveq2d ${⊢}{y}\in ℋ\to {x}{\cdot }_{ℎ}\left({S}\circ {T}\right)\left({y}\right)={x}{\cdot }_{ℎ}{S}\left({T}\left({y}\right)\right)$
22 21 adantl ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{ℎ}\left({S}\circ {T}\right)\left({y}\right)={x}{\cdot }_{ℎ}{S}\left({T}\left({y}\right)\right)$
23 3 4 hocoi ${⊢}{z}\in ℋ\to \left({S}\circ {T}\right)\left({z}\right)={S}\left({T}\left({z}\right)\right)$
24 22 23 oveqan12d ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}\left({S}\circ {T}\right)\left({y}\right)\right){+}_{ℎ}\left({S}\circ {T}\right)\left({z}\right)=\left({x}{\cdot }_{ℎ}{S}\left({T}\left({y}\right)\right)\right){+}_{ℎ}{S}\left({T}\left({z}\right)\right)$
25 14 19 24 3eqtr4d ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({S}\circ {T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({S}\circ {T}\right)\left({y}\right)\right){+}_{ℎ}\left({S}\circ {T}\right)\left({z}\right)$
26 25 3impa ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\wedge {z}\in ℋ\right)\to \left({S}\circ {T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({S}\circ {T}\right)\left({y}\right)\right){+}_{ℎ}\left({S}\circ {T}\right)\left({z}\right)$
27 26 rgen3 ${⊢}\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({S}\circ {T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({S}\circ {T}\right)\left({y}\right)\right){+}_{ℎ}\left({S}\circ {T}\right)\left({z}\right)$
28 ellnop ${⊢}{S}\circ {T}\in \mathrm{LinOp}↔\left(\left({S}\circ {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}\circ {T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({S}\circ {T}\right)\left({y}\right)\right){+}_{ℎ}\left({S}\circ {T}\right)\left({z}\right)\right)$
29 5 27 28 mpbir2an ${⊢}{S}\circ {T}\in \mathrm{LinOp}$