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

Metamath Proof Explorer

Theorem lmhmrnlss

Description: The range of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Assertion lmhmrnlss ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ran 𝐹 ∈ ( LSubSp ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
2 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
3 1 2 lmhmf ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
4 ffn ⊢ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
5 fnima ⊢ ( 𝐹 Fn ( Base ‘ 𝑆 ) → ( 𝐹 “ ( Base ‘ 𝑆 ) ) = ran 𝐹 )
6 3 4 5 3syl ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝐹 “ ( Base ‘ 𝑆 ) ) = ran 𝐹 )
7 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
8 eqid ⊢ ( LSubSp ‘ 𝑆 ) = ( LSubSp ‘ 𝑆 )
9 1 8 lss1 ⊢ ( 𝑆 ∈ LMod → ( Base ‘ 𝑆 ) ∈ ( LSubSp ‘ 𝑆 ) )
10 7 9 syl ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Base ‘ 𝑆 ) ∈ ( LSubSp ‘ 𝑆 ) )
11 eqid ⊢ ( LSubSp ‘ 𝑇 ) = ( LSubSp ‘ 𝑇 )
12 8 11 lmhmima ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( Base ‘ 𝑆 ) ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝐹 “ ( Base ‘ 𝑆 ) ) ∈ ( LSubSp ‘ 𝑇 ) )
13 10 12 mpdan ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝐹 “ ( Base ‘ 𝑆 ) ) ∈ ( LSubSp ‘ 𝑇 ) )
14 6 13 eqeltrrd ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ran 𝐹 ∈ ( LSubSp ‘ 𝑇 ) )