Theorem isunitc

Description: Characterize units in a commutative ring. (Contributed by Thierry Arnoux, 6-Jun-2026)

	Ref	Expression
Hypotheses	isunit2.b	$$⊢B={\mathrm{Base}}_R$$
	isunit2.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
	isunit2.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	isunit2.1	$$⊢\underset{\dot{}}{1}=1_R$$
	isunitc.x	$$⊢\phi \to X\in B$$
	isunitc.r	$$⊢\phi \to R\in \mathrm{CRing}$$
Assertion	isunitc	$$⊢\phi \to \left(X\in U\leftrightarrow \exists y\in BX\underset{\dot{}}{·}y=\underset{\dot{}}{1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		isunit2.b	$$⊢B={\mathrm{Base}}_R$$
2		isunit2.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
3		isunit2.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		isunit2.1	$$⊢\underset{\dot{}}{1}=1_R$$
5		isunitc.x	$$⊢\phi \to X\in B$$
6		isunitc.r	$$⊢\phi \to R\in \mathrm{CRing}$$
7	6	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
8	1 2 3 4 5 7	isunit3	$$⊢\phi \to \left(X\in U\leftrightarrow \exists y\in B\left(X\underset{\dot{}}{·}y=\underset{\dot{}}{1}\wedge y\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\right)$$
9	6	adantr	$$⊢\left(\phi \wedge y\in B\right)\to R\in \mathrm{CRing}$$
10	5	adantr	$$⊢\left(\phi \wedge y\in B\right)\to X\in B$$
11		simpr	$$⊢\left(\phi \wedge y\in B\right)\to y\in B$$
12	1 3 9 10 11	crngcomd	$$⊢\left(\phi \wedge y\in B\right)\to X\underset{\dot{}}{·}y=y\underset{\dot{}}{·}X$$
13	12	eqeq1d	$$⊢\left(\phi \wedge y\in B\right)\to \left(X\underset{\dot{}}{·}y=\underset{\dot{}}{1}\leftrightarrow y\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)$$
14	13	biimpa	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge X\underset{\dot{}}{·}y=\underset{\dot{}}{1}\right)\to y\underset{\dot{}}{·}X=\underset{\dot{}}{1}$$
15	14	ex	$$⊢\left(\phi \wedge y\in B\right)\to \left(X\underset{\dot{}}{·}y=\underset{\dot{}}{1}\to y\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)$$
16	15	pm4.71d	$$⊢\left(\phi \wedge y\in B\right)\to \left(X\underset{\dot{}}{·}y=\underset{\dot{}}{1}\leftrightarrow \left(X\underset{\dot{}}{·}y=\underset{\dot{}}{1}\wedge y\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\right)$$
17	16	rexbidva	$$⊢\phi \to \left(\exists y\in BX\underset{\dot{}}{·}y=\underset{\dot{}}{1}\leftrightarrow \exists y\in B\left(X\underset{\dot{}}{·}y=\underset{\dot{}}{1}\wedge y\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\right)$$
18	8 17	bitr4d	$$⊢\phi \to \left(X\in U\leftrightarrow \exists y\in BX\underset{\dot{}}{·}y=\underset{\dot{}}{1}\right)$$