domnlcanb

Description: Left-cancellation law for domains, biconditional version of domnlcan . (Contributed by Thierry Arnoux, 8-Jun-2025) Shorten this theorem and domnlcan overall. (Revised by SN, 21-Jun-2025)

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

Proof

Step	Hyp	Ref	Expression
1		domncan.b	$⊢ B = {Base}_{R}$
2		domncan.0	$⊢ \underset{˙}{0} = 0_{R}$
3		domncan.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		domncan.x	$⊢ φ \to X \in (B ∖ \{\underset{˙}{0}\})$
5		domncan.y	$⊢ φ \to Y \in B$
6		domncan.z	$⊢ φ \to Z \in B$
7		domncan.r	$⊢ φ \to R \in Domn$
8		oveq1	$⊢ a = X \to a \underset{˙}{\cdot} b = X \underset{˙}{\cdot} b$
9		oveq1	$⊢ a = X \to a \underset{˙}{\cdot} c = X \underset{˙}{\cdot} c$
10	8 9	eqeq12d	$⊢ a = X \to (a \underset{˙}{\cdot} b = a \underset{˙}{\cdot} c \leftrightarrow X \underset{˙}{\cdot} b = X \underset{˙}{\cdot} c)$
11	10	imbi1d	$⊢ a = X \to ((a \underset{˙}{\cdot} b = a \underset{˙}{\cdot} c \to b = c) \leftrightarrow (X \underset{˙}{\cdot} b = X \underset{˙}{\cdot} c \to b = c))$
12		oveq2	$⊢ b = Y \to X \underset{˙}{\cdot} b = X \underset{˙}{\cdot} Y$
13	12	eqeq1d	$⊢ b = Y \to (X \underset{˙}{\cdot} b = X \underset{˙}{\cdot} c \leftrightarrow X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} c)$
14		eqeq1	$⊢ b = Y \to (b = c \leftrightarrow Y = c)$
15	13 14	imbi12d	$⊢ b = Y \to ((X \underset{˙}{\cdot} b = X \underset{˙}{\cdot} c \to b = c) \leftrightarrow (X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} c \to Y = c))$
16		oveq2	$⊢ c = Z \to X \underset{˙}{\cdot} c = X \underset{˙}{\cdot} Z$
17	16	eqeq2d	$⊢ c = Z \to (X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} c \leftrightarrow X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z)$
18		eqeq2	$⊢ c = Z \to (Y = c \leftrightarrow Y = Z)$
19	17 18	imbi12d	$⊢ c = Z \to ((X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} c \to Y = c) \leftrightarrow (X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z \to Y = Z))$
20	1 2 3	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))$
21	7 20	sylib	$⊢ φ \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))$
22	21	simprd	$⊢ φ \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)$
23	11 15 19 22 4 5 6	rspc3dv	$⊢ φ \to (X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z \to Y = Z)$
24		oveq2	$⊢ Y = Z \to X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z$
25	23 24	impbid1	$⊢ φ \to (X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z \leftrightarrow Y = Z)$

Metamath Proof Explorer

Theorem domnlcanb

Proof