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

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 ` R )
sdrgdvcl.0 
|- .0. = ( 0g ` R )
sdrgdvcl.a 
|- ( ph -> A e. ( SubDRing ` R ) )
sdrgdvcl.x 
|- ( ph -> X e. A )
sdrgdvcl.y 
|- ( ph -> Y e. A )
sdrgdvcl.1 
|- ( ph -> Y =/= .0. )
Assertion sdrgdvcl 
|- ( ph -> ( X ./ Y ) e. A )

Proof

Step Hyp Ref Expression
1 sdrgdvcl.i 
 |-  ./ = ( /r ` R )
2 sdrgdvcl.0 
 |-  .0. = ( 0g ` R )
3 sdrgdvcl.a 
 |-  ( ph -> A e. ( SubDRing ` R ) )
4 sdrgdvcl.x 
 |-  ( ph -> X e. A )
5 sdrgdvcl.y 
 |-  ( ph -> Y e. A )
6 sdrgdvcl.1 
 |-  ( ph -> Y =/= .0. )
7 issdrg 
 |-  ( A e. ( SubDRing ` R ) <-> ( R e. DivRing /\ A e. ( SubRing ` R ) /\ ( R |`s A ) e. DivRing ) )
8 3 7 sylib 
 |-  ( ph -> ( R e. DivRing /\ A e. ( SubRing ` R ) /\ ( R |`s A ) e. DivRing ) )
9 8 simp3d 
 |-  ( ph -> ( R |`s A ) e. DivRing )
10 9 drngringd 
 |-  ( ph -> ( R |`s A ) e. Ring )
11 8 simp2d 
 |-  ( ph -> A e. ( SubRing ` R ) )
12 eqid 
 |-  ( R |`s A ) = ( R |`s A )
13 12 subrgbas 
 |-  ( A e. ( SubRing ` R ) -> A = ( Base ` ( R |`s A ) ) )
14 11 13 syl 
 |-  ( ph -> A = ( Base ` ( R |`s A ) ) )
15 4 14 eleqtrd 
 |-  ( ph -> X e. ( Base ` ( R |`s A ) ) )
16 5 14 eleqtrd 
 |-  ( ph -> Y e. ( Base ` ( R |`s A ) ) )
17 12 2 subrg0 
 |-  ( A e. ( SubRing ` R ) -> .0. = ( 0g ` ( R |`s A ) ) )
18 11 17 syl 
 |-  ( ph -> .0. = ( 0g ` ( R |`s A ) ) )
19 6 18 neeqtrd 
 |-  ( ph -> Y =/= ( 0g ` ( R |`s A ) ) )
20 eqid 
 |-  ( Base ` ( R |`s A ) ) = ( Base ` ( R |`s A ) )
21 eqid 
 |-  ( Unit ` ( R |`s A ) ) = ( Unit ` ( R |`s A ) )
22 eqid 
 |-  ( 0g ` ( R |`s A ) ) = ( 0g ` ( R |`s A ) )
23 20 21 22 drngunit 
 |-  ( ( R |`s A ) e. DivRing -> ( Y e. ( Unit ` ( R |`s A ) ) <-> ( Y e. ( Base ` ( R |`s A ) ) /\ Y =/= ( 0g ` ( R |`s A ) ) ) ) )
24 23 biimpar 
 |-  ( ( ( R |`s A ) e. DivRing /\ ( Y e. ( Base ` ( R |`s A ) ) /\ Y =/= ( 0g ` ( R |`s A ) ) ) ) -> Y e. ( Unit ` ( R |`s A ) ) )
25 9 16 19 24 syl12anc 
 |-  ( ph -> Y e. ( Unit ` ( R |`s A ) ) )
26 eqid 
 |-  ( /r ` ( R |`s A ) ) = ( /r ` ( R |`s A ) )
27 20 21 26 dvrcl 
 |-  ( ( ( R |`s A ) e. Ring /\ X e. ( Base ` ( R |`s A ) ) /\ Y e. ( Unit ` ( R |`s A ) ) ) -> ( X ( /r ` ( R |`s A ) ) Y ) e. ( Base ` ( R |`s A ) ) )
28 10 15 25 27 syl3anc 
 |-  ( ph -> ( X ( /r ` ( R |`s A ) ) Y ) e. ( Base ` ( R |`s A ) ) )
29 12 1 21 26 subrgdv 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. ( Unit ` ( R |`s A ) ) ) -> ( X ./ Y ) = ( X ( /r ` ( R |`s A ) ) Y ) )
30 11 4 25 29 syl3anc 
 |-  ( ph -> ( X ./ Y ) = ( X ( /r ` ( R |`s A ) ) Y ) )
31 28 30 14 3eltr4d 
 |-  ( ph -> ( X ./ Y ) e. A )