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 = { 𝑟 ∈ NzRing ∣ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( 0g ‘ 𝑟 ) / 𝑧 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdomn	⊢ Domn
1		vr	⊢ 𝑟
2		cnzr	⊢ NzRing
3		cbs	⊢ Base
4	1	cv	⊢ 𝑟
5	4 3	cfv	⊢ ( Base ‘ 𝑟 )
6		vb	⊢ 𝑏
7		c0g	⊢ 0g
8	4 7	cfv	⊢ ( 0g ‘ 𝑟 )
9		vz	⊢ 𝑧
10		vx	⊢ 𝑥
11	6	cv	⊢ 𝑏
12		vy	⊢ 𝑦
13	10	cv	⊢ 𝑥
14		cmulr	⊢ .r
15	4 14	cfv	⊢ ( .r ‘ 𝑟 )
16	12	cv	⊢ 𝑦
17	13 16 15	co	⊢ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 )
18	9	cv	⊢ 𝑧
19	17 18	wceq	⊢ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧
20	13 18	wceq	⊢ 𝑥 = 𝑧
21	16 18	wceq	⊢ 𝑦 = 𝑧
22	20 21	wo	⊢ ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 )
23	19 22	wi	⊢ ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) )
24	23 12 11	wral	⊢ ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) )
25	24 10 11	wral	⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) )
26	25 9 8	wsbc	⊢ [ ( 0g ‘ 𝑟 ) / 𝑧 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) )
27	26 6 5	wsbc	⊢ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( 0g ‘ 𝑟 ) / 𝑧 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) )
28	27 1 2	crab	⊢ { 𝑟 ∈ NzRing ∣ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( 0g ‘ 𝑟 ) / 𝑧 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) }
29	0 28	wceq	⊢ Domn = { 𝑟 ∈ NzRing ∣ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( 0g ‘ 𝑟 ) / 𝑧 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) }