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

Metamath Proof Explorer

Theorem drngmulrcan

Description: Cancellation of a nonzero factor on the right for multiplication. ( mulcan2ad analog). (Contributed by SN, 14-Aug-2024) (Proof shortened by SN, 25-Jun-2025)

		Ref	Expression
	Hypotheses	drngmullcan.b	$⊢ B = {Base}_{R}$
		drngmullcan.0	$⊢ \underset{˙}{0} = 0_{R}$
		drngmullcan.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		drngmullcan.r	$⊢ φ \to R \in DivRing$
		drngmullcan.x	$⊢ φ \to X \in B$
		drngmullcan.y	$⊢ φ \to Y \in B$
		drngmullcan.z	$⊢ φ \to Z \in B$
		drngmullcan.1	$⊢ φ \to Z \neq \underset{˙}{0}$
		drngmulrcan.2	$⊢ φ \to X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z$
	Assertion	drngmulrcan	$⊢ φ \to X = Y$

Proof

Step	Hyp	Ref	Expression
1		drngmullcan.b	$⊢ B = {Base}_{R}$
2		drngmullcan.0	$⊢ \underset{˙}{0} = 0_{R}$
3		drngmullcan.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		drngmullcan.r	$⊢ φ \to R \in DivRing$
5		drngmullcan.x	$⊢ φ \to X \in B$
6		drngmullcan.y	$⊢ φ \to Y \in B$
7		drngmullcan.z	$⊢ φ \to Z \in B$
8		drngmullcan.1	$⊢ φ \to Z \neq \underset{˙}{0}$
9		drngmulrcan.2	$⊢ φ \to X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z$
10	7 8	eldifsnd	$⊢ φ \to Z \in (B ∖ \{\underset{˙}{0}\})$
11		drngdomn	$⊢ R \in DivRing \to R \in Domn$
12	4 11	syl	$⊢ φ \to R \in Domn$
13	1 2 3 5 6 10 12 9	domnrcan	$⊢ φ \to X = Y$