idomcanl

Description: Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by AV, 13-Jul-2026)

	Ref	Expression
Hypotheses	isidom3.b	$⊢ B = {Base}_{R}$
	isidom3.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	isidom3.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	idomcanl	$⊢ ((R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \land X \neq \underset{˙}{0}) \to (X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z \to Y = Z)$

Proof

Step	Hyp	Ref	Expression
1		isidom3.b	$⊢ B = {Base}_{R}$
2		isidom3.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		isidom3.0	$⊢ \underset{˙}{0} = 0_{R}$
4		eqid	$⊢ -_{R} = -_{R}$
5		isidom	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in Domn)$
6		crngring	$⊢ R \in CRing \to R \in Ring$
7	6	adantr	$⊢ (R \in CRing \land R \in Domn) \to R \in Ring$
8	5 7	sylbi	$⊢ R \in IDomn \to R \in Ring$
9	8	adantr	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to R \in Ring$
10		simpr1	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
11		simpr2	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
12		simpr3	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
13	1 2 4 9 10 11 12	ringsubdi	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\cdot} (Y -_{R} Z) = (X \underset{˙}{\cdot} Y) -_{R} (X \underset{˙}{\cdot} Z)$
14	13	adantr	$⊢ ((R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \land X \neq \underset{˙}{0}) \to X \underset{˙}{\cdot} (Y -_{R} Z) = (X \underset{˙}{\cdot} Y) -_{R} (X \underset{˙}{\cdot} Z)$
15	14	eqeq1d	$⊢ ((R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \land X \neq \underset{˙}{0}) \to (X \underset{˙}{\cdot} (Y -_{R} Z) = \underset{˙}{0} \leftrightarrow (X \underset{˙}{\cdot} Y) -_{R} (X \underset{˙}{\cdot} Z) = \underset{˙}{0})$
16	8	ringgrpd	$⊢ R \in IDomn \to R \in Grp$
17	1 4	grpsubcl	$⊢ (R \in Grp \land Y \in B \land Z \in B) \to Y -_{R} Z \in B$
18	17	3expb	$⊢ (R \in Grp \land (Y \in B \land Z \in B)) \to Y -_{R} Z \in B$
19	16 18	sylan	$⊢ (R \in IDomn \land (Y \in B \land Z \in B)) \to Y -_{R} Z \in B$
20	19	adantlr	$⊢ ((R \in IDomn \land X \in B) \land (Y \in B \land Z \in B)) \to Y -_{R} Z \in B$
21	1 2 3	idomnzd	$⊢ (R \in IDomn \land (X \in B \land Y -_{R} Z \in B \land X \underset{˙}{\cdot} (Y -_{R} Z) = \underset{˙}{0})) \to (X = \underset{˙}{0} \lor Y -_{R} Z = \underset{˙}{0})$
22	21	3exp2	$⊢ R \in IDomn \to (X \in B \to (Y -_{R} Z \in B \to (X \underset{˙}{\cdot} (Y -_{R} Z) = \underset{˙}{0} \to (X = \underset{˙}{0} \lor Y -_{R} Z = \underset{˙}{0}))))$
23	22	imp31	$⊢ ((R \in IDomn \land X \in B) \land Y -_{R} Z \in B) \to (X \underset{˙}{\cdot} (Y -_{R} Z) = \underset{˙}{0} \to (X = \underset{˙}{0} \lor Y -_{R} Z = \underset{˙}{0}))$
24	20 23	syldan	$⊢ ((R \in IDomn \land X \in B) \land (Y \in B \land Z \in B)) \to (X \underset{˙}{\cdot} (Y -_{R} Z) = \underset{˙}{0} \to (X = \underset{˙}{0} \lor Y -_{R} Z = \underset{˙}{0}))$
25	24	exp43	$⊢ R \in IDomn \to (X \in B \to (Y \in B \to (Z \in B \to (X \underset{˙}{\cdot} (Y -_{R} Z) = \underset{˙}{0} \to (X = \underset{˙}{0} \lor Y -_{R} Z = \underset{˙}{0})))))$
26	25	3imp2	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\cdot} (Y -_{R} Z) = \underset{˙}{0} \to (X = \underset{˙}{0} \lor Y -_{R} Z = \underset{˙}{0}))$
27		neor	$⊢ (X = \underset{˙}{0} \lor Y -_{R} Z = \underset{˙}{0}) \leftrightarrow (X \neq \underset{˙}{0} \to Y -_{R} Z = \underset{˙}{0})$
28	26 27	imbitrdi	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\cdot} (Y -_{R} Z) = \underset{˙}{0} \to (X \neq \underset{˙}{0} \to Y -_{R} Z = \underset{˙}{0}))$
29	28	com23	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to (X \neq \underset{˙}{0} \to (X \underset{˙}{\cdot} (Y -_{R} Z) = \underset{˙}{0} \to Y -_{R} Z = \underset{˙}{0}))$
30	29	imp	$⊢ ((R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \land X \neq \underset{˙}{0}) \to (X \underset{˙}{\cdot} (Y -_{R} Z) = \underset{˙}{0} \to Y -_{R} Z = \underset{˙}{0})$
31	15 30	sylbird	$⊢ ((R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \land X \neq \underset{˙}{0}) \to ((X \underset{˙}{\cdot} Y) -_{R} (X \underset{˙}{\cdot} Z) = \underset{˙}{0} \to Y -_{R} Z = \underset{˙}{0})$
32	16	adantr	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to R \in Grp$
33	1 2 9 10 11	ringcld	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\cdot} Y \in B$
34	1 2 9 10 12	ringcld	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\cdot} Z \in B$
35	1 3 4	grpsubeq0	$⊢ (R \in Grp \land X \underset{˙}{\cdot} Y \in B \land X \underset{˙}{\cdot} Z \in B) \to ((X \underset{˙}{\cdot} Y) -_{R} (X \underset{˙}{\cdot} Z) = \underset{˙}{0} \leftrightarrow X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z)$
36	35	bicomd	$⊢ (R \in Grp \land X \underset{˙}{\cdot} Y \in B \land X \underset{˙}{\cdot} Z \in B) \to (X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z \leftrightarrow (X \underset{˙}{\cdot} Y) -_{R} (X \underset{˙}{\cdot} Z) = \underset{˙}{0})$
37	32 33 34 36	syl3anc	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z \leftrightarrow (X \underset{˙}{\cdot} Y) -_{R} (X \underset{˙}{\cdot} Z) = \underset{˙}{0})$
38	37	adantr	$⊢ ((R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \land X \neq \underset{˙}{0}) \to (X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z \leftrightarrow (X \underset{˙}{\cdot} Y) -_{R} (X \underset{˙}{\cdot} Z) = \underset{˙}{0})$
39	1 3 4	grpsubeq0	$⊢ (R \in Grp \land Y \in B \land Z \in B) \to (Y -_{R} Z = \underset{˙}{0} \leftrightarrow Y = Z)$
40	39	bicomd	$⊢ (R \in Grp \land Y \in B \land Z \in B) \to (Y = Z \leftrightarrow Y -_{R} Z = \underset{˙}{0})$
41	40	3expb	$⊢ (R \in Grp \land (Y \in B \land Z \in B)) \to (Y = Z \leftrightarrow Y -_{R} Z = \underset{˙}{0})$
42	16 41	sylan	$⊢ (R \in IDomn \land (Y \in B \land Z \in B)) \to (Y = Z \leftrightarrow Y -_{R} Z = \underset{˙}{0})$
43	42	3adantr1	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to (Y = Z \leftrightarrow Y -_{R} Z = \underset{˙}{0})$
44	43	adantr	$⊢ ((R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \land X \neq \underset{˙}{0}) \to (Y = Z \leftrightarrow Y -_{R} Z = \underset{˙}{0})$
45	31 38 44	3imtr4d	$⊢ ((R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \land X \neq \underset{˙}{0}) \to (X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z \to Y = Z)$

Metamath Proof Explorer

Theorem idomcanl

Proof