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 e. LinOp
Assertion rnelshi 
|- ran T e. SH

Proof

Step Hyp Ref Expression
1 rnelsh.1 
 |-  T e. LinOp
2 imadmrn 
 |-  ( T " dom T ) = ran T
3 1 lnopfi 
 |-  T : ~H --> ~H
4 3 fdmi 
 |-  dom T = ~H
5 helsh 
 |-  ~H e. SH
6 4 5 eqeltri 
 |-  dom T e. SH
7 1 6 imaelshi 
 |-  ( T " dom T ) e. SH
8 2 7 eqeltrri 
 |-  ran T e. SH