Theorem isunit3

Description: Alternate definition of being a unit. (Contributed by Thierry Arnoux, 3-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		isunit2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isunit2.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		isunit2.m	⊢ · = ( .r ‘ 𝑅 )
4		isunit2.1	⊢ 1 = ( 1r ‘ 𝑅 )
5		isunit3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		isunit3.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7	1 2 3 4	isunit2	⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝐵 ∧ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) )
8	5	biantrurd	⊢ ( 𝜑 → ( ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) ) )
9	7 8	bitr4id	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) )
10		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
11	10 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
12	10 4	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
13	10 3	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
14	10	ringmgp	⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
15	6 14	syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
16	11 12 13 15 5	mndlrinvb	⊢ ( 𝜑 → ( ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑋 ) = 1 ) ) )
17	9 16	bitrd	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑋 ) = 1 ) ) )