This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sdrginvcl

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

Ref Expression
Hypotheses sdrginvcl.i ⊢ 𝐼 = ( invr ‘ 𝑅 )
sdrginvcl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion sdrginvcl ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 sdrginvcl.i ⊢ 𝐼 = ( invr ‘ 𝑅 )
2 sdrginvcl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 issdrg ⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝐴 ) ∈ DivRing ) )
4 3 biimpi ⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝐴 ) ∈ DivRing ) )
5 4 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝐴 ) ∈ DivRing ) )
6 5 simp3d ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → ( 𝑅 ↾s 𝐴 ) ∈ DivRing )
7 simp2 ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝐴 )
8 5 simp2d ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → 𝐴 ∈ ( SubRing ‘ 𝑅 ) )
9 eqid ⊢ ( 𝑅 ↾s 𝐴 ) = ( 𝑅 ↾s 𝐴 )
10 9 subrgbas ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
11 8 10 syl ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → 𝐴 = ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
12 7 11 eleqtrd ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
13 simp3 ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ 0 )
14 9 2 subrg0 ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 0 = ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) )
15 8 14 syl ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → 0 = ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) )
16 13 15 neeqtrd ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) )
17 eqid ⊢ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) = ( Base ‘ ( 𝑅 ↾s 𝐴 ) )
18 eqid ⊢ ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) = ( 0g ‘ ( 𝑅 ↾s 𝐴 ) )
19 eqid ⊢ ( invr ‘ ( 𝑅 ↾s 𝐴 ) ) = ( invr ‘ ( 𝑅 ↾s 𝐴 ) )
20 17 18 19 drnginvrcl ⊢ ( ( ( 𝑅 ↾s 𝐴 ) ∈ DivRing ∧ 𝑋 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ∧ 𝑋 ≠ ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) ) → ( ( invr ‘ ( 𝑅 ↾s 𝐴 ) ) ‘ 𝑋 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
21 6 12 16 20 syl3anc ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → ( ( invr ‘ ( 𝑅 ↾s 𝐴 ) ) ‘ 𝑋 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
22 eqid ⊢ ( Unit ‘ ( 𝑅 ↾s 𝐴 ) ) = ( Unit ‘ ( 𝑅 ↾s 𝐴 ) )
23 17 22 18 drngunit ⊢ ( ( 𝑅 ↾s 𝐴 ) ∈ DivRing → ( 𝑋 ∈ ( Unit ‘ ( 𝑅 ↾s 𝐴 ) ) ↔ ( 𝑋 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ∧ 𝑋 ≠ ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) ) ) )
24 23 biimpar ⊢ ( ( ( 𝑅 ↾s 𝐴 ) ∈ DivRing ∧ ( 𝑋 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ∧ 𝑋 ≠ ( 0g ‘ ( 𝑅 ↾s 𝐴 ) ) ) ) → 𝑋 ∈ ( Unit ‘ ( 𝑅 ↾s 𝐴 ) ) )
25 6 12 16 24 syl12anc ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ( Unit ‘ ( 𝑅 ↾s 𝐴 ) ) )
26 9 1 22 19 subrginv ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ ( Unit ‘ ( 𝑅 ↾s 𝐴 ) ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( invr ‘ ( 𝑅 ↾s 𝐴 ) ) ‘ 𝑋 ) )
27 8 25 26 syl2anc ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → ( 𝐼 ‘ 𝑋 ) = ( ( invr ‘ ( 𝑅 ↾s 𝐴 ) ) ‘ 𝑋 ) )
28 21 27 11 3eltr4d ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 )