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

Metamath Proof Explorer

Theorem domnlcanbOLD

Description: Obsolete version of domnlcanb as of 21-Jun-2025. (Contributed by Thierry Arnoux, 8-Jun-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$
		domnlcanbOLD.r	$⊢ φ \to R \in Domn$
	Assertion	domnlcanbOLD	$⊢ φ \to (X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z \leftrightarrow 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		domnlcanbOLD.r	$⊢ φ \to R \in Domn$
8	4	adantr	$⊢ (φ \land X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z) \to X \in (B ∖ \{\underset{˙}{0}\})$
9	5	adantr	$⊢ (φ \land X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z) \to Y \in B$
10	6	adantr	$⊢ (φ \land X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z) \to Z \in B$
11	7	adantr	$⊢ (φ \land X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z) \to R \in Domn$
12		simpr	$⊢ (φ \land X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z) \to X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z$
13	1 2 3 8 9 10 11 12	domnlcan	$⊢ (φ \land X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z) \to Y = Z$
14		simpr	$⊢ (φ \land Y = Z) \to Y = Z$
15	14	oveq2d	$⊢ (φ \land Y = Z) \to X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z$
16	13 15	impbida	$⊢ φ \to (X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Z \leftrightarrow Y = Z)$