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{\upharpoonright }_{𝑠}\mathrm{ran}F$$
	rndrhmcl.1	$$⊢\underset{\dot{}}{0}=0_N$$
	rndrhmcl.h	$$⊢\phi \to F\in \left(M\mathrm{RingHom}N\right)$$
	rndrhmcl.2	$$⊢\phi \to \mathrm{ran}F\ne \left\{\underset{\dot{}}{0}\right\}$$
	rndrhmcl.m	$$⊢\phi \to M\in \mathrm{DivRing}$$
Assertion	rndrhmcl	$$⊢\phi \to R\in \mathrm{DivRing}$$

Proof

Step	Hyp	Ref	Expression
1		rndrhmcl.r	$$⊢R=N{\upharpoonright }_{𝑠}\mathrm{ran}F$$
2		rndrhmcl.1	$$⊢\underset{\dot{}}{0}=0_N$$
3		rndrhmcl.h	$$⊢\phi \to F\in \left(M\mathrm{RingHom}N\right)$$
4		rndrhmcl.2	$$⊢\phi \to \mathrm{ran}F\ne \left\{\underset{\dot{}}{0}\right\}$$
5		rndrhmcl.m	$$⊢\phi \to M\in \mathrm{DivRing}$$
6		imadmrn	$$⊢F\left[\mathrm{dom}F\right]=\mathrm{ran}F$$
7	6	oveq2i	$$⊢N{\upharpoonright }_{𝑠}F\left[\mathrm{dom}F\right]=N{\upharpoonright }_{𝑠}\mathrm{ran}F$$
8	1 7	eqtr4i	$$⊢R=N{\upharpoonright }_{𝑠}F\left[\mathrm{dom}F\right]$$
9		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
10		eqid	$$⊢{\mathrm{Base}}_N={\mathrm{Base}}_N$$
11	9 10	rhmf	$$⊢F\in \left(M\mathrm{RingHom}N\right)\to F:{\mathrm{Base}}_M⟶{\mathrm{Base}}_N$$
12	3 11	syl	$$⊢\phi \to F:{\mathrm{Base}}_M⟶{\mathrm{Base}}_N$$
13	12	fdmd	$$⊢\phi \to \mathrm{dom}F={\mathrm{Base}}_M$$
14	9	sdrgid	$$⊢M\in \mathrm{DivRing}\to {\mathrm{Base}}_M\in \mathrm{SubDRing}\left(M\right)$$
15	5 14	syl	$$⊢\phi \to {\mathrm{Base}}_M\in \mathrm{SubDRing}\left(M\right)$$
16	13 15	eqeltrd	$$⊢\phi \to \mathrm{dom}F\in \mathrm{SubDRing}\left(M\right)$$
17	8 2 3 16 4	imadrhmcl	$$⊢\phi \to R\in \mathrm{DivRing}$$