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 )