Theorem idomrcanOLD

Description: Obsolete version of idomrcan as of 21-Jun-2025. (Contributed by Thierry Arnoux, 22-Mar-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 )
	idomrcanOLD.r	|- ( ph -> R e. IDomn )
	idomrcanOLD.2	|- ( ph -> ( Y .x. X ) = ( Z .x. X ) )
Assertion	idomrcanOLD	|- ( ph -> 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		idomrcanOLD.r	|- ( ph -> R e. IDomn )
8		idomrcanOLD.2	|- ( ph -> ( Y .x. X ) = ( Z .x. X ) )
9	7	idomdomd	|- ( ph -> R e. Domn )
10		df-idom	|- IDomn = ( CRing i^i Domn )
11	7 10	eleqtrdi	|- ( ph -> R e. ( CRing i^i Domn ) )
12	11	elin1d	|- ( ph -> R e. CRing )
13	4	eldifad	|- ( ph -> X e. B )
14	1 3	crngcom	|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) = ( Y .x. X ) )
15	12 13 5 14	syl3anc	|- ( ph -> ( X .x. Y ) = ( Y .x. X ) )
16	1 3	crngcom	|- ( ( R e. CRing /\ X e. B /\ Z e. B ) -> ( X .x. Z ) = ( Z .x. X ) )
17	12 13 6 16	syl3anc	|- ( ph -> ( X .x. Z ) = ( Z .x. X ) )
18	8 15 17	3eqtr4d	|- ( ph -> ( X .x. Y ) = ( X .x. Z ) )
19	1 2 3 4 5 6 9 18	domnlcan	|- ( ph -> Y = Z )