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 ↾ 𝑠 ran ⁡ F
rndrhmcl.1 ⊢ 0 ˙ = 0 N
rndrhmcl.h ⊢ φ → F ∈ M RingHom N
rndrhmcl.2 ⊢ φ → ran ⁡ F ≠ 0 ˙
rndrhmcl.m ⊢ φ → M ∈ DivRing
Assertion rndrhmcl ⊢ φ → R ∈ DivRing

Proof

Step Hyp Ref Expression
1 rndrhmcl.r ⊢ R = N ↾ 𝑠 ran ⁡ F
2 rndrhmcl.1 ⊢ 0 ˙ = 0 N
3 rndrhmcl.h ⊢ φ → F ∈ M RingHom N
4 rndrhmcl.2 ⊢ φ → ran ⁡ F ≠ 0 ˙
5 rndrhmcl.m ⊢ φ → M ∈ DivRing
6 imadmrn ⊢ F dom ⁡ F = ran ⁡ F
7 6 oveq2i ⊢ N ↾ 𝑠 F dom ⁡ F = N ↾ 𝑠 ran ⁡ F
8 1 7 eqtr4i ⊢ R = N ↾ 𝑠 F dom ⁡ F
9 eqid ⊢ Base M = Base M
10 eqid ⊢ Base N = Base N
11 9 10 rhmf ⊢ F ∈ M RingHom N → F : Base M ⟶ Base N
12 3 11 syl ⊢ φ → F : Base M ⟶ Base N
13 12 fdmd ⊢ φ → dom ⁡ F = Base M
14 9 sdrgid ⊢ M ∈ DivRing → Base M ∈ SubDRing ⁡ M
15 5 14 syl ⊢ φ → Base M ∈ SubDRing ⁡ M
16 13 15 eqeltrd ⊢ φ → dom ⁡ F ∈ SubDRing ⁡ M
17 8 2 3 16 4 imadrhmcl ⊢ φ → R ∈ DivRing