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 ⊢ 𝑅 = ( 𝑁 ↾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 )