Theorem isdomn4

Description: A ring is a domain iff it is nonzero and the cancellation law for multiplication holds. (Contributed by SN, 15-Sep-2024)

	Ref	Expression
Hypotheses	isdomn4.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isdomn4.0	⊢ 0 = ( 0g ‘ 𝑅 )
	isdomn4.x	⊢ · = ( .r ‘ 𝑅 )
Assertion	isdomn4	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isdomn4.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isdomn4.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		isdomn4.x	⊢ · = ( .r ‘ 𝑅 )
4		domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
5		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
6		domnring	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
7	6	adantr	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
8		eldifi	⊢ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) → 𝑎 ∈ 𝐵 )
9	8	3ad2ant1	⊢ ( ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
10	9	adantl	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
11		simpr2	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
12		simpr3	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑐 ∈ 𝐵 )
13	1 3 5 7 10 11 12	ringsubdi	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 · ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 · 𝑏 ) ( -g ‘ 𝑅 ) ( 𝑎 · 𝑐 ) ) )
14	13	eqeq1d	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 · ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ) = 0 ↔ ( ( 𝑎 · 𝑏 ) ( -g ‘ 𝑅 ) ( 𝑎 · 𝑐 ) ) = 0 ) )
15		simpll	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) → 𝑅 ∈ Domn )
16	10	adantr	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) → 𝑎 ∈ 𝐵 )
17		eldifsni	⊢ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) → 𝑎 ≠ 0 )
18	17	3ad2ant1	⊢ ( ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → 𝑎 ≠ 0 )
19	18	ad2antlr	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) → 𝑎 ≠ 0 )
20	6	ringgrpd	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Grp )
21	1 5	grpsubcl	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐵 )
22	20 21	syl3an1	⊢ ( ( 𝑅 ∈ Domn ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐵 )
23	22	3adant3r1	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐵 )
24	23	adantr	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐵 )
25		simpr	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 )
26	1 3 2	domnmuln0	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑎 ≠ 0 ) ∧ ( ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐵 ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) ) → ( 𝑎 · ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ) ≠ 0 )
27	15 16 19 24 25 26	syl122anc	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) → ( 𝑎 · ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ) ≠ 0 )
28	27	ex	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 → ( 𝑎 · ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ) ≠ 0 ) )
29	28	necon4d	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 · ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ) = 0 → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) = 0 ) )
30	14 29	sylbird	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( ( 𝑎 · 𝑏 ) ( -g ‘ 𝑅 ) ( 𝑎 · 𝑐 ) ) = 0 → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) = 0 ) )
31	20	adantr	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑅 ∈ Grp )
32		id	⊢ ( 𝑏 ∈ 𝐵 → 𝑏 ∈ 𝐵 )
33	1 3	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
34	6 8 32 33	syl3an	⊢ ( ( 𝑅 ∈ Domn ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
35	34	3adant3r3	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
36		id	⊢ ( 𝑐 ∈ 𝐵 → 𝑐 ∈ 𝐵 )
37	1 3	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 𝑎 · 𝑐 ) ∈ 𝐵 )
38	6 8 36 37	syl3an	⊢ ( ( 𝑅 ∈ Domn ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑎 · 𝑐 ) ∈ 𝐵 )
39	38	3adant3r2	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 · 𝑐 ) ∈ 𝐵 )
40	1 2 5	grpsubeq0	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑎 · 𝑏 ) ∈ 𝐵 ∧ ( 𝑎 · 𝑐 ) ∈ 𝐵 ) → ( ( ( 𝑎 · 𝑏 ) ( -g ‘ 𝑅 ) ( 𝑎 · 𝑐 ) ) = 0 ↔ ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) ) )
41	31 35 39 40	syl3anc	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( ( 𝑎 · 𝑏 ) ( -g ‘ 𝑅 ) ( 𝑎 · 𝑐 ) ) = 0 ↔ ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) ) )
42	1 2 5	grpsubeq0	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) = 0 ↔ 𝑏 = 𝑐 ) )
43	31 11 12 42	syl3anc	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) = 0 ↔ 𝑏 = 𝑐 ) )
44	30 41 43	3imtr3d	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) )
45	44	ralrimivvva	⊢ ( 𝑅 ∈ Domn → ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) )
46	4 45	jca	⊢ ( 𝑅 ∈ Domn → ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) ) )
47		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
48	47	ringgrpd	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Grp )
49	1 2	grpidcl	⊢ ( 𝑅 ∈ Grp → 0 ∈ 𝐵 )
50	48 49	syl	⊢ ( 𝑅 ∈ NzRing → 0 ∈ 𝐵 )
51	50	adantr	⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) ) → 0 ∈ 𝐵 )
52		oveq2	⊢ ( 𝑐 = 0 → ( 𝑎 · 𝑐 ) = ( 𝑎 · 0 ) )
53	52	eqeq2d	⊢ ( 𝑐 = 0 → ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) ↔ ( 𝑎 · 𝑏 ) = ( 𝑎 · 0 ) ) )
54		eqeq2	⊢ ( 𝑐 = 0 → ( 𝑏 = 𝑐 ↔ 𝑏 = 0 ) )
55	53 54	imbi12d	⊢ ( 𝑐 = 0 → ( ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) ↔ ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 0 ) → 𝑏 = 0 ) ) )
56	55	rspcv	⊢ ( 0 ∈ 𝐵 → ( ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) → ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 0 ) → 𝑏 = 0 ) ) )
57	51 56	syl	⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) → ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 0 ) → 𝑏 = 0 ) ) )
58	1 3 2	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 · 0 ) = 0 )
59	47 8 58	syl2an	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑎 · 0 ) = 0 )
60	59	adantrr	⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 · 0 ) = 0 )
61	60	eqeq2d	⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 0 ) ↔ ( 𝑎 · 𝑏 ) = 0 ) )
62	61	imbi1d	⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 0 ) → 𝑏 = 0 ) ↔ ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) ) )
63	57 62	sylibd	⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) → ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) ) )
64	63	ralimdvva	⊢ ( 𝑅 ∈ NzRing → ( ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) → ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) ) )
65		isdomn5	⊢ ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ↔ ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) )
66	64 65	imbitrrdi	⊢ ( 𝑅 ∈ NzRing → ( ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) )
67	66	imdistani	⊢ ( ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) ) → ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) )
68	1 3 2	isdomn	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) )
69	67 68	sylibr	⊢ ( ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) ) → 𝑅 ∈ Domn )
70	46 69	impbii	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) ) )