# Metamath Proof Explorer

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}\mathrm{Mat}{R}$
madurid.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
madurid.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
madurid.d ${⊢}{D}={N}\mathrm{maDet}{R}$

### Proof

Step Hyp Ref Expression
1 madurid.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 madurid.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 madurid.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
4 madurid.d ${⊢}{D}={N}\mathrm{maDet}{R}$
8 simpr ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {R}\in \mathrm{CRing}$
9 1 3 2 maduf ${⊢}{R}\in \mathrm{CRing}\to {J}:{B}⟶{B}$
10 9 ffvelrnda ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {J}\left({M}\right)\in {B}$
11 10 ancoms ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {J}\left({M}\right)\in {B}$
12 simpl ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {M}\in {B}$
13 1 2 6 mattposm
14 8 11 12 13 syl3anc
15 1 3 2 madutpos ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {J}\left(tpos{M}\right)=tpos{J}\left({M}\right)$
16 15 ancoms ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {J}\left(tpos{M}\right)=tpos{J}\left({M}\right)$
17 16 oveq2d
18 1 2 mattposcl ${⊢}{M}\in {B}\to tpos{M}\in {B}$
19 1 2 3 4 5 6 7 madurid
20 18 19 sylan
21 14 17 20 3eqtr2d
22 21 tposeqd
23 1 2 matrcl ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
24 23 simpld ${⊢}{M}\in {B}\to {N}\in \mathrm{Fin}$
25 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
26 1 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
27 24 25 26 syl2an ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {A}\in \mathrm{Ring}$
28 2 6 ringcl
29 27 11 12 28 syl3anc
30 1 2 mattpostpos
31 29 30 syl
32 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
33 4 1 2 32 mdetf ${⊢}{R}\in \mathrm{CRing}\to {D}:{B}⟶{\mathrm{Base}}_{{R}}$
34 33 adantl ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {D}:{B}⟶{\mathrm{Base}}_{{R}}$
35 18 adantr ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to tpos{M}\in {B}$
36 34 35 ffvelrnd ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {D}\left(tpos{M}\right)\in {\mathrm{Base}}_{{R}}$
37 2 5 ringidcl
38 27 37 syl
39 1 2 32 7 mattposvs
40 36 38 39 syl2anc
41 4 1 2 mdettpos ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {D}\left(tpos{M}\right)={D}\left({M}\right)$
42 41 ancoms ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {D}\left(tpos{M}\right)={D}\left({M}\right)$
43 1 5 mattpos1
44 24 25 43 syl2an
45 42 44 oveq12d
46 40 45 eqtrd
47 22 31 46 3eqtr3d