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. ) ) )