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

Metamath Proof Explorer

Theorem rndrhmcl

Description: The image of a division ring by a ring homomorphism is a division ring. (Contributed by Thierry Arnoux, 25-Feb-2025)

Ref Expression
Hypotheses rndrhmcl.r 
|- R = ( N |`s ran F )
rndrhmcl.1 
|- .0. = ( 0g ` N )
rndrhmcl.h 
|- ( ph -> F e. ( M RingHom N ) )
rndrhmcl.2 
|- ( ph -> ran F =/= { .0. } )
rndrhmcl.m 
|- ( ph -> M e. DivRing )
Assertion rndrhmcl 
|- ( ph -> R e. DivRing )

Proof

Step Hyp Ref Expression
1 rndrhmcl.r 
 |-  R = ( N |`s ran F )
2 rndrhmcl.1 
 |-  .0. = ( 0g ` N )
3 rndrhmcl.h 
 |-  ( ph -> F e. ( M RingHom N ) )
4 rndrhmcl.2 
 |-  ( ph -> ran F =/= { .0. } )
5 rndrhmcl.m 
 |-  ( ph -> M e. DivRing )
6 imadmrn 
 |-  ( F " dom F ) = ran F
7 6 oveq2i 
 |-  ( N |`s ( F " dom F ) ) = ( N |`s ran F )
8 1 7 eqtr4i 
 |-  R = ( N |`s ( F " dom F ) )
9 eqid 
 |-  ( Base ` M ) = ( Base ` M )
10 eqid 
 |-  ( Base ` N ) = ( Base ` N )
11 9 10 rhmf 
 |-  ( F e. ( M RingHom N ) -> F : ( Base ` M ) --> ( Base ` N ) )
12 3 11 syl 
 |-  ( ph -> F : ( Base ` M ) --> ( Base ` N ) )
13 12 fdmd 
 |-  ( ph -> dom F = ( Base ` M ) )
14 9 sdrgid 
 |-  ( M e. DivRing -> ( Base ` M ) e. ( SubDRing ` M ) )
15 5 14 syl 
 |-  ( ph -> ( Base ` M ) e. ( SubDRing ` M ) )
16 13 15 eqeltrd 
 |-  ( ph -> dom F e. ( SubDRing ` M ) )
17 8 2 3 16 4 imadrhmcl 
 |-  ( ph -> R e. DivRing )