Metamath Proof Explorer

Theorem drngmulcan2ad

Description: Cancellation of a nonzero factor on the right for multiplication. ( mulcan2ad analog). (Contributed by SN, 14-Aug-2024)

Ref Expression
Hypotheses drngmulcanad.b 
|- B = ( Base ` R )
drngmulcanad.0 
|- .0. = ( 0g ` R )
drngmulcanad.t 
|- .x. = ( .r ` R )
drngmulcanad.r 
|- ( ph -> R e. DivRing )
drngmulcanad.x 
|- ( ph -> X e. B )
drngmulcanad.y 
|- ( ph -> Y e. B )
drngmulcanad.z 
|- ( ph -> Z e. B )
drngmulcanad.1 
|- ( ph -> Z =/= .0. )
drngmulcan2ad.2 
|- ( ph -> ( X .x. Z ) = ( Y .x. Z ) )
Assertion drngmulcan2ad 
|- ( ph -> X = Y )

Proof

Step Hyp Ref Expression
1 drngmulcanad.b 
 |-  B = ( Base ` R )
2 drngmulcanad.0 
 |-  .0. = ( 0g ` R )
3 drngmulcanad.t 
 |-  .x. = ( .r ` R )
4 drngmulcanad.r 
 |-  ( ph -> R e. DivRing )
5 drngmulcanad.x 
 |-  ( ph -> X e. B )
6 drngmulcanad.y 
 |-  ( ph -> Y e. B )
7 drngmulcanad.z 
 |-  ( ph -> Z e. B )
8 drngmulcanad.1 
 |-  ( ph -> Z =/= .0. )
9 drngmulcan2ad.2 
 |-  ( ph -> ( X .x. Z ) = ( Y .x. Z ) )
10 9 oveq1d 
 |-  ( ph -> ( ( X .x. Z ) .x. ( ( invr ` R ) ` Z ) ) = ( ( Y .x. Z ) .x. ( ( invr ` R ) ` Z ) ) )
11 4 drngringd 
 |-  ( ph -> R e. Ring )
12 eqid 
 |-  ( invr ` R ) = ( invr ` R )
13 1 2 12 4 7 8 drnginvrcld 
 |-  ( ph -> ( ( invr ` R ) ` Z ) e. B )
14 1 3 11 5 7 13 ringassd 
 |-  ( ph -> ( ( X .x. Z ) .x. ( ( invr ` R ) ` Z ) ) = ( X .x. ( Z .x. ( ( invr ` R ) ` Z ) ) ) )
15 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
16 1 2 3 15 12 4 7 8 drnginvrrd 
 |-  ( ph -> ( Z .x. ( ( invr ` R ) ` Z ) ) = ( 1r ` R ) )
17 16 oveq2d 
 |-  ( ph -> ( X .x. ( Z .x. ( ( invr ` R ) ` Z ) ) ) = ( X .x. ( 1r ` R ) ) )
18 1 3 15 11 5 ringridmd 
 |-  ( ph -> ( X .x. ( 1r ` R ) ) = X )
19 14 17 18 3eqtrd 
 |-  ( ph -> ( ( X .x. Z ) .x. ( ( invr ` R ) ` Z ) ) = X )
20 1 3 11 6 7 13 ringassd 
 |-  ( ph -> ( ( Y .x. Z ) .x. ( ( invr ` R ) ` Z ) ) = ( Y .x. ( Z .x. ( ( invr ` R ) ` Z ) ) ) )
21 16 oveq2d 
 |-  ( ph -> ( Y .x. ( Z .x. ( ( invr ` R ) ` Z ) ) ) = ( Y .x. ( 1r ` R ) ) )
22 1 3 15 11 6 ringridmd 
 |-  ( ph -> ( Y .x. ( 1r ` R ) ) = Y )
23 20 21 22 3eqtrd 
 |-  ( ph -> ( ( Y .x. Z ) .x. ( ( invr ` R ) ` Z ) ) = Y )
24 10 19 23 3eqtr3d 
 |-  ( ph -> X = Y )