Metamath Proof Explorer

Theorem sdrgdvcl

Description: A sub-division-ring is closed under the ring division operation. (Contributed by Thierry Arnoux, 15-Jan-2025)

Ref Expression
Hypotheses sdrgdvcl.i ⊢ / = ( /r ‘ 𝑅 )
sdrgdvcl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
sdrgdvcl.a ⊢ ( 𝜑 → 𝐴 ∈ ( SubDRing ‘ 𝑅 ) )
sdrgdvcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
sdrgdvcl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
sdrgdvcl.1 ⊢ ( 𝜑 → 𝑌 ≠ 0 )
Assertion sdrgdvcl ( 𝜑 → ( 𝑋 / 𝑌 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 sdrgdvcl.i ⊢ / = ( /r ‘ 𝑅 )
2 sdrgdvcl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 sdrgdvcl.a ⊢ ( 𝜑 → 𝐴 ∈ ( SubDRing ‘ 𝑅 ) )
4 sdrgdvcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
5 sdrgdvcl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
6 sdrgdvcl.1 ⊢ ( 𝜑 → 𝑌 ≠ 0 )
7 issdrg ⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝐴 ) ∈ DivRing ) )
8 3 7 sylib ⊢ ( 𝜑 → ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝐴 ) ∈ DivRing ) )
9 8 simp3d ⊢ ( 𝜑 → ( 𝑅 ↾s 𝐴 ) ∈ DivRing )
10 9 drngringd ⊢ ( 𝜑 → ( 𝑅 ↾s 𝐴 ) ∈ Ring )
11 8 simp2d ⊢ ( 𝜑 → 𝐴 ∈ ( SubRing ‘ 𝑅 ) )
12 eqid ⊢ ( 𝑅 ↾s 𝐴 ) = ( 𝑅 ↾s 𝐴 )
13 12 subrgbas ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
14 11 13 syl ⊢ ( 𝜑 → 𝐴 = ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
15 4 14 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
16 5 14 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
17 12 2 subrg0 ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 0 = ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) )
18 11 17 syl ⊢ ( 𝜑 → 0 = ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) )
19 6 18 neeqtrd ⊢ ( 𝜑 → 𝑌 ≠ ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) )
20 eqid ⊢ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) = ( Base ‘ ( 𝑅 ↾s 𝐴 ) )
21 eqid ⊢ ( Unit ‘ ( 𝑅 ↾s 𝐴 ) ) = ( Unit ‘ ( 𝑅 ↾s 𝐴 ) )
22 eqid ⊢ ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) = ( 0g ‘ ( 𝑅 ↾s 𝐴 ) )
23 20 21 22 drngunit ⊢ ( ( 𝑅 ↾s 𝐴 ) ∈ DivRing → ( 𝑌 ∈ ( Unit ‘ ( 𝑅 ↾s 𝐴 ) ) ↔ ( 𝑌 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ∧ 𝑌 ≠ ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) ) ) )
24 23 biimpar ⊢ ( ( ( 𝑅 ↾s 𝐴 ) ∈ DivRing ∧ ( 𝑌 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ∧ 𝑌 ≠ ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) ) ) → 𝑌 ∈ ( Unit ‘ ( 𝑅 ↾s 𝐴 ) ) )
25 9 16 19 24 syl12anc ⊢ ( 𝜑 → 𝑌 ∈ ( Unit ‘ ( 𝑅 ↾s 𝐴 ) ) )
26 eqid ⊢ ( /r ‘ ( 𝑅 ↾s 𝐴 ) ) = ( /r ‘ ( 𝑅 ↾s 𝐴 ) )
27 20 21 26 dvrcl ⊢ ( ( ( 𝑅 ↾s 𝐴 ) ∈ Ring ∧ 𝑋 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ∧ 𝑌 ∈ ( Unit ‘ ( 𝑅 ↾s 𝐴 ) ) ) → ( 𝑋 ( /r ‘ ( 𝑅 ↾s 𝐴 ) ) 𝑌 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
28 10 15 25 27 syl3anc ⊢ ( 𝜑 → ( 𝑋 ( /r ‘ ( 𝑅 ↾s 𝐴 ) ) 𝑌 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
29 12 1 21 26 subrgdv ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ ( Unit ‘ ( 𝑅 ↾s 𝐴 ) ) ) → ( 𝑋 / 𝑌 ) = ( 𝑋 ( /r ‘ ( 𝑅 ↾s 𝐴 ) ) 𝑌 ) )
30 11 4 25 29 syl3anc ⊢ ( 𝜑 → ( 𝑋 / 𝑌 ) = ( 𝑋 ( /r ‘ ( 𝑅 ↾s 𝐴 ) ) 𝑌 ) )
31 28 30 14 3eltr4d ⊢ ( 𝜑 → ( 𝑋 / 𝑌 ) ∈ 𝐴 )