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 ⊢ B = Base R
isdomn4r.0 ⊢ 0 ˙ = 0 R
isdomn4r.x ⊢ · ˙ = ⋅ R
Assertion isdomn4r ⊢ R ∈ Domn ↔ R ∈ NzRing ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ∖ 0 ˙ a · ˙ c = b · ˙ c → a = b

Proof

Step Hyp Ref Expression
1 isdomn4r.b ⊢ B = Base R
2 isdomn4r.0 ⊢ 0 ˙ = 0 R
3 isdomn4r.x ⊢ · ˙ = ⋅ R
4 eqid ⊢ opp r ⁡ R = opp r ⁡ R
5 4 1 opprbas ⊢ B = Base opp r ⁡ R
6 4 2 oppr0 ⊢ 0 ˙ = 0 opp r ⁡ R
7 eqid ⊢ ⋅ opp r ⁡ R = ⋅ opp r ⁡ R
8 5 6 7 isdomn4 ⊢ opp r ⁡ R ∈ Domn ↔ opp r ⁡ R ∈ NzRing ∧ ∀ c ∈ B ∖ 0 ˙ ∀ a ∈ B ∀ b ∈ B c ⋅ opp r ⁡ R a = c ⋅ opp r ⁡ R b → a = b
9 4 opprdomnb ⊢ R ∈ Domn ↔ opp r ⁡ R ∈ Domn
10 4 opprnzrb ⊢ R ∈ NzRing ↔ opp r ⁡ R ∈ NzRing
11 1 3 4 7 opprmul ⊢ c ⋅ opp r ⁡ R a = a · ˙ c
12 1 3 4 7 opprmul ⊢ c ⋅ opp r ⁡ R b = b · ˙ c
13 11 12 eqeq12i ⊢ c ⋅ opp r ⁡ R a = c ⋅ opp r ⁡ R b ↔ a · ˙ c = b · ˙ c
14 13 imbi1i ⊢ c ⋅ opp r ⁡ R a = c ⋅ opp r ⁡ R b → a = b ↔ a · ˙ c = b · ˙ c → a = b
15 14 3ralbii ⊢ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ∖ 0 ˙ c ⋅ opp r ⁡ R a = c ⋅ opp r ⁡ R b → a = b ↔ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ∖ 0 ˙ a · ˙ c = b · ˙ c → a = b
16 ralrot3 ⊢ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ∖ 0 ˙ c ⋅ opp r ⁡ R a = c ⋅ opp r ⁡ R b → a = b ↔ ∀ c ∈ B ∖ 0 ˙ ∀ a ∈ B ∀ b ∈ B c ⋅ opp r ⁡ R a = c ⋅ opp r ⁡ R b → a = b
17 15 16 bitr3i ⊢ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ∖ 0 ˙ a · ˙ c = b · ˙ c → a = b ↔ ∀ c ∈ B ∖ 0 ˙ ∀ a ∈ B ∀ b ∈ B c ⋅ opp r ⁡ R a = c ⋅ opp r ⁡ R b → a = b
18 10 17 anbi12i ⊢ R ∈ NzRing ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ∖ 0 ˙ a · ˙ c = b · ˙ c → a = b ↔ opp r ⁡ R ∈ NzRing ∧ ∀ c ∈ B ∖ 0 ˙ ∀ a ∈ B ∀ b ∈ B c ⋅ opp r ⁡ R a = c ⋅ opp r ⁡ R b → a = b
19 8 9 18 3bitr4i ⊢ R ∈ Domn ↔ R ∈ NzRing ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ∖ 0 ˙ a · ˙ c = b · ˙ c → a = b