Theorem isunitc

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

	Ref	Expression
Hypotheses	isunit2.b	|- B = ( Base ` R )
	isunit2.u	|- U = ( Unit ` R )
	isunit2.m	|- .x. = ( .r ` R )
	isunit2.1	|- .1. = ( 1r ` R )
	isunitc.x	|- ( ph -> X e. B )
	isunitc.r	|- ( ph -> R e. CRing )
Assertion	isunitc	|- ( ph -> ( X e. U <-> E. y e. B ( X .x. y ) = .1. ) )

Proof

Step	Hyp	Ref	Expression
1		isunit2.b	|- B = ( Base ` R )
2		isunit2.u	|- U = ( Unit ` R )
3		isunit2.m	|- .x. = ( .r ` R )
4		isunit2.1	|- .1. = ( 1r ` R )
5		isunitc.x	|- ( ph -> X e. B )
6		isunitc.r	|- ( ph -> R e. CRing )
7	6	crngringd	|- ( ph -> R e. Ring )
8	1 2 3 4 5 7	isunit3	|- ( ph -> ( X e. U <-> E. y e. B ( ( X .x. y ) = .1. /\ ( y .x. X ) = .1. ) ) )
9	6	adantr	|- ( ( ph /\ y e. B ) -> R e. CRing )
10	5	adantr	|- ( ( ph /\ y e. B ) -> X e. B )
11		simpr	|- ( ( ph /\ y e. B ) -> y e. B )
12	1 3 9 10 11	crngcomd	|- ( ( ph /\ y e. B ) -> ( X .x. y ) = ( y .x. X ) )
13	12	eqeq1d	|- ( ( ph /\ y e. B ) -> ( ( X .x. y ) = .1. <-> ( y .x. X ) = .1. ) )
14	13	biimpa	|- ( ( ( ph /\ y e. B ) /\ ( X .x. y ) = .1. ) -> ( y .x. X ) = .1. )
15	14	ex	|- ( ( ph /\ y e. B ) -> ( ( X .x. y ) = .1. -> ( y .x. X ) = .1. ) )
16	15	pm4.71d	|- ( ( ph /\ y e. B ) -> ( ( X .x. y ) = .1. <-> ( ( X .x. y ) = .1. /\ ( y .x. X ) = .1. ) ) )
17	16	rexbidva	|- ( ph -> ( E. y e. B ( X .x. y ) = .1. <-> E. y e. B ( ( X .x. y ) = .1. /\ ( y .x. X ) = .1. ) ) )
18	8 17	bitr4d	|- ( ph -> ( X e. U <-> E. y e. B ( X .x. y ) = .1. ) )