Metamath Proof Explorer

Theorem madulid

Description: Multiplying the adjunct of a matrix with the matrix 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, 17-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 madulid 
|- ( ( M e. B /\ R e. CRing ) -> ( ( J ` M ) .x. 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 simpr 
 |-  ( ( M e. B /\ R e. CRing ) -> R e. CRing )
9 1 3 2 maduf 
 |-  ( R e. CRing -> J : B --> B )
10 9 ffvelcdmda 
 |-  ( ( R e. CRing /\ M e. B ) -> ( J ` M ) e. B )
11 10 ancoms 
 |-  ( ( M e. B /\ R e. CRing ) -> ( J ` M ) e. B )
12 simpl 
 |-  ( ( M e. B /\ R e. CRing ) -> M e. B )
13 1 2 6 mattposm 
 |-  ( ( R e. CRing /\ ( J ` M ) e. B /\ M e. B ) -> tpos ( ( J ` M ) .x. M ) = ( tpos M .x. tpos ( J ` M ) ) )
14 8 11 12 13 syl3anc 
 |-  ( ( M e. B /\ R e. CRing ) -> tpos ( ( J ` M ) .x. M ) = ( tpos M .x. tpos ( J ` M ) ) )
15 1 3 2 madutpos 
 |-  ( ( R e. CRing /\ M e. B ) -> ( J ` tpos M ) = tpos ( J ` M ) )
16 15 ancoms 
 |-  ( ( M e. B /\ R e. CRing ) -> ( J ` tpos M ) = tpos ( J ` M ) )
17 16 oveq2d 
 |-  ( ( M e. B /\ R e. CRing ) -> ( tpos M .x. ( J ` tpos M ) ) = ( tpos M .x. tpos ( J ` M ) ) )
18 1 2 mattposcl 
 |-  ( M e. B -> tpos M e. B )
19 1 2 3 4 5 6 7 madurid 
 |-  ( ( tpos M e. B /\ R e. CRing ) -> ( tpos M .x. ( J ` tpos M ) ) = ( ( D ` tpos M ) .xb .1. ) )
20 18 19 sylan 
 |-  ( ( M e. B /\ R e. CRing ) -> ( tpos M .x. ( J ` tpos M ) ) = ( ( D ` tpos M ) .xb .1. ) )
21 14 17 20 3eqtr2d 
 |-  ( ( M e. B /\ R e. CRing ) -> tpos ( ( J ` M ) .x. M ) = ( ( D ` tpos M ) .xb .1. ) )
22 21 tposeqd 
 |-  ( ( M e. B /\ R e. CRing ) -> tpos tpos ( ( J ` M ) .x. M ) = tpos ( ( D ` tpos M ) .xb .1. ) )
23 1 2 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
24 23 simpld 
 |-  ( M e. B -> N e. Fin )
25 crngring 
 |-  ( R e. CRing -> R e. Ring )
26 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
27 24 25 26 syl2an 
 |-  ( ( M e. B /\ R e. CRing ) -> A e. Ring )
28 2 6 ringcl 
 |-  ( ( A e. Ring /\ ( J ` M ) e. B /\ M e. B ) -> ( ( J ` M ) .x. M ) e. B )
29 27 11 12 28 syl3anc 
 |-  ( ( M e. B /\ R e. CRing ) -> ( ( J ` M ) .x. M ) e. B )
30 1 2 mattpostpos 
 |-  ( ( ( J ` M ) .x. M ) e. B -> tpos tpos ( ( J ` M ) .x. M ) = ( ( J ` M ) .x. M ) )
31 29 30 syl 
 |-  ( ( M e. B /\ R e. CRing ) -> tpos tpos ( ( J ` M ) .x. M ) = ( ( J ` M ) .x. M ) )
32 eqid 
 |-  ( Base ` R ) = ( Base ` R )
33 4 1 2 32 mdetf 
 |-  ( R e. CRing -> D : B --> ( Base ` R ) )
34 33 adantl 
 |-  ( ( M e. B /\ R e. CRing ) -> D : B --> ( Base ` R ) )
35 18 adantr 
 |-  ( ( M e. B /\ R e. CRing ) -> tpos M e. B )
36 34 35 ffvelcdmd 
 |-  ( ( M e. B /\ R e. CRing ) -> ( D ` tpos M ) e. ( Base ` R ) )
37 2 5 ringidcl 
 |-  ( A e. Ring -> .1. e. B )
38 27 37 syl 
 |-  ( ( M e. B /\ R e. CRing ) -> .1. e. B )
39 1 2 32 7 mattposvs 
 |-  ( ( ( D ` tpos M ) e. ( Base ` R ) /\ .1. e. B ) -> tpos ( ( D ` tpos M ) .xb .1. ) = ( ( D ` tpos M ) .xb tpos .1. ) )
40 36 38 39 syl2anc 
 |-  ( ( M e. B /\ R e. CRing ) -> tpos ( ( D ` tpos M ) .xb .1. ) = ( ( D ` tpos M ) .xb tpos .1. ) )
41 4 1 2 mdettpos 
 |-  ( ( R e. CRing /\ M e. B ) -> ( D ` tpos M ) = ( D ` M ) )
42 41 ancoms 
 |-  ( ( M e. B /\ R e. CRing ) -> ( D ` tpos M ) = ( D ` M ) )
43 1 5 mattpos1 
 |-  ( ( N e. Fin /\ R e. Ring ) -> tpos .1. = .1. )
44 24 25 43 syl2an 
 |-  ( ( M e. B /\ R e. CRing ) -> tpos .1. = .1. )
45 42 44 oveq12d 
 |-  ( ( M e. B /\ R e. CRing ) -> ( ( D ` tpos M ) .xb tpos .1. ) = ( ( D ` M ) .xb .1. ) )
46 40 45 eqtrd 
 |-  ( ( M e. B /\ R e. CRing ) -> tpos ( ( D ` tpos M ) .xb .1. ) = ( ( D ` M ) .xb .1. ) )
47 22 31 46 3eqtr3d 
 |-  ( ( M e. B /\ R e. CRing ) -> ( ( J ` M ) .x. M ) = ( ( D ` M ) .xb .1. ) )