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	⊢ 𝑅 = ( 𝑁 ↾s ran 𝐹 )
	rndrhmcl.1	⊢ 0 = ( 0g ‘ 𝑁 )
	rndrhmcl.h	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) )
	rndrhmcl.2	⊢ ( 𝜑 → ran 𝐹 ≠ { 0 } )
	rndrhmcl.m	⊢ ( 𝜑 → 𝑀 ∈ DivRing )
Assertion	rndrhmcl	⊢ ( 𝜑 → 𝑅 ∈ DivRing )

Proof

Step	Hyp	Ref	Expression
1		rndrhmcl.r	⊢ 𝑅 = ( 𝑁 ↾s ran 𝐹 )
2		rndrhmcl.1	⊢ 0 = ( 0g ‘ 𝑁 )
3		rndrhmcl.h	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) )
4		rndrhmcl.2	⊢ ( 𝜑 → ran 𝐹 ≠ { 0 } )
5		rndrhmcl.m	⊢ ( 𝜑 → 𝑀 ∈ DivRing )
6		imadmrn	⊢ ( 𝐹 “ dom 𝐹 ) = ran 𝐹
7	6	oveq2i	⊢ ( 𝑁 ↾s ( 𝐹 “ dom 𝐹 ) ) = ( 𝑁 ↾s ran 𝐹 )
8	1 7	eqtr4i	⊢ 𝑅 = ( 𝑁 ↾s ( 𝐹 “ dom 𝐹 ) )
9		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
10		eqid	⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
11	9 10	rhmf	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
12	3 11	syl	⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
13	12	fdmd	⊢ ( 𝜑 → dom 𝐹 = ( Base ‘ 𝑀 ) )
14	9	sdrgid	⊢ ( 𝑀 ∈ DivRing → ( Base ‘ 𝑀 ) ∈ ( SubDRing ‘ 𝑀 ) )
15	5 14	syl	⊢ ( 𝜑 → ( Base ‘ 𝑀 ) ∈ ( SubDRing ‘ 𝑀 ) )
16	13 15	eqeltrd	⊢ ( 𝜑 → dom 𝐹 ∈ ( SubDRing ‘ 𝑀 ) )
17	8 2 3 16 4	imadrhmcl	⊢ ( 𝜑 → 𝑅 ∈ DivRing )