domnrcan

Description: Right-cancellation law for domains. (Contributed by SN, 21-Jun-2025)

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

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

Metamath Proof Explorer