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

Metamath Proof Explorer

Theorem domnlcanOLD

Description: Obsolete version of domnlcan 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 )
domnlcanOLD.r 
|- ( ph -> R e. Domn )
domnlcanOLD.2 
|- ( ph -> ( X .x. Y ) = ( X .x. Z ) )
Assertion domnlcanOLD 
|- ( 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 domnlcanOLD.r 
 |-  ( ph -> R e. Domn )
8 domnlcanOLD.2 
 |-  ( ph -> ( X .x. Y ) = ( X .x. Z ) )
9 oveq1 
 |-  ( a = X -> ( a .x. b ) = ( X .x. b ) )
10 oveq1 
 |-  ( a = X -> ( a .x. c ) = ( X .x. c ) )
11 9 10 eqeq12d 
 |-  ( a = X -> ( ( a .x. b ) = ( a .x. c ) <-> ( X .x. b ) = ( X .x. c ) ) )
12 11 imbi1d 
 |-  ( a = X -> ( ( ( a .x. b ) = ( a .x. c ) -> b = c ) <-> ( ( X .x. b ) = ( X .x. c ) -> b = c ) ) )
13 oveq2 
 |-  ( b = Y -> ( X .x. b ) = ( X .x. Y ) )
14 13 eqeq1d 
 |-  ( b = Y -> ( ( X .x. b ) = ( X .x. c ) <-> ( X .x. Y ) = ( X .x. c ) ) )
15 eqeq1 
 |-  ( b = Y -> ( b = c <-> Y = c ) )
16 14 15 imbi12d 
 |-  ( b = Y -> ( ( ( X .x. b ) = ( X .x. c ) -> b = c ) <-> ( ( X .x. Y ) = ( X .x. c ) -> Y = c ) ) )
17 oveq2 
 |-  ( c = Z -> ( X .x. c ) = ( X .x. Z ) )
18 17 eqeq2d 
 |-  ( c = Z -> ( ( X .x. Y ) = ( X .x. c ) <-> ( X .x. Y ) = ( X .x. Z ) ) )
19 eqeq2 
 |-  ( c = Z -> ( Y = c <-> Y = Z ) )
20 18 19 imbi12d 
 |-  ( c = Z -> ( ( ( X .x. Y ) = ( X .x. c ) -> Y = c ) <-> ( ( X .x. Y ) = ( X .x. Z ) -> Y = Z ) ) )
21 1 2 3 isdomn4 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) ) )
22 7 21 sylib 
 |-  ( ph -> ( R e. NzRing /\ A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) ) )
23 22 simprd 
 |-  ( ph -> A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) )
24 12 16 20 23 4 5 6 rspc3dv 
 |-  ( ph -> ( ( X .x. Y ) = ( X .x. Z ) -> Y = Z ) )
25 8 24 mpd 
 |-  ( ph -> Y = Z )