Metamath Proof Explorer

Theorem rnrhmsubrg

Description: The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023)

Ref Expression
Assertion rnrhmsubrg 
|- ( F e. ( M RingHom N ) -> ran F e. ( SubRing ` N ) )

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( F " ( Base ` M ) ) = ran ( F |` ( Base ` M ) )
2 eqid 
 |-  ( Base ` M ) = ( Base ` M )
3 eqid 
 |-  ( Base ` N ) = ( Base ` N )
4 2 3 rhmf 
 |-  ( F e. ( M RingHom N ) -> F : ( Base ` M ) --> ( Base ` N ) )
5 4 ffnd 
 |-  ( F e. ( M RingHom N ) -> F Fn ( Base ` M ) )
6 fnresdm 
 |-  ( F Fn ( Base ` M ) -> ( F |` ( Base ` M ) ) = F )
7 5 6 syl 
 |-  ( F e. ( M RingHom N ) -> ( F |` ( Base ` M ) ) = F )
8 7 rneqd 
 |-  ( F e. ( M RingHom N ) -> ran ( F |` ( Base ` M ) ) = ran F )
9 1 8 syl5req 
 |-  ( F e. ( M RingHom N ) -> ran F = ( F " ( Base ` M ) ) )
10 rhmrcl1 
 |-  ( F e. ( M RingHom N ) -> M e. Ring )
11 2 subrgid 
 |-  ( M e. Ring -> ( Base ` M ) e. ( SubRing ` M ) )
12 10 11 syl 
 |-  ( F e. ( M RingHom N ) -> ( Base ` M ) e. ( SubRing ` M ) )
13 rhmima 
 |-  ( ( F e. ( M RingHom N ) /\ ( Base ` M ) e. ( SubRing ` M ) ) -> ( F " ( Base ` M ) ) e. ( SubRing ` N ) )
14 12 13 mpdan 
 |-  ( F e. ( M RingHom N ) -> ( F " ( Base ` M ) ) e. ( SubRing ` N ) )
15 9 14 eqeltrd 
 |-  ( F e. ( M RingHom N ) -> ran F e. ( SubRing ` N ) )