This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idomrcan

Description: Right-cancellation law for integral domains. (Contributed by Thierry Arnoux, 22-Mar-2025) (Proof shortened by SN, 21-Jun-2025)

	Ref	Expression
Hypotheses	idomrcan.b	$⊢ B = {Base}_{R}$
	idomrcan.0	$⊢ \underset{˙}{0} = 0_{R}$
	idomrcan.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	idomrcan.x	$⊢ φ \to X \in B$
	idomrcan.y	$⊢ φ \to Y \in B$
	idomrcan.z	$⊢ φ \to Z \in (B ∖ \{\underset{˙}{0}\})$
	idomrcan.r	$⊢ φ \to R \in IDomn$
	idomrcan.1	$⊢ φ \to X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z$
Assertion	idomrcan	$⊢ φ \to X = Y$

Step	Hyp	Ref	Expression
1		idomrcan.b	$⊢ B = {Base}_{R}$
2		idomrcan.0	$⊢ \underset{˙}{0} = 0_{R}$
3		idomrcan.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		idomrcan.x	$⊢ φ \to X \in B$
5		idomrcan.y	$⊢ φ \to Y \in B$
6		idomrcan.z	$⊢ φ \to Z \in (B ∖ \{\underset{˙}{0}\})$
7		idomrcan.r	$⊢ φ \to R \in IDomn$
8		idomrcan.1	$⊢ φ \to X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z$
9	7	idomdomd	$⊢ φ \to R \in Domn$
10	1 2 3 4 5 6 9 8	domnrcan	$⊢ φ \to X = Y$