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 ↾_{𝑠} A$
	sdrgunit.0	$⊢ \underset{˙}{0} = 0_{R}$
	sdrgunit.u	$⊢ U = Unit (S)$
Assertion	sdrgunit	$⊢ A \in SubDRing (R) \to (X \in U \leftrightarrow (X \in A \land X \neq \underset{˙}{0}))$

Step	Hyp	Ref	Expression
1		sdrgunit.s	$⊢ S = R ↾_{𝑠} A$
2		sdrgunit.0	$⊢ \underset{˙}{0} = 0_{R}$
3		sdrgunit.u	$⊢ U = Unit (S)$
4	1	sdrgdrng	$⊢ A \in SubDRing (R) \to S \in DivRing$
5		eqid	$⊢ {Base}_{S} = {Base}_{S}$
6		eqid	$⊢ 0_{S} = 0_{S}$
7	5 3 6	drngunit	$⊢ S \in DivRing \to (X \in U \leftrightarrow (X \in {Base}_{S} \land X \neq 0_{S}))$
8	4 7	syl	$⊢ A \in SubDRing (R) \to (X \in U \leftrightarrow (X \in {Base}_{S} \land X \neq 0_{S}))$
9	1	sdrgbas	$⊢ A \in SubDRing (R) \to A = {Base}_{S}$
10	9	eleq2d	$⊢ A \in SubDRing (R) \to (X \in A \leftrightarrow X \in {Base}_{S})$
11		sdrgsubrg	$⊢ A \in SubDRing (R) \to A \in SubRing (R)$
12	1 2	subrg0	$⊢ A \in SubRing (R) \to \underset{˙}{0} = 0_{S}$
13	11 12	syl	$⊢ A \in SubDRing (R) \to \underset{˙}{0} = 0_{S}$
14	13	neeq2d	$⊢ A \in SubDRing (R) \to (X \neq \underset{˙}{0} \leftrightarrow X \neq 0_{S})$
15	10 14	anbi12d	$⊢ A \in SubDRing (R) \to ((X \in A \land X \neq \underset{˙}{0}) \leftrightarrow (X \in {Base}_{S} \land X \neq 0_{S}))$
16	8 15	bitr4d	$⊢ A \in SubDRing (R) \to (X \in U \leftrightarrow (X \in A \land X \neq \underset{˙}{0}))$

Metamath Proof Explorer