Definition df-domn 13739

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 = { r e. NzRing | [. ( Base ` r ) / b ]. [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) }

Distinct variable group:   r, b, x, y, z

Detailed syntax breakdown of Definition df-domn

Step	Hyp	Ref	Expression
1		cdomn 13736	. 2 class Domn
2		vx	. . . . . . . . . . 11 setvar x
3	2	cv 1363	. . . . . . . . . 10 class x
4		vy	. . . . . . . . . . 11 setvar y
5	4	cv 1363	. . . . . . . . . 10 class y
6		vr	. . . . . . . . . . . 12 setvar r
7	6	cv 1363	. . . . . . . . . . 11 class r
8		cmulr 12686	. . . . . . . . . . 11 class .r
9	7, 8	cfv 5246	. . . . . . . . . 10 class ( .r ` r )
10	3, 5, 9	co 5910	. . . . . . . . 9 class ( x ( .r ` r ) y )
11		vz	. . . . . . . . . 10 setvar z
12	11	cv 1363	. . . . . . . . 9 class z
13	10, 12	wceq 1364	. . . . . . . 8 wff ( x ( .r ` r ) y ) = z
14	2, 11	weq 1514	. . . . . . . . 9 wff x = z
15	4, 11	weq 1514	. . . . . . . . 9 wff y = z
16	14, 15	wo 709	. . . . . . . 8 wff ( x = z \/ y = z )
17	13, 16	wi 4	. . . . . . 7 wff ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) )
18		vb	. . . . . . . 8 setvar b
19	18	cv 1363	. . . . . . 7 class b
20	17, 4, 19	wral 2472	. . . . . 6 wff A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) )
21	20, 2, 19	wral 2472	. . . . 5 wff A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) )
22		c0g 12857	. . . . . 6 class 0g
23	7, 22	cfv 5246	. . . . 5 class ( 0g ` r )
24	21, 11, 23	wsbc 2985	. . . 4 wff [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) )
25		cbs 12608	. . . . 5 class Base
26	7, 25	cfv 5246	. . . 4 class ( Base ` r )
27	24, 18, 26	wsbc 2985	. . 3 wff [. ( Base ` r ) / b ]. [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) )
28		cnzr 13659	. . 3 class NzRing
29	27, 6, 28	crab 2476	. 2 class { r e. NzRing | [. ( Base ` r ) / b ]. [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) }
30	1, 29	wceq 1364	1 wff Domn = { r e. NzRing | [. ( Base ` r ) / b ]. [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) }

This definition is referenced by:  isdomn  13749