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

Metamath Proof Explorer

Definition df-domn

Description: Adomain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015)

Ref Expression
Assertion df-domn ⊢ Domn = r ∈ NzRing | [˙Base r / b]˙ [˙0 r / z]˙ ∀ x ∈ b ∀ y ∈ b x ⋅ r y = z → x = z ∨ y = z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdomn class Domn
1 vr setvar r
2 cnzr class NzRing
3 cbs class Base
4 1 cv setvar r
5 4 3 cfv class Base r
6 vb setvar b
7 c0g class 0 𝑔
8 4 7 cfv class 0 r
9 vz setvar z
10 vx setvar x
11 6 cv setvar b
12 vy setvar y
13 10 cv setvar x
14 cmulr class ⋅ 𝑟
15 4 14 cfv class ⋅ r
16 12 cv setvar y
17 13 16 15 co class x ⋅ r y
18 9 cv setvar z
19 17 18 wceq wff x ⋅ r y = z
20 13 18 wceq wff x = z
21 16 18 wceq wff y = z
22 20 21 wo wff x = z ∨ y = z
23 19 22 wi wff x ⋅ r y = z → x = z ∨ y = z
24 23 12 11 wral wff ∀ y ∈ b x ⋅ r y = z → x = z ∨ y = z
25 24 10 11 wral wff ∀ x ∈ b ∀ y ∈ b x ⋅ r y = z → x = z ∨ y = z
26 25 9 8 wsbc wff [˙0 r / z]˙ ∀ x ∈ b ∀ y ∈ b x ⋅ r y = z → x = z ∨ y = z
27 26 6 5 wsbc wff [˙Base r / b]˙ [˙0 r / z]˙ ∀ x ∈ b ∀ y ∈ b x ⋅ r y = z → x = z ∨ y = z
28 27 1 2 crab class r ∈ NzRing | [˙Base r / b]˙ [˙0 r / z]˙ ∀ x ∈ b ∀ y ∈ b x ⋅ r y = z → x = z ∨ y = z
29 0 28 wceq wff Domn = r ∈ NzRing | [˙Base r / b]˙ [˙0 r / z]˙ ∀ x ∈ b ∀ y ∈ b x ⋅ r y = z → x = z ∨ y = z