Theorem drngmullcan

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

	Ref	Expression
Hypotheses	drngmullcan.b	|- B = ( Base ` R )
	drngmullcan.0	|- .0. = ( 0g ` R )
	drngmullcan.t	|- .x. = ( .r ` R )
	drngmullcan.r	|- ( ph -> R e. DivRing )
	drngmullcan.x	|- ( ph -> X e. B )
	drngmullcan.y	|- ( ph -> Y e. B )
	drngmullcan.z	|- ( ph -> Z e. B )
	drngmullcan.1	|- ( ph -> Z =/= .0. )
	drngmullcan.2	|- ( ph -> ( Z .x. X ) = ( Z .x. Y ) )
Assertion	drngmullcan	|- ( ph -> X = Y )

Proof

Step	Hyp	Ref	Expression
1		drngmullcan.b	|- B = ( Base ` R )
2		drngmullcan.0	|- .0. = ( 0g ` R )
3		drngmullcan.t	|- .x. = ( .r ` R )
4		drngmullcan.r	|- ( ph -> R e. DivRing )
5		drngmullcan.x	|- ( ph -> X e. B )
6		drngmullcan.y	|- ( ph -> Y e. B )
7		drngmullcan.z	|- ( ph -> Z e. B )
8		drngmullcan.1	|- ( ph -> Z =/= .0. )
9		drngmullcan.2	|- ( ph -> ( Z .x. X ) = ( Z .x. Y ) )
10	7 8	eldifsnd	|- ( ph -> Z e. ( B \ { .0. } ) )
11		drngdomn	|- ( R e. DivRing -> R e. Domn )
12	4 11	syl	|- ( ph -> R e. Domn )
13	1 2 3 10 5 6 12 9	domnlcan	|- ( ph -> X = Y )