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 = { 𝑟 ∈ 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 ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) }