Theorem domnlcanbOLD

Description: Obsolete version of domnlcanb as of 21-Jun-2025. (Contributed by Thierry Arnoux, 8-Jun-2025) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		domncanOLD.b	|- B = ( Base ` R )
2		domncanOLD.1	|- .0. = ( 0g ` R )
3		domncanOLD.m	|- .x. = ( .r ` R )
4		domncanOLD.x	|- ( ph -> X e. ( B \ { .0. } ) )
5		domncanOLD.y	|- ( ph -> Y e. B )
6		domncanOLD.z	|- ( ph -> Z e. B )
7		domnlcanbOLD.r	|- ( ph -> R e. Domn )
8	4	adantr	|- ( ( ph /\ ( X .x. Y ) = ( X .x. Z ) ) -> X e. ( B \ { .0. } ) )
9	5	adantr	|- ( ( ph /\ ( X .x. Y ) = ( X .x. Z ) ) -> Y e. B )
10	6	adantr	|- ( ( ph /\ ( X .x. Y ) = ( X .x. Z ) ) -> Z e. B )
11	7	adantr	|- ( ( ph /\ ( X .x. Y ) = ( X .x. Z ) ) -> R e. Domn )
12		simpr	|- ( ( ph /\ ( X .x. Y ) = ( X .x. Z ) ) -> ( X .x. Y ) = ( X .x. Z ) )
13	1 2 3 8 9 10 11 12	domnlcan	|- ( ( ph /\ ( X .x. Y ) = ( X .x. Z ) ) -> Y = Z )
14		simpr	|- ( ( ph /\ Y = Z ) -> Y = Z )
15	14	oveq2d	|- ( ( ph /\ Y = Z ) -> ( X .x. Y ) = ( X .x. Z ) )
16	13 15	impbida	|- ( ph -> ( ( X .x. Y ) = ( X .x. Z ) <-> Y = Z ) )