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:\mathscr{H}⟶\mathscr{H}$$
4	2	lnopfi	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
5	3 4	hocofi	$$⊢\left(S\circ T\right):\mathscr{H}⟶\mathscr{H}$$
6	2	lnopli	$$⊢\left(x\in ℂ\wedge y\in \mathscr{H}\wedge z\in \mathscr{H}\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 \mathscr{H}\wedge z\in \mathscr{H}\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	ffvelcdmi	$$⊢y\in \mathscr{H}\to T\left(y\right)\in \mathscr{H}$$
10	4	ffvelcdmi	$$⊢z\in \mathscr{H}\to T\left(z\right)\in \mathscr{H}$$
11	1	lnopli	$$⊢\left(x\in ℂ\wedge T\left(y\right)\in \mathscr{H}\wedge T\left(z\right)\in \mathscr{H}\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 \mathscr{H}\wedge z\in \mathscr{H}\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 \mathscr{H}\wedge z\in \mathscr{H}\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 \mathscr{H}\right)\wedge z\in \mathscr{H}\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 \mathscr{H}\right)\to x{\cdot }_{ℎ}y\in \mathscr{H}$$
16		hvaddcl	$$⊢\left(x{\cdot }_{ℎ}y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\to \left(x{\cdot }_{ℎ}y\right){+}_{ℎ}z\in \mathscr{H}$$
17	15 16	sylan	$$⊢\left(\left(x\in ℂ\wedge y\in \mathscr{H}\right)\wedge z\in \mathscr{H}\right)\to \left(x{\cdot }_{ℎ}y\right){+}_{ℎ}z\in \mathscr{H}$$
18	3 4	hocoi	$$⊢\left(x{\cdot }_{ℎ}y\right){+}_{ℎ}z\in \mathscr{H}\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 \mathscr{H}\right)\wedge z\in \mathscr{H}\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 \mathscr{H}\to \left(S\circ T\right)\left(y\right)=S\left(T\left(y\right)\right)$$
21	20	oveq2d	$$⊢y\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\right)\wedge z\in \mathscr{H}\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 \mathscr{H}\right)\wedge z\in \mathscr{H}\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 \mathscr{H}\wedge z\in \mathscr{H}\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 ℂ\forall y\in \mathscr{H}\forall z\in \mathscr{H}\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}\leftrightarrow \left(\left(S\circ T\right):\mathscr{H}⟶\mathscr{H}\wedge \forall x\in ℂ\forall y\in \mathscr{H}\forall z\in \mathscr{H}\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}$$