isdomn4

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

	Ref	Expression
Hypotheses	isdomn4.b	$⊢ B = {Base}_{R}$
	isdomn4.0	$⊢ \underset{˙}{0} = 0_{R}$
	isdomn4.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	isdomn4	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land \forall a \in (B ∖ \{\underset{˙}{0}\}) \forall b \in B \forall c \in B (a \underset{˙}{\cdot} b = a \underset{˙}{\cdot} c \to b = c))$

Proof

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

Metamath Proof Explorer

Theorem isdomn4

Proof