This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 LinOp$
	Assertion	rnelshi	$⊢ ran T \in S_{ℋ}$

Step	Hyp	Ref	Expression
1		rnelsh.1	$⊢ T \in LinOp$
2		imadmrn	$⊢ T [dom T] = ran T$
3	1	lnopfi	$⊢ T : ℋ ⟶ ℋ$
4	3	fdmi	$⊢ dom T = ℋ$
5		helsh	$⊢ ℋ \in S_{ℋ}$
6	4 5	eqeltri	$⊢ dom T \in S_{ℋ}$
7	1 6	imaelshi	$⊢ T [dom T] \in S_{ℋ}$
8	2 7	eqeltrri	$⊢ ran T \in S_{ℋ}$