Definition df-domn 20695

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

Assertion

Ref	Expression
df-domn	⊢ Domn = {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))}

Distinct variable group:   𝑟,𝑏,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-domn

Step	Hyp	Ref	Expression
1		cdomn 20692	. 2 class Domn
2		vx	. . . . . . . . . . 11 setvar 𝑥
3	2	cv 1539	. . . . . . . . . 10 class 𝑥
4		vy	. . . . . . . . . . 11 setvar 𝑦
5	4	cv 1539	. . . . . . . . . 10 class 𝑦
6		vr	. . . . . . . . . . . 12 setvar 𝑟
7	6	cv 1539	. . . . . . . . . . 11 class 𝑟
8		cmulr 17298	. . . . . . . . . . 11 class .r
9	7, 8	cfv 6561	. . . . . . . . . 10 class (.r‘𝑟)
10	3, 5, 9	co 7431	. . . . . . . . 9 class (𝑥(.r‘𝑟)𝑦)
11		vz	. . . . . . . . . 10 setvar 𝑧
12	11	cv 1539	. . . . . . . . 9 class 𝑧
13	10, 12	wceq 1540	. . . . . . . 8 wff (𝑥(.r‘𝑟)𝑦) = 𝑧
14	2, 11	weq 1962	. . . . . . . . 9 wff 𝑥 = 𝑧
15	4, 11	weq 1962	. . . . . . . . 9 wff 𝑦 = 𝑧
16	14, 15	wo 848	. . . . . . . 8 wff (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)
17	13, 16	wi 4	. . . . . . 7 wff ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))
18		vb	. . . . . . . 8 setvar 𝑏
19	18	cv 1539	. . . . . . 7 class 𝑏
20	17, 4, 19	wral 3061	. . . . . 6 wff ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))
21	20, 2, 19	wral 3061	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))
22		c0g 17484	. . . . . 6 class 0g
23	7, 22	cfv 6561	. . . . 5 class (0g‘𝑟)
24	21, 11, 23	wsbc 3788	. . . 4 wff [(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))
25		cbs 17247	. . . . 5 class Base
26	7, 25	cfv 6561	. . . 4 class (Base‘𝑟)
27	24, 18, 26	wsbc 3788	. . 3 wff [(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))
28		cnzr 20512	. . 3 class NzRing
29	27, 6, 28	crab 3436	. 2 class {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))}
30	1, 29	wceq 1540	1 wff Domn = {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))}

This definition is referenced by:  isdomn  20705