This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) ( ( 𝑎 · 𝑐 ) = ( 𝑏 · 𝑐 ) → 𝑎 = 𝑏 ) ) )