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

Metamath Proof Explorer

Theorem matinv

Description: The inverse of a matrix is the adjunct of the matrix multiplied with the inverse of the determinant of the matrix if the determinant is a unit in the underlying ring. Proposition 4.16 in Lang p. 518. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Hypotheses matinv.a 
|- A = ( N Mat R )
matinv.j 
|- J = ( N maAdju R )
matinv.d 
|- D = ( N maDet R )
matinv.b 
|- B = ( Base ` A )
matinv.u 
|- U = ( Unit ` A )
matinv.v 
|- V = ( Unit ` R )
matinv.h 
|- H = ( invr ` R )
matinv.i 
|- I = ( invr ` A )
matinv.t 
|- .xb = ( .s ` A )
Assertion matinv 
|- ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( M e. U /\ ( I ` M ) = ( ( H ` ( D ` M ) ) .xb ( J ` M ) ) ) )

Proof

Step Hyp Ref Expression
1 matinv.a 
 |-  A = ( N Mat R )
2 matinv.j 
 |-  J = ( N maAdju R )
3 matinv.d 
 |-  D = ( N maDet R )
4 matinv.b 
 |-  B = ( Base ` A )
5 matinv.u 
 |-  U = ( Unit ` A )
6 matinv.v 
 |-  V = ( Unit ` R )
7 matinv.h 
 |-  H = ( invr ` R )
8 matinv.i 
 |-  I = ( invr ` A )
9 matinv.t 
 |-  .xb = ( .s ` A )
10 eqid 
 |-  ( .r ` A ) = ( .r ` A )
11 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
12 1 4 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
13 12 simpld 
 |-  ( M e. B -> N e. Fin )
14 13 3ad2ant2 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> N e. Fin )
15 simp1 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> R e. CRing )
16 1 matassa 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. AssAlg )
17 14 15 16 syl2anc 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> A e. AssAlg )
18 assaring 
 |-  ( A e. AssAlg -> A e. Ring )
19 17 18 syl 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> A e. Ring )
20 simp2 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> M e. B )
21 assalmod 
 |-  ( A e. AssAlg -> A e. LMod )
22 17 21 syl 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> A e. LMod )
23 crngring 
 |-  ( R e. CRing -> R e. Ring )
24 23 3ad2ant1 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> R e. Ring )
25 simp3 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( D ` M ) e. V )
26 eqid 
 |-  ( Base ` R ) = ( Base ` R )
27 6 7 26 ringinvcl 
 |-  ( ( R e. Ring /\ ( D ` M ) e. V ) -> ( H ` ( D ` M ) ) e. ( Base ` R ) )
28 24 25 27 syl2anc 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( H ` ( D ` M ) ) e. ( Base ` R ) )
29 1 matsca2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R = ( Scalar ` A ) )
30 14 15 29 syl2anc 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> R = ( Scalar ` A ) )
31 30 fveq2d 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( Base ` R ) = ( Base ` ( Scalar ` A ) ) )
32 28 31 eleqtrd 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( H ` ( D ` M ) ) e. ( Base ` ( Scalar ` A ) ) )
33 1 2 4 maduf 
 |-  ( R e. CRing -> J : B --> B )
34 33 3ad2ant1 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> J : B --> B )
35 34 20 ffvelcdmd 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( J ` M ) e. B )
36 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
37 eqid 
 |-  ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) )
38 4 36 9 37 lmodvscl 
 |-  ( ( A e. LMod /\ ( H ` ( D ` M ) ) e. ( Base ` ( Scalar ` A ) ) /\ ( J ` M ) e. B ) -> ( ( H ` ( D ` M ) ) .xb ( J ` M ) ) e. B )
39 22 32 35 38 syl3anc 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( H ` ( D ` M ) ) .xb ( J ` M ) ) e. B )
40 4 36 37 9 10 assaassr 
 |-  ( ( A e. AssAlg /\ ( ( H ` ( D ` M ) ) e. ( Base ` ( Scalar ` A ) ) /\ M e. B /\ ( J ` M ) e. B ) ) -> ( M ( .r ` A ) ( ( H ` ( D ` M ) ) .xb ( J ` M ) ) ) = ( ( H ` ( D ` M ) ) .xb ( M ( .r ` A ) ( J ` M ) ) ) )
41 17 32 20 35 40 syl13anc 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( M ( .r ` A ) ( ( H ` ( D ` M ) ) .xb ( J ` M ) ) ) = ( ( H ` ( D ` M ) ) .xb ( M ( .r ` A ) ( J ` M ) ) ) )
42 1 4 2 3 11 10 9 madurid 
 |-  ( ( M e. B /\ R e. CRing ) -> ( M ( .r ` A ) ( J ` M ) ) = ( ( D ` M ) .xb ( 1r ` A ) ) )
43 20 15 42 syl2anc 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( M ( .r ` A ) ( J ` M ) ) = ( ( D ` M ) .xb ( 1r ` A ) ) )
44 43 oveq2d 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( H ` ( D ` M ) ) .xb ( M ( .r ` A ) ( J ` M ) ) ) = ( ( H ` ( D ` M ) ) .xb ( ( D ` M ) .xb ( 1r ` A ) ) ) )
45 eqid 
 |-  ( .r ` R ) = ( .r ` R )
46 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
47 6 7 45 46 unitlinv 
 |-  ( ( R e. Ring /\ ( D ` M ) e. V ) -> ( ( H ` ( D ` M ) ) ( .r ` R ) ( D ` M ) ) = ( 1r ` R ) )
48 24 25 47 syl2anc 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( H ` ( D ` M ) ) ( .r ` R ) ( D ` M ) ) = ( 1r ` R ) )
49 30 fveq2d 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( .r ` R ) = ( .r ` ( Scalar ` A ) ) )
50 49 oveqd 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( H ` ( D ` M ) ) ( .r ` R ) ( D ` M ) ) = ( ( H ` ( D ` M ) ) ( .r ` ( Scalar ` A ) ) ( D ` M ) ) )
51 30 fveq2d 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( 1r ` R ) = ( 1r ` ( Scalar ` A ) ) )
52 48 50 51 3eqtr3d 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( H ` ( D ` M ) ) ( .r ` ( Scalar ` A ) ) ( D ` M ) ) = ( 1r ` ( Scalar ` A ) ) )
53 52 oveq1d 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( ( H ` ( D ` M ) ) ( .r ` ( Scalar ` A ) ) ( D ` M ) ) .xb ( 1r ` A ) ) = ( ( 1r ` ( Scalar ` A ) ) .xb ( 1r ` A ) ) )
54 26 6 unitcl 
 |-  ( ( D ` M ) e. V -> ( D ` M ) e. ( Base ` R ) )
55 54 3ad2ant3 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( D ` M ) e. ( Base ` R ) )
56 55 31 eleqtrd 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( D ` M ) e. ( Base ` ( Scalar ` A ) ) )
57 4 11 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. B )
58 19 57 syl 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( 1r ` A ) e. B )
59 eqid 
 |-  ( .r ` ( Scalar ` A ) ) = ( .r ` ( Scalar ` A ) )
60 4 36 9 37 59 lmodvsass 
 |-  ( ( A e. LMod /\ ( ( H ` ( D ` M ) ) e. ( Base ` ( Scalar ` A ) ) /\ ( D ` M ) e. ( Base ` ( Scalar ` A ) ) /\ ( 1r ` A ) e. B ) ) -> ( ( ( H ` ( D ` M ) ) ( .r ` ( Scalar ` A ) ) ( D ` M ) ) .xb ( 1r ` A ) ) = ( ( H ` ( D ` M ) ) .xb ( ( D ` M ) .xb ( 1r ` A ) ) ) )
61 22 32 56 58 60 syl13anc 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( ( H ` ( D ` M ) ) ( .r ` ( Scalar ` A ) ) ( D ` M ) ) .xb ( 1r ` A ) ) = ( ( H ` ( D ` M ) ) .xb ( ( D ` M ) .xb ( 1r ` A ) ) ) )
62 eqid 
 |-  ( 1r ` ( Scalar ` A ) ) = ( 1r ` ( Scalar ` A ) )
63 4 36 9 62 lmodvs1 
 |-  ( ( A e. LMod /\ ( 1r ` A ) e. B ) -> ( ( 1r ` ( Scalar ` A ) ) .xb ( 1r ` A ) ) = ( 1r ` A ) )
64 22 58 63 syl2anc 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( 1r ` ( Scalar ` A ) ) .xb ( 1r ` A ) ) = ( 1r ` A ) )
65 53 61 64 3eqtr3d 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( H ` ( D ` M ) ) .xb ( ( D ` M ) .xb ( 1r ` A ) ) ) = ( 1r ` A ) )
66 41 44 65 3eqtrd 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( M ( .r ` A ) ( ( H ` ( D ` M ) ) .xb ( J ` M ) ) ) = ( 1r ` A ) )
67 4 36 37 9 10 assaass 
 |-  ( ( A e. AssAlg /\ ( ( H ` ( D ` M ) ) e. ( Base ` ( Scalar ` A ) ) /\ ( J ` M ) e. B /\ M e. B ) ) -> ( ( ( H ` ( D ` M ) ) .xb ( J ` M ) ) ( .r ` A ) M ) = ( ( H ` ( D ` M ) ) .xb ( ( J ` M ) ( .r ` A ) M ) ) )
68 17 32 35 20 67 syl13anc 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( ( H ` ( D ` M ) ) .xb ( J ` M ) ) ( .r ` A ) M ) = ( ( H ` ( D ` M ) ) .xb ( ( J ` M ) ( .r ` A ) M ) ) )
69 1 4 2 3 11 10 9 madulid 
 |-  ( ( M e. B /\ R e. CRing ) -> ( ( J ` M ) ( .r ` A ) M ) = ( ( D ` M ) .xb ( 1r ` A ) ) )
70 20 15 69 syl2anc 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( J ` M ) ( .r ` A ) M ) = ( ( D ` M ) .xb ( 1r ` A ) ) )
71 70 oveq2d 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( H ` ( D ` M ) ) .xb ( ( J ` M ) ( .r ` A ) M ) ) = ( ( H ` ( D ` M ) ) .xb ( ( D ` M ) .xb ( 1r ` A ) ) ) )
72 68 71 65 3eqtrd 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( ( ( H ` ( D ` M ) ) .xb ( J ` M ) ) ( .r ` A ) M ) = ( 1r ` A ) )
73 4 10 11 5 8 19 20 39 66 72 invrvald 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( M e. U /\ ( I ` M ) = ( ( H ` ( D ` M ) ) .xb ( J ` M ) ) ) )