Theorem isdomn4r

Description: A ring is a domain iff it is nonzero and the right cancellation law for multiplication holds. (Contributed by SN, 20-Jun-2025)

	Ref	Expression
Hypotheses	isdomn4r.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isdomn4r.0	⊢ 0 = ( 0g ‘ 𝑅 )
	isdomn4r.x	⊢ · = ( .r ‘ 𝑅 )
Assertion	isdomn4r	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ( ( 𝑎 · 𝑐 ) = ( 𝑏 · 𝑐 ) → 𝑎 = 𝑏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isdomn4r.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isdomn4r.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		isdomn4r.x	⊢ · = ( .r ‘ 𝑅 )
4		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
5	4 1	opprbas	⊢ 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) )
6	4 2	oppr0	⊢ 0 = ( 0g ‘ ( oppr ‘ 𝑅 ) )
7		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
8	5 6 7	isdomn4	⊢ ( ( oppr ‘ 𝑅 ) ∈ Domn ↔ ( ( oppr ‘ 𝑅 ) ∈ NzRing ∧ ∀ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑎 ) = ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑏 ) → 𝑎 = 𝑏 ) ) )
9	4	opprdomnb	⊢ ( 𝑅 ∈ Domn ↔ ( oppr ‘ 𝑅 ) ∈ Domn )
10	4	opprnzrb	⊢ ( 𝑅 ∈ NzRing ↔ ( oppr ‘ 𝑅 ) ∈ NzRing )
11	1 3 4 7	opprmul	⊢ ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑎 ) = ( 𝑎 · 𝑐 )
12	1 3 4 7	opprmul	⊢ ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑏 ) = ( 𝑏 · 𝑐 )
13	11 12	eqeq12i	⊢ ( ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑎 ) = ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑏 ) ↔ ( 𝑎 · 𝑐 ) = ( 𝑏 · 𝑐 ) )
14	13	imbi1i	⊢ ( ( ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑎 ) = ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑏 ) → 𝑎 = 𝑏 ) ↔ ( ( 𝑎 · 𝑐 ) = ( 𝑏 · 𝑐 ) → 𝑎 = 𝑏 ) )
15	14	3ralbii	⊢ ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ( ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑎 ) = ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑏 ) → 𝑎 = 𝑏 ) ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ( ( 𝑎 · 𝑐 ) = ( 𝑏 · 𝑐 ) → 𝑎 = 𝑏 ) )
16		ralrot3	⊢ ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ( ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑎 ) = ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑏 ) → 𝑎 = 𝑏 ) ↔ ∀ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑎 ) = ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑏 ) → 𝑎 = 𝑏 ) )
17	15 16	bitr3i	⊢ ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ( ( 𝑎 · 𝑐 ) = ( 𝑏 · 𝑐 ) → 𝑎 = 𝑏 ) ↔ ∀ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑎 ) = ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑏 ) → 𝑎 = 𝑏 ) )
18	10 17	anbi12i	⊢ ( ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ( ( 𝑎 · 𝑐 ) = ( 𝑏 · 𝑐 ) → 𝑎 = 𝑏 ) ) ↔ ( ( oppr ‘ 𝑅 ) ∈ NzRing ∧ ∀ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑎 ) = ( 𝑐 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑏 ) → 𝑎 = 𝑏 ) ) )
19	8 9 18	3bitr4i	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ( ( 𝑎 · 𝑐 ) = ( 𝑏 · 𝑐 ) → 𝑎 = 𝑏 ) ) )