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	⊢ 𝑇 ∈ LinOp
Assertion	rnelshi	⊢ ran 𝑇 ∈ Sℋ

Proof

Step	Hyp	Ref	Expression
1		rnelsh.1	⊢ 𝑇 ∈ LinOp
2		imadmrn	⊢ ( 𝑇 “ dom 𝑇 ) = ran 𝑇
3	1	lnopfi	⊢ 𝑇 : ℋ ⟶ ℋ
4	3	fdmi	⊢ dom 𝑇 = ℋ
5		helsh	⊢ ℋ ∈ Sℋ
6	4 5	eqeltri	⊢ dom 𝑇 ∈ Sℋ
7	1 6	imaelshi	⊢ ( 𝑇 “ dom 𝑇 ) ∈ Sℋ
8	2 7	eqeltrri	⊢ ran 𝑇 ∈ Sℋ