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

Metamath Proof Explorer

Theorem sdrgunit

Description: A unit of a sub-division-ring is a nonzero element of the subring. (Contributed by SN, 19-Feb-2025)

Ref Expression
Hypotheses sdrgunit.s 
|- S = ( R |`s A )
sdrgunit.0 
|- .0. = ( 0g ` R )
sdrgunit.u 
|- U = ( Unit ` S )
Assertion sdrgunit 
|- ( A e. ( SubDRing ` R ) -> ( X e. U <-> ( X e. A /\ X =/= .0. ) ) )

Proof

Step Hyp Ref Expression
1 sdrgunit.s 
 |-  S = ( R |`s A )
2 sdrgunit.0 
 |-  .0. = ( 0g ` R )
3 sdrgunit.u 
 |-  U = ( Unit ` S )
4 1 sdrgdrng 
 |-  ( A e. ( SubDRing ` R ) -> S e. DivRing )
5 eqid 
 |-  ( Base ` S ) = ( Base ` S )
6 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
7 5 3 6 drngunit 
 |-  ( S e. DivRing -> ( X e. U <-> ( X e. ( Base ` S ) /\ X =/= ( 0g ` S ) ) ) )
8 4 7 syl 
 |-  ( A e. ( SubDRing ` R ) -> ( X e. U <-> ( X e. ( Base ` S ) /\ X =/= ( 0g ` S ) ) ) )
9 1 sdrgbas 
 |-  ( A e. ( SubDRing ` R ) -> A = ( Base ` S ) )
10 9 eleq2d 
 |-  ( A e. ( SubDRing ` R ) -> ( X e. A <-> X e. ( Base ` S ) ) )
11 sdrgsubrg 
 |-  ( A e. ( SubDRing ` R ) -> A e. ( SubRing ` R ) )
12 1 2 subrg0 
 |-  ( A e. ( SubRing ` R ) -> .0. = ( 0g ` S ) )
13 11 12 syl 
 |-  ( A e. ( SubDRing ` R ) -> .0. = ( 0g ` S ) )
14 13 neeq2d 
 |-  ( A e. ( SubDRing ` R ) -> ( X =/= .0. <-> X =/= ( 0g ` S ) ) )
15 10 14 anbi12d 
 |-  ( A e. ( SubDRing ` R ) -> ( ( X e. A /\ X =/= .0. ) <-> ( X e. ( Base ` S ) /\ X =/= ( 0g ` S ) ) ) )
16 8 15 bitr4d 
 |-  ( A e. ( SubDRing ` R ) -> ( X e. U <-> ( X e. A /\ X =/= .0. ) ) )