Metamath Proof Explorer

Theorem idomcanr

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	idomcanr	$⊢ ((R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \land Z \neq \underset{˙}{0}) \to (X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z \to X = Y)$

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		isidom	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in Domn)$
5	4	simplbi	$⊢ R \in IDomn \to R \in CRing$
6	1 2	crngcom	$⊢ (R \in CRing \land X \in B \land Z \in B) \to X \underset{˙}{\cdot} Z = Z \underset{˙}{\cdot} X$
7	6	3adant3r2	$⊢ (R \in CRing \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\cdot} Z = Z \underset{˙}{\cdot} X$
8	1 2	crngcom	$⊢ (R \in CRing \land Y \in B \land Z \in B) \to Y \underset{˙}{\cdot} Z = Z \underset{˙}{\cdot} Y$
9	8	3adant3r1	$⊢ (R \in CRing \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{\cdot} Z = Z \underset{˙}{\cdot} Y$
10	7 9	eqeq12d	$⊢ (R \in CRing \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z \leftrightarrow Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y)$
11	5 10	sylan	$⊢ (R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z \leftrightarrow Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y)$
12	11	adantr	$⊢ ((R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \land Z \neq \underset{˙}{0}) \to (X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z \leftrightarrow Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y)$
13		3anrot	$⊢ (Z \in B \land X \in B \land Y \in B) \leftrightarrow (X \in B \land Y \in B \land Z \in B)$
14	13	biimpri	$⊢ (X \in B \land Y \in B \land Z \in B) \to (Z \in B \land X \in B \land Y \in B)$
15	1 2 3	idomcanl	$⊢ ((R \in IDomn \land (Z \in B \land X \in B \land Y \in B)) \land Z \neq \underset{˙}{0}) \to (Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y \to X = Y)$
16	14 15	sylanl2	$⊢ ((R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \land Z \neq \underset{˙}{0}) \to (Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y \to X = Y)$
17	12 16	sylbid	$⊢ ((R \in IDomn \land (X \in B \land Y \in B \land Z \in B)) \land Z \neq \underset{˙}{0}) \to (X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z \to X = Y)$