MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-domn Structured version   Visualization version   GIF version

Definition df-domn 19224
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
StepHypRef Expression
1 cdomn 19220 . 2 class Domn
2 vx . . . . . . . . . . 11 setvar 𝑥
32cv 1479 . . . . . . . . . 10 class 𝑥
4 vy . . . . . . . . . . 11 setvar 𝑦
54cv 1479 . . . . . . . . . 10 class 𝑦
6 vr . . . . . . . . . . . 12 setvar 𝑟
76cv 1479 . . . . . . . . . . 11 class 𝑟
8 cmulr 15882 . . . . . . . . . . 11 class .r
97, 8cfv 5857 . . . . . . . . . 10 class (.r𝑟)
103, 5, 9co 6615 . . . . . . . . 9 class (𝑥(.r𝑟)𝑦)
11 vz . . . . . . . . . 10 setvar 𝑧
1211cv 1479 . . . . . . . . 9 class 𝑧
1310, 12wceq 1480 . . . . . . . 8 wff (𝑥(.r𝑟)𝑦) = 𝑧
142, 11weq 1871 . . . . . . . . 9 wff 𝑥 = 𝑧
154, 11weq 1871 . . . . . . . . 9 wff 𝑦 = 𝑧
1614, 15wo 383 . . . . . . . 8 wff (𝑥 = 𝑧𝑦 = 𝑧)
1713, 16wi 4 . . . . . . 7 wff ((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧))
18 vb . . . . . . . 8 setvar 𝑏
1918cv 1479 . . . . . . 7 class 𝑏
2017, 4, 19wral 2908 . . . . . 6 wff 𝑦𝑏 ((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧))
2120, 2, 19wral 2908 . . . . 5 wff 𝑥𝑏𝑦𝑏 ((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧))
22 c0g 16040 . . . . . 6 class 0g
237, 22cfv 5857 . . . . 5 class (0g𝑟)
2421, 11, 23wsbc 3422 . . . 4 wff [(0g𝑟) / 𝑧]𝑥𝑏𝑦𝑏 ((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧))
25 cbs 15800 . . . . 5 class Base
267, 25cfv 5857 . . . 4 class (Base‘𝑟)
2724, 18, 26wsbc 3422 . . 3 wff [(Base‘𝑟) / 𝑏][(0g𝑟) / 𝑧]𝑥𝑏𝑦𝑏 ((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧))
28 cnzr 19197 . . 3 class NzRing
2927, 6, 28crab 2912 . 2 class {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g𝑟) / 𝑧]𝑥𝑏𝑦𝑏 ((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧))}
301, 29wceq 1480 1 wff Domn = {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g𝑟) / 𝑧]𝑥𝑏𝑦𝑏 ((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  isdomn  19234
  Copyright terms: Public domain W3C validator