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

Metamath Proof Explorer

Theorem domnrcanb

Description: Right-cancellation law for domains, biconditional version of domnrcan . (Contributed by SN, 21-Jun-2025)

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

Proof

Step Hyp Ref Expression
1 domnrcan.b 
 |-  B = ( Base ` R )
2 domnrcan.0 
 |-  .0. = ( 0g ` R )
3 domnrcan.m 
 |-  .x. = ( .r ` R )
4 domnrcan.x 
 |-  ( ph -> X e. B )
5 domnrcan.y 
 |-  ( ph -> Y e. B )
6 domnrcan.z 
 |-  ( ph -> Z e. ( B \ { .0. } ) )
7 domnrcan.r 
 |-  ( ph -> R e. Domn )
8 oveq1 
 |-  ( a = X -> ( a .x. c ) = ( X .x. c ) )
9 8 eqeq1d 
 |-  ( a = X -> ( ( a .x. c ) = ( b .x. c ) <-> ( X .x. c ) = ( b .x. c ) ) )
10 eqeq1 
 |-  ( a = X -> ( a = b <-> X = b ) )
11 9 10 imbi12d 
 |-  ( a = X -> ( ( ( a .x. c ) = ( b .x. c ) -> a = b ) <-> ( ( X .x. c ) = ( b .x. c ) -> X = b ) ) )
12 oveq1 
 |-  ( b = Y -> ( b .x. c ) = ( Y .x. c ) )
13 12 eqeq2d 
 |-  ( b = Y -> ( ( X .x. c ) = ( b .x. c ) <-> ( X .x. c ) = ( Y .x. c ) ) )
14 eqeq2 
 |-  ( b = Y -> ( X = b <-> X = Y ) )
15 13 14 imbi12d 
 |-  ( b = Y -> ( ( ( X .x. c ) = ( b .x. c ) -> X = b ) <-> ( ( X .x. c ) = ( Y .x. c ) -> X = Y ) ) )
16 oveq2 
 |-  ( c = Z -> ( X .x. c ) = ( X .x. Z ) )
17 oveq2 
 |-  ( c = Z -> ( Y .x. c ) = ( Y .x. Z ) )
18 16 17 eqeq12d 
 |-  ( c = Z -> ( ( X .x. c ) = ( Y .x. c ) <-> ( X .x. Z ) = ( Y .x. Z ) ) )
19 18 imbi1d 
 |-  ( c = Z -> ( ( ( X .x. c ) = ( Y .x. c ) -> X = Y ) <-> ( ( X .x. Z ) = ( Y .x. Z ) -> X = Y ) ) )
20 1 2 3 isdomn4r 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A. a e. B A. b e. B A. c e. ( B \ { .0. } ) ( ( a .x. c ) = ( b .x. c ) -> a = b ) ) )
21 7 20 sylib 
 |-  ( ph -> ( R e. NzRing /\ A. a e. B A. b e. B A. c e. ( B \ { .0. } ) ( ( a .x. c ) = ( b .x. c ) -> a = b ) ) )
22 21 simprd 
 |-  ( ph -> A. a e. B A. b e. B A. c e. ( B \ { .0. } ) ( ( a .x. c ) = ( b .x. c ) -> a = b ) )
23 11 15 19 22 4 5 6 rspc3dv 
 |-  ( ph -> ( ( X .x. Z ) = ( Y .x. Z ) -> X = Y ) )
24 oveq1 
 |-  ( X = Y -> ( X .x. Z ) = ( Y .x. Z ) )
25 23 24 impbid1 
 |-  ( ph -> ( ( X .x. Z ) = ( Y .x. Z ) <-> X = Y ) )