This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )