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 
|- I = ( invr ` R )
sdrginvcl.0 
|- .0. = ( 0g ` R )
Assertion sdrginvcl 
|- ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> ( I ` X ) e. A )

Proof

Step Hyp Ref Expression
1 sdrginvcl.i 
 |-  I = ( invr ` R )
2 sdrginvcl.0 
 |-  .0. = ( 0g ` R )
3 issdrg 
 |-  ( A e. ( SubDRing ` R ) <-> ( R e. DivRing /\ A e. ( SubRing ` R ) /\ ( R |`s A ) e. DivRing ) )
4 3 biimpi 
 |-  ( A e. ( SubDRing ` R ) -> ( R e. DivRing /\ A e. ( SubRing ` R ) /\ ( R |`s A ) e. DivRing ) )
5 4 3ad2ant1 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> ( R e. DivRing /\ A e. ( SubRing ` R ) /\ ( R |`s A ) e. DivRing ) )
6 5 simp3d 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> ( R |`s A ) e. DivRing )
7 simp2 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> X e. A )
8 5 simp2d 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> A e. ( SubRing ` R ) )
9 eqid 
 |-  ( R |`s A ) = ( R |`s A )
10 9 subrgbas 
 |-  ( A e. ( SubRing ` R ) -> A = ( Base ` ( R |`s A ) ) )
11 8 10 syl 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> A = ( Base ` ( R |`s A ) ) )
12 7 11 eleqtrd 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> X e. ( Base ` ( R |`s A ) ) )
13 simp3 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> X =/= .0. )
14 9 2 subrg0 
 |-  ( A e. ( SubRing ` R ) -> .0. = ( 0g ` ( R |`s A ) ) )
15 8 14 syl 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> .0. = ( 0g ` ( R |`s A ) ) )
16 13 15 neeqtrd 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> X =/= ( 0g ` ( R |`s A ) ) )
17 eqid 
 |-  ( Base ` ( R |`s A ) ) = ( Base ` ( R |`s A ) )
18 eqid 
 |-  ( 0g ` ( R |`s A ) ) = ( 0g ` ( R |`s A ) )
19 eqid 
 |-  ( invr ` ( R |`s A ) ) = ( invr ` ( R |`s A ) )
20 17 18 19 drnginvrcl 
 |-  ( ( ( R |`s A ) e. DivRing /\ X e. ( Base ` ( R |`s A ) ) /\ X =/= ( 0g ` ( R |`s A ) ) ) -> ( ( invr ` ( R |`s A ) ) ` X ) e. ( Base ` ( R |`s A ) ) )
21 6 12 16 20 syl3anc 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> ( ( invr ` ( R |`s A ) ) ` X ) e. ( Base ` ( R |`s A ) ) )
22 eqid 
 |-  ( Unit ` ( R |`s A ) ) = ( Unit ` ( R |`s A ) )
23 17 22 18 drngunit 
 |-  ( ( R |`s A ) e. DivRing -> ( X e. ( Unit ` ( R |`s A ) ) <-> ( X e. ( Base ` ( R |`s A ) ) /\ X =/= ( 0g ` ( R |`s A ) ) ) ) )
24 23 biimpar 
 |-  ( ( ( R |`s A ) e. DivRing /\ ( X e. ( Base ` ( R |`s A ) ) /\ X =/= ( 0g ` ( R |`s A ) ) ) ) -> X e. ( Unit ` ( R |`s A ) ) )
25 6 12 16 24 syl12anc 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> X e. ( Unit ` ( R |`s A ) ) )
26 9 1 22 19 subrginv 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. ( Unit ` ( R |`s A ) ) ) -> ( I ` X ) = ( ( invr ` ( R |`s A ) ) ` X ) )
27 8 25 26 syl2anc 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> ( I ` X ) = ( ( invr ` ( R |`s A ) ) ` X ) )
28 21 27 11 3eltr4d 
 |-  ( ( A e. ( SubDRing ` R ) /\ X e. A /\ X =/= .0. ) -> ( I ` X ) e. A )