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

Metamath Proof Explorer

Theorem idomrcanOLD

Description: Obsolete version of idomrcan 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$
		idomrcanOLD.r	$⊢ φ \to R \in IDomn$
		idomrcanOLD.2	$⊢ φ \to Y \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} X$
	Assertion	idomrcanOLD	$⊢ φ \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		idomrcanOLD.r	$⊢ φ \to R \in IDomn$
8		idomrcanOLD.2	$⊢ φ \to Y \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} X$
9	7	idomdomd	$⊢ φ \to R \in Domn$
10		df-idom	$⊢ IDomn = CRing \cap Domn$
11	7 10	eleqtrdi	$⊢ φ \to R \in (CRing \cap Domn)$
12	11	elin1d	$⊢ φ \to R \in CRing$
13	4	eldifad	$⊢ φ \to X \in B$
14	1 3	crngcom	$⊢ (R \in CRing \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y = Y \underset{˙}{\cdot} X$
15	12 13 5 14	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Y = Y \underset{˙}{\cdot} X$
16	1 3	crngcom	$⊢ (R \in CRing \land X \in B \land Z \in B) \to X \underset{˙}{\cdot} Z = Z \underset{˙}{\cdot} X$
17	12 13 6 16	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Z = Z \underset{˙}{\cdot} X$
18	8 15 17	3eqtr4d	$⊢ φ \to X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z$
19	1 2 3 4 5 6 9 18	domnlcan	$⊢ φ \to Y = Z$