Theorem rnelshi

Description: The range of a linear operator is a subspace. (Contributed by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	rnelsh.1	$$⊢T\in \mathrm{LinOp}$$
Assertion	rnelshi	$$⊢\mathrm{ran}T\in {\mathbf{S}}_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		rnelsh.1	$$⊢T\in \mathrm{LinOp}$$
2		imadmrn	$$⊢T\left[\mathrm{dom}T\right]=\mathrm{ran}T$$
3	1	lnopfi	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
4	3	fdmi	$$⊢\mathrm{dom}T=\mathscr{H}$$
5		helsh	$$⊢\mathscr{H}\in {\mathbf{S}}_{\mathscr{H}}$$
6	4 5	eqeltri	$$⊢\mathrm{dom}T\in {\mathbf{S}}_{\mathscr{H}}$$
7	1 6	imaelshi	$$⊢T\left[\mathrm{dom}T\right]\in {\mathbf{S}}_{\mathscr{H}}$$
8	2 7	eqeltrri	$$⊢\mathrm{ran}T\in {\mathbf{S}}_{\mathscr{H}}$$