Metamath Proof Explorer

Theorem drngmulcanad

Description: Cancellation of a nonzero factor on the left for multiplication. ( mulcanad 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. )
drngmulcanad.2 
|- ( ph -> ( Z .x. X ) = ( Z .x. Y ) )
Assertion drngmulcanad 
|- ( 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 drngmulcanad.2 
 |-  ( ph -> ( Z .x. X ) = ( Z .x. Y ) )
10 9 oveq2d 
 |-  ( ph -> ( ( ( invr ` R ) ` Z ) .x. ( Z .x. X ) ) = ( ( ( invr ` R ) ` Z ) .x. ( Z .x. Y ) ) )
11 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
12 eqid 
 |-  ( invr ` R ) = ( invr ` R )
13 1 2 3 11 12 4 7 8 drnginvrld 
 |-  ( ph -> ( ( ( invr ` R ) ` Z ) .x. Z ) = ( 1r ` R ) )
14 13 oveq1d 
 |-  ( ph -> ( ( ( ( invr ` R ) ` Z ) .x. Z ) .x. X ) = ( ( 1r ` R ) .x. X ) )
15 4 drngringd 
 |-  ( ph -> R e. Ring )
16 1 2 12 4 7 8 drnginvrcld 
 |-  ( ph -> ( ( invr ` R ) ` Z ) e. B )
17 1 3 15 16 7 5 ringassd 
 |-  ( ph -> ( ( ( ( invr ` R ) ` Z ) .x. Z ) .x. X ) = ( ( ( invr ` R ) ` Z ) .x. ( Z .x. X ) ) )
18 1 3 11 15 5 ringlidmd 
 |-  ( ph -> ( ( 1r ` R ) .x. X ) = X )
19 14 17 18 3eqtr3d 
 |-  ( ph -> ( ( ( invr ` R ) ` Z ) .x. ( Z .x. X ) ) = X )
20 13 oveq1d 
 |-  ( ph -> ( ( ( ( invr ` R ) ` Z ) .x. Z ) .x. Y ) = ( ( 1r ` R ) .x. Y ) )
21 1 3 15 16 7 6 ringassd 
 |-  ( ph -> ( ( ( ( invr ` R ) ` Z ) .x. Z ) .x. Y ) = ( ( ( invr ` R ) ` Z ) .x. ( Z .x. Y ) ) )
22 1 3 11 15 6 ringlidmd 
 |-  ( ph -> ( ( 1r ` R ) .x. Y ) = Y )
23 20 21 22 3eqtr3d 
 |-  ( ph -> ( ( ( invr ` R ) ` Z ) .x. ( Z .x. Y ) ) = Y )
24 10 19 23 3eqtr3d 
 |-  ( ph -> X = Y )