Theorem domnrcan

Description: Right-cancellation law for domains. (Contributed by SN, 21-Jun-2025)

	Ref	Expression
Hypotheses	domnrcan.b	|- B = ( Base ` R )
	domnrcan.0	|- .0. = ( 0g ` R )
	domnrcan.m	|- .x. = ( .r ` R )
	domnrcan.x	|- ( ph -> X e. B )
	domnrcan.y	|- ( ph -> Y e. B )
	domnrcan.z	|- ( ph -> Z e. ( B \ { .0. } ) )
	domnrcan.r	|- ( ph -> R e. Domn )
	domnrcan.1	|- ( ph -> ( X .x. Z ) = ( Y .x. Z ) )
Assertion	domnrcan	|- ( ph -> X = Y )

Proof

Step	Hyp	Ref	Expression
1		domnrcan.b	|- B = ( Base ` R )
2		domnrcan.0	|- .0. = ( 0g ` R )
3		domnrcan.m	|- .x. = ( .r ` R )
4		domnrcan.x	|- ( ph -> X e. B )
5		domnrcan.y	|- ( ph -> Y e. B )
6		domnrcan.z	|- ( ph -> Z e. ( B \ { .0. } ) )
7		domnrcan.r	|- ( ph -> R e. Domn )
8		domnrcan.1	|- ( ph -> ( X .x. Z ) = ( Y .x. Z ) )
9	1 2 3 4 5 6 7	domnrcanb	|- ( ph -> ( ( X .x. Z ) = ( Y .x. Z ) <-> X = Y ) )
10	8 9	mpbid	|- ( ph -> X = Y )