Metamath Proof Explorer

Theorem drnginvmuld

Description: Inverse of a nonzero product. (Contributed by SN, 14-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 drnginvmuld.b 
 |-  B = ( Base ` R )
2 drnginvmuld.z 
 |-  .0. = ( 0g ` R )
3 drnginvmuld.t 
 |-  .x. = ( .r ` R )
4 drnginvmuld.i 
 |-  I = ( invr ` R )
5 drnginvmuld.r 
 |-  ( ph -> R e. DivRing )
6 drnginvmuld.x 
 |-  ( ph -> X e. B )
7 drnginvmuld.y 
 |-  ( ph -> Y e. B )
8 drnginvmuld.1 
 |-  ( ph -> X =/= .0. )
9 drnginvmuld.2 
 |-  ( ph -> Y =/= .0. )
10 5 drngringd 
 |-  ( ph -> R e. Ring )
11 1 3 10 6 7 ringcld 
 |-  ( ph -> ( X .x. Y ) e. B )
12 1 2 3 5 6 7 drngmulne0 
 |-  ( ph -> ( ( X .x. Y ) =/= .0. <-> ( X =/= .0. /\ Y =/= .0. ) ) )
13 8 9 12 mpbir2and 
 |-  ( ph -> ( X .x. Y ) =/= .0. )
14 1 2 4 5 11 13 drnginvrcld 
 |-  ( ph -> ( I ` ( X .x. Y ) ) e. B )
15 1 2 4 5 7 9 drnginvrcld 
 |-  ( ph -> ( I ` Y ) e. B )
16 1 2 4 5 6 8 drnginvrcld 
 |-  ( ph -> ( I ` X ) e. B )
17 1 3 10 15 16 ringcld 
 |-  ( ph -> ( ( I ` Y ) .x. ( I ` X ) ) e. B )
18 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
19 1 2 3 18 4 5 6 8 drnginvrld 
 |-  ( ph -> ( ( I ` X ) .x. X ) = ( 1r ` R ) )
20 19 oveq1d 
 |-  ( ph -> ( ( ( I ` X ) .x. X ) .x. Y ) = ( ( 1r ` R ) .x. Y ) )
21 1 3 18 10 7 ringlidmd 
 |-  ( ph -> ( ( 1r ` R ) .x. Y ) = Y )
22 20 21 eqtrd 
 |-  ( ph -> ( ( ( I ` X ) .x. X ) .x. Y ) = Y )
23 22 oveq2d 
 |-  ( ph -> ( ( I ` Y ) .x. ( ( ( I ` X ) .x. X ) .x. Y ) ) = ( ( I ` Y ) .x. Y ) )
24 23 eqcomd 
 |-  ( ph -> ( ( I ` Y ) .x. Y ) = ( ( I ` Y ) .x. ( ( ( I ` X ) .x. X ) .x. Y ) ) )
25 1 2 3 18 4 5 7 9 drnginvrld 
 |-  ( ph -> ( ( I ` Y ) .x. Y ) = ( 1r ` R ) )
26 1 3 10 16 6 7 ringassd 
 |-  ( ph -> ( ( ( I ` X ) .x. X ) .x. Y ) = ( ( I ` X ) .x. ( X .x. Y ) ) )
27 26 oveq2d 
 |-  ( ph -> ( ( I ` Y ) .x. ( ( ( I ` X ) .x. X ) .x. Y ) ) = ( ( I ` Y ) .x. ( ( I ` X ) .x. ( X .x. Y ) ) ) )
28 24 25 27 3eqtr3d 
 |-  ( ph -> ( 1r ` R ) = ( ( I ` Y ) .x. ( ( I ` X ) .x. ( X .x. Y ) ) ) )
29 1 2 3 18 4 5 11 13 drnginvrld 
 |-  ( ph -> ( ( I ` ( X .x. Y ) ) .x. ( X .x. Y ) ) = ( 1r ` R ) )
30 1 3 10 15 16 11 ringassd 
 |-  ( ph -> ( ( ( I ` Y ) .x. ( I ` X ) ) .x. ( X .x. Y ) ) = ( ( I ` Y ) .x. ( ( I ` X ) .x. ( X .x. Y ) ) ) )
31 28 29 30 3eqtr4d 
 |-  ( ph -> ( ( I ` ( X .x. Y ) ) .x. ( X .x. Y ) ) = ( ( ( I ` Y ) .x. ( I ` X ) ) .x. ( X .x. Y ) ) )
32 1 2 3 5 14 17 11 13 31 drngmulcan2ad 
 |-  ( ph -> ( I ` ( X .x. Y ) ) = ( ( I ` Y ) .x. ( I ` X ) ) )