Theorem isunitc

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

	Ref	Expression
Hypotheses	isunit2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isunit2.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	isunit2.m	⊢ · = ( .r ‘ 𝑅 )
	isunit2.1	⊢ 1 = ( 1r ‘ 𝑅 )
	isunitc.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	isunitc.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
Assertion	isunitc	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑋 · 𝑦 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		isunit2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isunit2.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		isunit2.m	⊢ · = ( .r ‘ 𝑅 )
4		isunit2.1	⊢ 1 = ( 1r ‘ 𝑅 )
5		isunitc.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		isunitc.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
7	6	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8	1 2 3 4 5 7	isunit3	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑋 ) = 1 ) ) )
9	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑅 ∈ CRing )
10	5	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
12	1 3 9 10 11	crngcomd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑋 · 𝑦 ) = ( 𝑦 · 𝑋 ) )
13	12	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑋 · 𝑦 ) = 1 ↔ ( 𝑦 · 𝑋 ) = 1 ) )
14	13	biimpa	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 · 𝑦 ) = 1 ) → ( 𝑦 · 𝑋 ) = 1 )
15	14	ex	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑋 · 𝑦 ) = 1 → ( 𝑦 · 𝑋 ) = 1 ) )
16	15	pm4.71d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑋 · 𝑦 ) = 1 ↔ ( ( 𝑋 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑋 ) = 1 ) ) )
17	16	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐵 ( 𝑋 · 𝑦 ) = 1 ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑋 ) = 1 ) ) )
18	8 17	bitr4d	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑋 · 𝑦 ) = 1 ) )