Theorem isidom3

Description: The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by AV, 12-Jul-2026)

	Ref	Expression
Hypotheses	isidom3.b	|- B = ( Base ` R )
	isidom3.t	|- .x. = ( .r ` R )
	isidom3.0	|- .0. = ( 0g ` R )
	isidom3.1	|- .1. = ( 1r ` R )
Assertion	isidom3	|- ( R e. IDomn <-> ( R e. CRing /\ .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isidom3.b	|- B = ( Base ` R )
2		isidom3.t	|- .x. = ( .r ` R )
3		isidom3.0	|- .0. = ( 0g ` R )
4		isidom3.1	|- .1. = ( 1r ` R )
5		isidom2	|- ( R e. IDomn <-> ( R e. PrmRing /\ R e. CRing ) )
6		eqid	|- ( PrmIdeal ` R ) = ( PrmIdeal ` R )
7	3 6	isprmrng	|- ( R e. PrmRing <-> ( R e. Ring /\ { .0. } e. ( PrmIdeal ` R ) ) )
8	1 2	isprmidlc	|- ( R e. CRing -> ( { .0. } e. ( PrmIdeal ` R ) <-> ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= B /\ A. a e. B A. b e. B ( ( a .x. b ) e. { .0. } -> ( a e. { .0. } \/ b e. { .0. } ) ) ) ) )
9		crngring	|- ( R e. CRing -> R e. Ring )
10	9	biantrurd	|- ( R e. CRing -> ( { .0. } e. ( PrmIdeal ` R ) <-> ( R e. Ring /\ { .0. } e. ( PrmIdeal ` R ) ) ) )
11		3anass	|- ( ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= B /\ A. a e. B A. b e. B ( ( a .x. b ) e. { .0. } -> ( a e. { .0. } \/ b e. { .0. } ) ) ) <-> ( { .0. } e. ( LIdeal ` R ) /\ ( { .0. } =/= B /\ A. a e. B A. b e. B ( ( a .x. b ) e. { .0. } -> ( a e. { .0. } \/ b e. { .0. } ) ) ) ) )
12		eqid	|- ( 2Ideal ` R ) = ( 2Ideal ` R )
13	12 3	2idl0	|- ( R e. Ring -> { .0. } e. ( 2Ideal ` R ) )
14	9 13	syl	|- ( R e. CRing -> { .0. } e. ( 2Ideal ` R ) )
15	14	2idllidld	|- ( R e. CRing -> { .0. } e. ( LIdeal ` R ) )
16	15	biantrurd	|- ( R e. CRing -> ( ( { .0. } =/= B /\ A. a e. B A. b e. B ( ( a .x. b ) e. { .0. } -> ( a e. { .0. } \/ b e. { .0. } ) ) ) <-> ( { .0. } e. ( LIdeal ` R ) /\ ( { .0. } =/= B /\ A. a e. B A. b e. B ( ( a .x. b ) e. { .0. } -> ( a e. { .0. } \/ b e. { .0. } ) ) ) ) ) )
17	1 4	ringidcl	|- ( R e. Ring -> .1. e. B )
18		eleq2	|- ( { .0. } = B -> ( .1. e. { .0. } <-> .1. e. B ) )
19		elsni	|- ( .1. e. { .0. } -> .1. = .0. )
20	19	eqcomd	|- ( .1. e. { .0. } -> .0. = .1. )
21	18 20	biimtrrdi	|- ( { .0. } = B -> ( .1. e. B -> .0. = .1. ) )
22	17 21	syl5com	|- ( R e. Ring -> ( { .0. } = B -> .0. = .1. ) )
23	1 3 4	0ring01eqbi	|- ( R e. Ring -> ( B ~~ 1o <-> .1. = .0. ) )
24		eqcom	|- ( .1. = .0. <-> .0. = .1. )
25	23 24	bitrdi	|- ( R e. Ring -> ( B ~~ 1o <-> .0. = .1. ) )
26	1 3	ring0cl	|- ( R e. Ring -> .0. e. B )
27		en1eqsn	|- ( ( .0. e. B /\ B ~~ 1o ) -> B = { .0. } )
28	27	eqcomd	|- ( ( .0. e. B /\ B ~~ 1o ) -> { .0. } = B )
29	28	ex	|- ( .0. e. B -> ( B ~~ 1o -> { .0. } = B ) )
30	26 29	syl	|- ( R e. Ring -> ( B ~~ 1o -> { .0. } = B ) )
31	25 30	sylbird	|- ( R e. Ring -> ( .0. = .1. -> { .0. } = B ) )
32	22 31	impbid	|- ( R e. Ring -> ( { .0. } = B <-> .0. = .1. ) )
33	9 32	syl	|- ( R e. CRing -> ( { .0. } = B <-> .0. = .1. ) )
34	33	necon3bid	|- ( R e. CRing -> ( { .0. } =/= B <-> .0. =/= .1. ) )
35		ovex	|- ( a .x. b ) e. _V
36	35	elsn	|- ( ( a .x. b ) e. { .0. } <-> ( a .x. b ) = .0. )
37		velsn	|- ( a e. { .0. } <-> a = .0. )
38		velsn	|- ( b e. { .0. } <-> b = .0. )
39	37 38	orbi12i	|- ( ( a e. { .0. } \/ b e. { .0. } ) <-> ( a = .0. \/ b = .0. ) )
40	36 39	imbi12i	|- ( ( ( a .x. b ) e. { .0. } -> ( a e. { .0. } \/ b e. { .0. } ) ) <-> ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) )
41	40	a1i	|- ( R e. CRing -> ( ( ( a .x. b ) e. { .0. } -> ( a e. { .0. } \/ b e. { .0. } ) ) <-> ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) )
42	41	2ralbidv	|- ( R e. CRing -> ( A. a e. B A. b e. B ( ( a .x. b ) e. { .0. } -> ( a e. { .0. } \/ b e. { .0. } ) ) <-> A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) )
43	34 42	anbi12d	|- ( R e. CRing -> ( ( { .0. } =/= B /\ A. a e. B A. b e. B ( ( a .x. b ) e. { .0. } -> ( a e. { .0. } \/ b e. { .0. } ) ) ) <-> ( .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) )
44	16 43	bitr3d	|- ( R e. CRing -> ( ( { .0. } e. ( LIdeal ` R ) /\ ( { .0. } =/= B /\ A. a e. B A. b e. B ( ( a .x. b ) e. { .0. } -> ( a e. { .0. } \/ b e. { .0. } ) ) ) ) <-> ( .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) )
45	11 44	bitrid	|- ( R e. CRing -> ( ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= B /\ A. a e. B A. b e. B ( ( a .x. b ) e. { .0. } -> ( a e. { .0. } \/ b e. { .0. } ) ) ) <-> ( .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) )
46	8 10 45	3bitr3d	|- ( R e. CRing -> ( ( R e. Ring /\ { .0. } e. ( PrmIdeal ` R ) ) <-> ( .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) )
47	7 46	bitrid	|- ( R e. CRing -> ( R e. PrmRing <-> ( .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) )
48	47	pm5.32i	|- ( ( R e. CRing /\ R e. PrmRing ) <-> ( R e. CRing /\ ( .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) )
49		ancom	|- ( ( R e. PrmRing /\ R e. CRing ) <-> ( R e. CRing /\ R e. PrmRing ) )
50		3anass	|- ( ( R e. CRing /\ .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) <-> ( R e. CRing /\ ( .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) )
51	48 49 50	3bitr4i	|- ( ( R e. PrmRing /\ R e. CRing ) <-> ( R e. CRing /\ .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) )
52	5 51	bitri	|- ( R e. IDomn <-> ( R e. CRing /\ .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) )