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{\upharpoonright }_{𝑠}A$$
	sdrgunit.0	$$⊢\underset{\dot{}}{0}=0_R$$
	sdrgunit.u	$$⊢U=\mathrm{Unit}\left(S\right)$$
Assertion	sdrgunit	$$⊢A\in \mathrm{SubDRing}\left(R\right)\to \left(X\in U\leftrightarrow \left(X\in A\wedge X\ne \underset{\dot{}}{0}\right)\right)$$

Proof

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