domnlcanOLD

Description: Obsolete version of domnlcan as of 21-Jun-2025. (Contributed by Thierry Arnoux, 22-Mar-2025) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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

Metamath Proof Explorer

Theorem domnlcanOLD

Proof