Metamath Proof Explorer

Theorem madurid

Description: Multiplying a matrix with its adjunct results in the identity matrix multiplied with the determinant of the matrix. See Proposition 4.16 in Lang p. 518. (Contributed by Stefan O'Rear, 16-Jul-2018)

Ref Expression
Hypotheses madurid.a 
|- A = ( N Mat R )
madurid.b 
|- B = ( Base ` A )
madurid.j 
|- J = ( N maAdju R )
madurid.d 
|- D = ( N maDet R )
madurid.i 
|- .1. = ( 1r ` A )
madurid.t 
|- .x. = ( .r ` A )
madurid.s 
|- .xb = ( .s ` A )
Assertion madurid 
|- ( ( M e. B /\ R e. CRing ) -> ( M .x. ( J ` M ) ) = ( ( D ` M ) .xb .1. ) )

Proof

Step Hyp Ref Expression
1 madurid.a 
 |-  A = ( N Mat R )
2 madurid.b 
 |-  B = ( Base ` A )
3 madurid.j 
 |-  J = ( N maAdju R )
4 madurid.d 
 |-  D = ( N maDet R )
5 madurid.i 
 |-  .1. = ( 1r ` A )
6 madurid.t 
 |-  .x. = ( .r ` A )
7 madurid.s 
 |-  .xb = ( .s ` A )
8 eqid 
 |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 simpr 
 |-  ( ( M e. B /\ R e. CRing ) -> R e. CRing )
12 1 2 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
13 12 simpld 
 |-  ( M e. B -> N e. Fin )
14 13 adantr 
 |-  ( ( M e. B /\ R e. CRing ) -> N e. Fin )
15 1 9 2 matbas2i 
 |-  ( M e. B -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
16 15 adantr 
 |-  ( ( M e. B /\ R e. CRing ) -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
17 1 3 2 maduf 
 |-  ( R e. CRing -> J : B --> B )
18 17 adantl 
 |-  ( ( M e. B /\ R e. CRing ) -> J : B --> B )
19 simpl 
 |-  ( ( M e. B /\ R e. CRing ) -> M e. B )
20 18 19 ffvelrnd 
 |-  ( ( M e. B /\ R e. CRing ) -> ( J ` M ) e. B )
21 1 9 2 matbas2i 
 |-  ( ( J ` M ) e. B -> ( J ` M ) e. ( ( Base ` R ) ^m ( N X. N ) ) )
22 20 21 syl 
 |-  ( ( M e. B /\ R e. CRing ) -> ( J ` M ) e. ( ( Base ` R ) ^m ( N X. N ) ) )
23 8 9 10 11 14 14 14 16 22 mamuval 
 |-  ( ( M e. B /\ R e. CRing ) -> ( M ( R maMul <. N , N , N >. ) ( J ` M ) ) = ( a e. N , b e. N |-> ( R gsum ( c e. N |-> ( ( a M c ) ( .r ` R ) ( c ( J ` M ) b ) ) ) ) ) )
24 1 8 matmulr 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
25 13 24 sylan 
 |-  ( ( M e. B /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
26 25 6 eqtr4di 
 |-  ( ( M e. B /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = .x. )
27 26 oveqd 
 |-  ( ( M e. B /\ R e. CRing ) -> ( M ( R maMul <. N , N , N >. ) ( J ` M ) ) = ( M .x. ( J ` M ) ) )
28 simp1l 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) -> M e. B )
29 simp1r 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) -> R e. CRing )
30 elmapi 
 |-  ( M e. ( ( Base ` R ) ^m ( N X. N ) ) -> M : ( N X. N ) --> ( Base ` R ) )
31 16 30 syl 
 |-  ( ( M e. B /\ R e. CRing ) -> M : ( N X. N ) --> ( Base ` R ) )
32 31 3ad2ant1 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) -> M : ( N X. N ) --> ( Base ` R ) )
33 32 adantr 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ c e. N ) -> M : ( N X. N ) --> ( Base ` R ) )
34 simpl2 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ c e. N ) -> a e. N )
35 simpr 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ c e. N ) -> c e. N )
36 33 34 35 fovrnd 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ c e. N ) -> ( a M c ) e. ( Base ` R ) )
37 simp3 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) -> b e. N )
38 1 3 2 4 10 9 28 29 36 37 madugsum 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) -> ( R gsum ( c e. N |-> ( ( a M c ) ( .r ` R ) ( c ( J ` M ) b ) ) ) ) = ( D ` ( d e. N , c e. N |-> if ( d = b , ( a M c ) , ( d M c ) ) ) ) )
39 iftrue 
 |-  ( a = b -> if ( a = b , ( D ` M ) , ( 0g ` R ) ) = ( D ` M ) )
40 39 adantl 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a = b ) -> if ( a = b , ( D ` M ) , ( 0g ` R ) ) = ( D ` M ) )
41 31 ffnd 
 |-  ( ( M e. B /\ R e. CRing ) -> M Fn ( N X. N ) )
42 fnov 
 |-  ( M Fn ( N X. N ) <-> M = ( d e. N , c e. N |-> ( d M c ) ) )
43 41 42 sylib 
 |-  ( ( M e. B /\ R e. CRing ) -> M = ( d e. N , c e. N |-> ( d M c ) ) )
44 43 adantr 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a = b ) -> M = ( d e. N , c e. N |-> ( d M c ) ) )
45 equtr2 
 |-  ( ( a = b /\ d = b ) -> a = d )
46 45 oveq1d 
 |-  ( ( a = b /\ d = b ) -> ( a M c ) = ( d M c ) )
47 46 ifeq1da 
 |-  ( a = b -> if ( d = b , ( a M c ) , ( d M c ) ) = if ( d = b , ( d M c ) , ( d M c ) ) )
48 ifid 
 |-  if ( d = b , ( d M c ) , ( d M c ) ) = ( d M c )
49 47 48 eqtrdi 
 |-  ( a = b -> if ( d = b , ( a M c ) , ( d M c ) ) = ( d M c ) )
50 49 adantl 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a = b ) -> if ( d = b , ( a M c ) , ( d M c ) ) = ( d M c ) )
51 50 mpoeq3dv 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a = b ) -> ( d e. N , c e. N |-> if ( d = b , ( a M c ) , ( d M c ) ) ) = ( d e. N , c e. N |-> ( d M c ) ) )
52 44 51 eqtr4d 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a = b ) -> M = ( d e. N , c e. N |-> if ( d = b , ( a M c ) , ( d M c ) ) ) )
53 52 fveq2d 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a = b ) -> ( D ` M ) = ( D ` ( d e. N , c e. N |-> if ( d = b , ( a M c ) , ( d M c ) ) ) ) )
54 40 53 eqtr2d 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a = b ) -> ( D ` ( d e. N , c e. N |-> if ( d = b , ( a M c ) , ( d M c ) ) ) ) = if ( a = b , ( D ` M ) , ( 0g ` R ) ) )
55 54 3ad2antl1 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ a = b ) -> ( D ` ( d e. N , c e. N |-> if ( d = b , ( a M c ) , ( d M c ) ) ) ) = if ( a = b , ( D ` M ) , ( 0g ` R ) ) )
56 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
57 simpl1r 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> R e. CRing )
58 14 3ad2ant1 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) -> N e. Fin )
59 58 adantr 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> N e. Fin )
60 32 ad2antrr 
 |-  ( ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) /\ c e. N ) -> M : ( N X. N ) --> ( Base ` R ) )
61 simpll2 
 |-  ( ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) /\ c e. N ) -> a e. N )
62 simpr 
 |-  ( ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) /\ c e. N ) -> c e. N )
63 60 61 62 fovrnd 
 |-  ( ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) /\ c e. N ) -> ( a M c ) e. ( Base ` R ) )
64 32 adantr 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> M : ( N X. N ) --> ( Base ` R ) )
65 64 fovrnda 
 |-  ( ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) /\ ( d e. N /\ c e. N ) ) -> ( d M c ) e. ( Base ` R ) )
66 65 3impb 
 |-  ( ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) /\ d e. N /\ c e. N ) -> ( d M c ) e. ( Base ` R ) )
67 simpl3 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> b e. N )
68 simpl2 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> a e. N )
69 neqne 
 |-  ( -. a = b -> a =/= b )
70 69 necomd 
 |-  ( -. a = b -> b =/= a )
71 70 adantl 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> b =/= a )
72 4 9 56 57 59 63 66 67 68 71 mdetralt2 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> ( D ` ( d e. N , c e. N |-> if ( d = b , ( a M c ) , if ( d = a , ( a M c ) , ( d M c ) ) ) ) ) = ( 0g ` R ) )
73 ifid 
 |-  if ( d = a , ( d M c ) , ( d M c ) ) = ( d M c )
74 oveq1 
 |-  ( d = a -> ( d M c ) = ( a M c ) )
75 74 adantl 
 |-  ( ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) /\ d = a ) -> ( d M c ) = ( a M c ) )
76 75 ifeq1da 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> if ( d = a , ( d M c ) , ( d M c ) ) = if ( d = a , ( a M c ) , ( d M c ) ) )
77 73 76 eqtr3id 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> ( d M c ) = if ( d = a , ( a M c ) , ( d M c ) ) )
78 77 ifeq2d 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> if ( d = b , ( a M c ) , ( d M c ) ) = if ( d = b , ( a M c ) , if ( d = a , ( a M c ) , ( d M c ) ) ) )
79 78 mpoeq3dv 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> ( d e. N , c e. N |-> if ( d = b , ( a M c ) , ( d M c ) ) ) = ( d e. N , c e. N |-> if ( d = b , ( a M c ) , if ( d = a , ( a M c ) , ( d M c ) ) ) ) )
80 79 fveq2d 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> ( D ` ( d e. N , c e. N |-> if ( d = b , ( a M c ) , ( d M c ) ) ) ) = ( D ` ( d e. N , c e. N |-> if ( d = b , ( a M c ) , if ( d = a , ( a M c ) , ( d M c ) ) ) ) ) )
81 iffalse 
 |-  ( -. a = b -> if ( a = b , ( D ` M ) , ( 0g ` R ) ) = ( 0g ` R ) )
82 81 adantl 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> if ( a = b , ( D ` M ) , ( 0g ` R ) ) = ( 0g ` R ) )
83 72 80 82 3eqtr4d 
 |-  ( ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) /\ -. a = b ) -> ( D ` ( d e. N , c e. N |-> if ( d = b , ( a M c ) , ( d M c ) ) ) ) = if ( a = b , ( D ` M ) , ( 0g ` R ) ) )
84 55 83 pm2.61dan 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) -> ( D ` ( d e. N , c e. N |-> if ( d = b , ( a M c ) , ( d M c ) ) ) ) = if ( a = b , ( D ` M ) , ( 0g ` R ) ) )
85 38 84 eqtrd 
 |-  ( ( ( M e. B /\ R e. CRing ) /\ a e. N /\ b e. N ) -> ( R gsum ( c e. N |-> ( ( a M c ) ( .r ` R ) ( c ( J ` M ) b ) ) ) ) = if ( a = b , ( D ` M ) , ( 0g ` R ) ) )
86 85 mpoeq3dva 
 |-  ( ( M e. B /\ R e. CRing ) -> ( a e. N , b e. N |-> ( R gsum ( c e. N |-> ( ( a M c ) ( .r ` R ) ( c ( J ` M ) b ) ) ) ) ) = ( a e. N , b e. N |-> if ( a = b , ( D ` M ) , ( 0g ` R ) ) ) )
87 5 oveq2i 
 |-  ( ( D ` M ) .xb .1. ) = ( ( D ` M ) .xb ( 1r ` A ) )
88 crngring 
 |-  ( R e. CRing -> R e. Ring )
89 88 adantl 
 |-  ( ( M e. B /\ R e. CRing ) -> R e. Ring )
90 4 1 2 9 mdetf 
 |-  ( R e. CRing -> D : B --> ( Base ` R ) )
91 90 adantl 
 |-  ( ( M e. B /\ R e. CRing ) -> D : B --> ( Base ` R ) )
92 91 19 ffvelrnd 
 |-  ( ( M e. B /\ R e. CRing ) -> ( D ` M ) e. ( Base ` R ) )
93 1 9 7 56 matsc 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( D ` M ) e. ( Base ` R ) ) -> ( ( D ` M ) .xb ( 1r ` A ) ) = ( a e. N , b e. N |-> if ( a = b , ( D ` M ) , ( 0g ` R ) ) ) )
94 14 89 92 93 syl3anc 
 |-  ( ( M e. B /\ R e. CRing ) -> ( ( D ` M ) .xb ( 1r ` A ) ) = ( a e. N , b e. N |-> if ( a = b , ( D ` M ) , ( 0g ` R ) ) ) )
95 87 94 syl5eq 
 |-  ( ( M e. B /\ R e. CRing ) -> ( ( D ` M ) .xb .1. ) = ( a e. N , b e. N |-> if ( a = b , ( D ` M ) , ( 0g ` R ) ) ) )
96 86 95 eqtr4d 
 |-  ( ( M e. B /\ R e. CRing ) -> ( a e. N , b e. N |-> ( R gsum ( c e. N |-> ( ( a M c ) ( .r ` R ) ( c ( J ` M ) b ) ) ) ) ) = ( ( D ` M ) .xb .1. ) )
97 23 27 96 3eqtr3d 
 |-  ( ( M e. B /\ R e. CRing ) -> ( M .x. ( J ` M ) ) = ( ( D ` M ) .xb .1. ) )