Theorem domnlcan

Description: Left-cancellation law for domains. (Contributed by Thierry Arnoux, 22-Mar-2025) (Proof shortened by SN, 21-Jun-2025)

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

Proof

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