Metamath Proof Explorer

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}\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 eqid ${⊢}{R}\mathrm{maMul}⟨{N},{N},{N}⟩={R}\mathrm{maMul}⟨{N},{N},{N}⟩$
9 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
10 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
11 simpr ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {R}\in \mathrm{CRing}$
12 1 2 matrcl ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
13 12 simpld ${⊢}{M}\in {B}\to {N}\in \mathrm{Fin}$
14 13 adantr ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {N}\in \mathrm{Fin}$
15 1 9 2 matbas2i ${⊢}{M}\in {B}\to {M}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
16 15 adantr ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {M}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
17 1 3 2 maduf ${⊢}{R}\in \mathrm{CRing}\to {J}:{B}⟶{B}$
18 17 adantl ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {J}:{B}⟶{B}$
19 simpl ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {M}\in {B}$
20 18 19 ffvelrnd ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {J}\left({M}\right)\in {B}$
21 1 9 2 matbas2i ${⊢}{J}\left({M}\right)\in {B}\to {J}\left({M}\right)\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
22 20 21 syl ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {J}\left({M}\right)\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
23 8 9 10 11 14 14 14 16 22 mamuval ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {M}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){J}\left({M}\right)=\left({a}\in {N},{b}\in {N}⟼\underset{{c}\in {N}}{{\sum }_{{R}}}\left(\left({a}{M}{c}\right){\cdot }_{{R}}\left({c}{J}\left({M}\right){b}\right)\right)\right)$
24 1 8 matmulr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
25 13 24 sylan ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
26 25 6 syl6eqr
27 26 oveqd
28 simp1l ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {M}\in {B}$
29 simp1r ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {R}\in \mathrm{CRing}$
30 elmapi ${⊢}{M}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
31 16 30 syl ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
32 31 3ad2ant1 ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
33 32 adantr ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge {c}\in {N}\right)\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
34 simpl2 ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge {c}\in {N}\right)\to {a}\in {N}$
35 simpr ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge {c}\in {N}\right)\to {c}\in {N}$
36 33 34 35 fovrnd ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge {c}\in {N}\right)\to {a}{M}{c}\in {\mathrm{Base}}_{{R}}$
37 simp3 ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {b}\in {N}$
38 1 3 2 4 10 9 28 29 36 37 madugsum ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to \underset{{c}\in {N}}{{\sum }_{{R}}}\left(\left({a}{M}{c}\right){\cdot }_{{R}}\left({c}{J}\left({M}\right){b}\right)\right)={D}\left(\left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)\right)\right)$
39 iftrue ${⊢}{a}={b}\to if\left({a}={b},{D}\left({M}\right),{0}_{{R}}\right)={D}\left({M}\right)$
40 39 adantl ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}={b}\right)\to if\left({a}={b},{D}\left({M}\right),{0}_{{R}}\right)={D}\left({M}\right)$
41 31 ffnd ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {M}Fn\left({N}×{N}\right)$
42 fnov ${⊢}{M}Fn\left({N}×{N}\right)↔{M}=\left({d}\in {N},{c}\in {N}⟼{d}{M}{c}\right)$
43 41 42 sylib ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {M}=\left({d}\in {N},{c}\in {N}⟼{d}{M}{c}\right)$
44 43 adantr ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}={b}\right)\to {M}=\left({d}\in {N},{c}\in {N}⟼{d}{M}{c}\right)$
45 equtr2 ${⊢}\left({a}={b}\wedge {d}={b}\right)\to {a}={d}$
46 45 oveq1d ${⊢}\left({a}={b}\wedge {d}={b}\right)\to {a}{M}{c}={d}{M}{c}$
47 46 ifeq1da ${⊢}{a}={b}\to if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)=if\left({d}={b},{d}{M}{c},{d}{M}{c}\right)$
48 ifid ${⊢}if\left({d}={b},{d}{M}{c},{d}{M}{c}\right)={d}{M}{c}$
49 47 48 syl6eq ${⊢}{a}={b}\to if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)={d}{M}{c}$
50 49 adantl ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}={b}\right)\to if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)={d}{M}{c}$
51 50 mpoeq3dv ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}={b}\right)\to \left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)\right)=\left({d}\in {N},{c}\in {N}⟼{d}{M}{c}\right)$
52 44 51 eqtr4d ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}={b}\right)\to {M}=\left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)\right)$
53 52 fveq2d ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}={b}\right)\to {D}\left({M}\right)={D}\left(\left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)\right)\right)$
54 40 53 eqtr2d ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}={b}\right)\to {D}\left(\left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)\right)\right)=if\left({a}={b},{D}\left({M}\right),{0}_{{R}}\right)$
55 54 3ad2antl1 ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge {a}={b}\right)\to {D}\left(\left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)\right)\right)=if\left({a}={b},{D}\left({M}\right),{0}_{{R}}\right)$
56 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
57 simpl1r ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to {R}\in \mathrm{CRing}$
58 14 3ad2ant1 ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {N}\in \mathrm{Fin}$
59 58 adantr ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to {N}\in \mathrm{Fin}$
60 32 ad2antrr ${⊢}\left(\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\wedge {c}\in {N}\right)\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
61 simpll2 ${⊢}\left(\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\wedge {c}\in {N}\right)\to {a}\in {N}$
62 simpr ${⊢}\left(\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\wedge {c}\in {N}\right)\to {c}\in {N}$
63 60 61 62 fovrnd ${⊢}\left(\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\wedge {c}\in {N}\right)\to {a}{M}{c}\in {\mathrm{Base}}_{{R}}$
64 32 adantr ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
65 64 fovrnda ${⊢}\left(\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\wedge \left({d}\in {N}\wedge {c}\in {N}\right)\right)\to {d}{M}{c}\in {\mathrm{Base}}_{{R}}$
66 65 3impb ${⊢}\left(\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\wedge {d}\in {N}\wedge {c}\in {N}\right)\to {d}{M}{c}\in {\mathrm{Base}}_{{R}}$
67 simpl3 ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to {b}\in {N}$
68 simpl2 ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to {a}\in {N}$
69 neqne ${⊢}¬{a}={b}\to {a}\ne {b}$
70 69 necomd ${⊢}¬{a}={b}\to {b}\ne {a}$
71 70 adantl ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to {b}\ne {a}$
72 4 9 56 57 59 63 66 67 68 71 mdetralt2 ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to {D}\left(\left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},if\left({d}={a},{a}{M}{c},{d}{M}{c}\right)\right)\right)\right)={0}_{{R}}$
73 ifid ${⊢}if\left({d}={a},{d}{M}{c},{d}{M}{c}\right)={d}{M}{c}$
74 oveq1 ${⊢}{d}={a}\to {d}{M}{c}={a}{M}{c}$
75 74 adantl ${⊢}\left(\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\wedge {d}={a}\right)\to {d}{M}{c}={a}{M}{c}$
76 75 ifeq1da ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to if\left({d}={a},{d}{M}{c},{d}{M}{c}\right)=if\left({d}={a},{a}{M}{c},{d}{M}{c}\right)$
77 73 76 syl5eqr ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to {d}{M}{c}=if\left({d}={a},{a}{M}{c},{d}{M}{c}\right)$
78 77 ifeq2d ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)=if\left({d}={b},{a}{M}{c},if\left({d}={a},{a}{M}{c},{d}{M}{c}\right)\right)$
79 78 mpoeq3dv ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to \left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)\right)=\left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},if\left({d}={a},{a}{M}{c},{d}{M}{c}\right)\right)\right)$
80 79 fveq2d ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to {D}\left(\left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)\right)\right)={D}\left(\left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},if\left({d}={a},{a}{M}{c},{d}{M}{c}\right)\right)\right)\right)$
81 iffalse ${⊢}¬{a}={b}\to if\left({a}={b},{D}\left({M}\right),{0}_{{R}}\right)={0}_{{R}}$
82 81 adantl ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to if\left({a}={b},{D}\left({M}\right),{0}_{{R}}\right)={0}_{{R}}$
83 72 80 82 3eqtr4d ${⊢}\left(\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\wedge ¬{a}={b}\right)\to {D}\left(\left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)\right)\right)=if\left({a}={b},{D}\left({M}\right),{0}_{{R}}\right)$
84 55 83 pm2.61dan ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {D}\left(\left({d}\in {N},{c}\in {N}⟼if\left({d}={b},{a}{M}{c},{d}{M}{c}\right)\right)\right)=if\left({a}={b},{D}\left({M}\right),{0}_{{R}}\right)$
85 38 84 eqtrd ${⊢}\left(\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to \underset{{c}\in {N}}{{\sum }_{{R}}}\left(\left({a}{M}{c}\right){\cdot }_{{R}}\left({c}{J}\left({M}\right){b}\right)\right)=if\left({a}={b},{D}\left({M}\right),{0}_{{R}}\right)$
86 85 mpoeq3dva ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to \left({a}\in {N},{b}\in {N}⟼\underset{{c}\in {N}}{{\sum }_{{R}}}\left(\left({a}{M}{c}\right){\cdot }_{{R}}\left({c}{J}\left({M}\right){b}\right)\right)\right)=\left({a}\in {N},{b}\in {N}⟼if\left({a}={b},{D}\left({M}\right),{0}_{{R}}\right)\right)$
87 5 oveq2i
88 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
89 88 adantl ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {R}\in \mathrm{Ring}$
90 4 1 2 9 mdetf ${⊢}{R}\in \mathrm{CRing}\to {D}:{B}⟶{\mathrm{Base}}_{{R}}$
91 90 adantl ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {D}:{B}⟶{\mathrm{Base}}_{{R}}$
92 91 19 ffvelrnd ${⊢}\left({M}\in {B}\wedge {R}\in \mathrm{CRing}\right)\to {D}\left({M}\right)\in {\mathrm{Base}}_{{R}}$
93 1 9 7 56 matsc
94 14 89 92 93 syl3anc
95 87 94 syl5eq
96 86 95 eqtr4d
97 23 27 96 3eqtr3d