Theorem isunit2

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 ‘ 𝑅 )
Assertion	isunit2	⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝐵 ∧ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 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		eqid	⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
6	1 5 3	dvdsr	⊢ ( 𝑋 ( ∥r ‘ 𝑅 ) 1 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) )
7		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
8	7 1	opprbas	⊢ 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) )
9		eqid	⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
10		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
11	8 9 10	dvdsr	⊢ ( 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑢 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 1 ) )
12	1 3 7 10	opprmul	⊢ ( 𝑢 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = ( 𝑋 · 𝑢 )
13	12	eqeq1i	⊢ ( ( 𝑢 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 1 ↔ ( 𝑋 · 𝑢 ) = 1 )
14	13	rexbii	⊢ ( ∃ 𝑢 ∈ 𝐵 ( 𝑢 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 1 ↔ ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 )
15	14	anbi2i	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑢 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 1 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ) )
16	11 15	bitri	⊢ ( 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ) )
17	6 16	anbi12ci	⊢ ( ( 𝑋 ( ∥r ‘ 𝑅 ) 1 ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) )
18	2 4 5 7 9	isunit	⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ( ∥r ‘ 𝑅 ) 1 ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ) )
19		anandi	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) )
20	17 18 19	3bitr4i	⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝐵 ∧ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) )