Metamath Proof Explorer

Theorem invrvald

Description: If a matrix multiplied with a given matrix (from the left as well as from the right) results in the identity matrix, this matrix is the inverse (matrix) of the given matrix. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Hypotheses invrvald.b 
|- B = ( Base ` R )
invrvald.t 
|- .x. = ( .r ` R )
invrvald.o 
|- .1. = ( 1r ` R )
invrvald.u 
|- U = ( Unit ` R )
invrvald.i 
|- I = ( invr ` R )
invrvald.r 
|- ( ph -> R e. Ring )
invrvald.x 
|- ( ph -> X e. B )
invrvald.y 
|- ( ph -> Y e. B )
invrvald.xy 
|- ( ph -> ( X .x. Y ) = .1. )
invrvald.yx 
|- ( ph -> ( Y .x. X ) = .1. )
Assertion invrvald 
|- ( ph -> ( X e. U /\ ( I ` X ) = Y ) )

Proof

Step Hyp Ref Expression
1 invrvald.b 
 |-  B = ( Base ` R )
2 invrvald.t 
 |-  .x. = ( .r ` R )
3 invrvald.o 
 |-  .1. = ( 1r ` R )
4 invrvald.u 
 |-  U = ( Unit ` R )
5 invrvald.i 
 |-  I = ( invr ` R )
6 invrvald.r 
 |-  ( ph -> R e. Ring )
7 invrvald.x 
 |-  ( ph -> X e. B )
8 invrvald.y 
 |-  ( ph -> Y e. B )
9 invrvald.xy 
 |-  ( ph -> ( X .x. Y ) = .1. )
10 invrvald.yx 
 |-  ( ph -> ( Y .x. X ) = .1. )
11 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
12 1 11 2 dvdsrmul 
 |-  ( ( X e. B /\ Y e. B ) -> X ( ||r ` R ) ( Y .x. X ) )
13 7 8 12 syl2anc 
 |-  ( ph -> X ( ||r ` R ) ( Y .x. X ) )
14 13 10 breqtrd 
 |-  ( ph -> X ( ||r ` R ) .1. )
15 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
16 15 1 opprbas 
 |-  B = ( Base ` ( oppR ` R ) )
17 eqid 
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
18 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
19 16 17 18 dvdsrmul 
 |-  ( ( X e. B /\ Y e. B ) -> X ( ||r ` ( oppR ` R ) ) ( Y ( .r ` ( oppR ` R ) ) X ) )
20 7 8 19 syl2anc 
 |-  ( ph -> X ( ||r ` ( oppR ` R ) ) ( Y ( .r ` ( oppR ` R ) ) X ) )
21 1 2 15 18 opprmul 
 |-  ( Y ( .r ` ( oppR ` R ) ) X ) = ( X .x. Y )
22 21 9 eqtrid 
 |-  ( ph -> ( Y ( .r ` ( oppR ` R ) ) X ) = .1. )
23 20 22 breqtrd 
 |-  ( ph -> X ( ||r ` ( oppR ` R ) ) .1. )
24 4 3 11 15 17 isunit 
 |-  ( X e. U <-> ( X ( ||r ` R ) .1. /\ X ( ||r ` ( oppR ` R ) ) .1. ) )
25 14 23 24 sylanbrc 
 |-  ( ph -> X e. U )
26 eqid 
 |-  ( ( mulGrp ` R ) |`s U ) = ( ( mulGrp ` R ) |`s U )
27 4 26 3 unitgrpid 
 |-  ( R e. Ring -> .1. = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) )
28 6 27 syl 
 |-  ( ph -> .1. = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) )
29 9 28 eqtrd 
 |-  ( ph -> ( X .x. Y ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) )
30 4 26 unitgrp 
 |-  ( R e. Ring -> ( ( mulGrp ` R ) |`s U ) e. Grp )
31 6 30 syl 
 |-  ( ph -> ( ( mulGrp ` R ) |`s U ) e. Grp )
32 1 11 2 dvdsrmul 
 |-  ( ( Y e. B /\ X e. B ) -> Y ( ||r ` R ) ( X .x. Y ) )
33 8 7 32 syl2anc 
 |-  ( ph -> Y ( ||r ` R ) ( X .x. Y ) )
34 33 9 breqtrd 
 |-  ( ph -> Y ( ||r ` R ) .1. )
35 16 17 18 dvdsrmul 
 |-  ( ( Y e. B /\ X e. B ) -> Y ( ||r ` ( oppR ` R ) ) ( X ( .r ` ( oppR ` R ) ) Y ) )
36 8 7 35 syl2anc 
 |-  ( ph -> Y ( ||r ` ( oppR ` R ) ) ( X ( .r ` ( oppR ` R ) ) Y ) )
37 1 2 15 18 opprmul 
 |-  ( X ( .r ` ( oppR ` R ) ) Y ) = ( Y .x. X )
38 37 10 eqtrid 
 |-  ( ph -> ( X ( .r ` ( oppR ` R ) ) Y ) = .1. )
39 36 38 breqtrd 
 |-  ( ph -> Y ( ||r ` ( oppR ` R ) ) .1. )
40 4 3 11 15 17 isunit 
 |-  ( Y e. U <-> ( Y ( ||r ` R ) .1. /\ Y ( ||r ` ( oppR ` R ) ) .1. ) )
41 34 39 40 sylanbrc 
 |-  ( ph -> Y e. U )
42 4 26 unitgrpbas 
 |-  U = ( Base ` ( ( mulGrp ` R ) |`s U ) )
43 4 fvexi 
 |-  U e. _V
44 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
45 44 2 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
46 26 45 ressplusg 
 |-  ( U e. _V -> .x. = ( +g ` ( ( mulGrp ` R ) |`s U ) ) )
47 43 46 ax-mp 
 |-  .x. = ( +g ` ( ( mulGrp ` R ) |`s U ) )
48 eqid 
 |-  ( 0g ` ( ( mulGrp ` R ) |`s U ) ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) )
49 4 26 5 invrfval 
 |-  I = ( invg ` ( ( mulGrp ` R ) |`s U ) )
50 42 47 48 49 grpinvid1 
 |-  ( ( ( ( mulGrp ` R ) |`s U ) e. Grp /\ X e. U /\ Y e. U ) -> ( ( I ` X ) = Y <-> ( X .x. Y ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) ) )
51 31 25 41 50 syl3anc 
 |-  ( ph -> ( ( I ` X ) = Y <-> ( X .x. Y ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) ) )
52 29 51 mpbird 
 |-  ( ph -> ( I ` X ) = Y )
53 25 52 jca 
 |-  ( ph -> ( X e. U /\ ( I ` X ) = Y ) )