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 eqid 
 |-  ( Base ` M ) = ( Base ` M )
2 eqid 
 |-  ( Base ` N ) = ( Base ` N )
3 1 2 rhmf 
 |-  ( F e. ( M RingHom N ) -> F : ( Base ` M ) --> ( Base ` N ) )
4 3 ffnd 
 |-  ( F e. ( M RingHom N ) -> F Fn ( Base ` M ) )
5 fnima 
 |-  ( F Fn ( Base ` M ) -> ( F " ( Base ` M ) ) = ran F )
6 4 5 syl 
 |-  ( F e. ( M RingHom N ) -> ( F " ( Base ` M ) ) = ran F )
7 rhmrcl1 
 |-  ( F e. ( M RingHom N ) -> M e. Ring )
8 1 subrgid 
 |-  ( M e. Ring -> ( Base ` M ) e. ( SubRing ` M ) )
9 7 8 syl 
 |-  ( F e. ( M RingHom N ) -> ( Base ` M ) e. ( SubRing ` M ) )
10 rhmima 
 |-  ( ( F e. ( M RingHom N ) /\ ( Base ` M ) e. ( SubRing ` M ) ) -> ( F " ( Base ` M ) ) e. ( SubRing ` N ) )
11 9 10 mpdan 
 |-  ( F e. ( M RingHom N ) -> ( F " ( Base ` M ) ) e. ( SubRing ` N ) )
12 6 11 eqeltrrd 
 |-  ( F e. ( M RingHom N ) -> ran F e. ( SubRing ` N ) )