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	|- .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. )
	drngmulrcan.2	|- ( ph -> ( X .x. Z ) = ( Y .x. Z ) )
Assertion	drngmulrcan	|- ( 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		drngmulrcan.2	|- ( ph -> ( X .x. Z ) = ( Y .x. Z ) )
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 5 6 10 12 9	domnrcan	|- ( ph -> X = Y )