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

Metamath Proof Explorer

Theorem domnlcanb

Description: Left-cancellation law for domains, biconditional version of domnlcan . (Contributed by Thierry Arnoux, 8-Jun-2025) Shorten this theorem and domnlcan overall. (Revised 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 )
Assertion domnlcanb 
|- ( ph -> ( ( X .x. Y ) = ( X .x. Z ) <-> 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 oveq1 
 |-  ( a = X -> ( a .x. b ) = ( X .x. b ) )
9 oveq1 
 |-  ( a = X -> ( a .x. c ) = ( X .x. c ) )
10 8 9 eqeq12d 
 |-  ( a = X -> ( ( a .x. b ) = ( a .x. c ) <-> ( X .x. b ) = ( X .x. c ) ) )
11 10 imbi1d 
 |-  ( a = X -> ( ( ( a .x. b ) = ( a .x. c ) -> b = c ) <-> ( ( X .x. b ) = ( X .x. c ) -> b = c ) ) )
12 oveq2 
 |-  ( b = Y -> ( X .x. b ) = ( X .x. Y ) )
13 12 eqeq1d 
 |-  ( b = Y -> ( ( X .x. b ) = ( X .x. c ) <-> ( X .x. Y ) = ( X .x. c ) ) )
14 eqeq1 
 |-  ( b = Y -> ( b = c <-> Y = c ) )
15 13 14 imbi12d 
 |-  ( b = Y -> ( ( ( X .x. b ) = ( X .x. c ) -> b = c ) <-> ( ( X .x. Y ) = ( X .x. c ) -> Y = c ) ) )
16 oveq2 
 |-  ( c = Z -> ( X .x. c ) = ( X .x. Z ) )
17 16 eqeq2d 
 |-  ( c = Z -> ( ( X .x. Y ) = ( X .x. c ) <-> ( X .x. Y ) = ( X .x. Z ) ) )
18 eqeq2 
 |-  ( c = Z -> ( Y = c <-> Y = Z ) )
19 17 18 imbi12d 
 |-  ( c = Z -> ( ( ( X .x. Y ) = ( X .x. c ) -> Y = c ) <-> ( ( X .x. Y ) = ( X .x. Z ) -> Y = Z ) ) )
20 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 ) ) )
21 7 20 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 ) ) )
22 21 simprd 
 |-  ( ph -> A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) )
23 11 15 19 22 4 5 6 rspc3dv 
 |-  ( ph -> ( ( X .x. Y ) = ( X .x. Z ) -> Y = Z ) )
24 oveq2 
 |-  ( Y = Z -> ( X .x. Y ) = ( X .x. Z ) )
25 23 24 impbid1 
 |-  ( ph -> ( ( X .x. Y ) = ( X .x. Z ) <-> Y = Z ) )