# Metamath Proof Explorer

Description: The determinant of a matrix with a row L consisting of the same element X is the sum of the elements of the L -th column of the adjunct of the matrix multiplied with X . (Contributed by Stefan O'Rear, 16-Jul-2018)

Ref Expression
Hypotheses maduf.a ${⊢}{A}={N}\mathrm{Mat}{R}$
maduf.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
maduf.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
madugsum.d ${⊢}{D}={N}\mathrm{maDet}{R}$
madugsum.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
madugsum.m ${⊢}{\phi }\to {M}\in {B}$
madugsum.r ${⊢}{\phi }\to {R}\in \mathrm{CRing}$
madugsum.x ${⊢}\left({\phi }\wedge {i}\in {N}\right)\to {X}\in {K}$
madugsum.l ${⊢}{\phi }\to {L}\in {N}$

### Proof

Step Hyp Ref Expression
1 maduf.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 maduf.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
3 maduf.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
4 madugsum.d ${⊢}{D}={N}\mathrm{maDet}{R}$
6 madugsum.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
7 madugsum.m ${⊢}{\phi }\to {M}\in {B}$
8 madugsum.r ${⊢}{\phi }\to {R}\in \mathrm{CRing}$
9 madugsum.x ${⊢}\left({\phi }\wedge {i}\in {N}\right)\to {X}\in {K}$
10 madugsum.l ${⊢}{\phi }\to {L}\in {N}$
11 mpteq1
12 11 oveq2d
13 eleq2 ${⊢}{c}=\varnothing \to \left({b}\in {c}↔{b}\in \varnothing \right)$
14 13 ifbid
15 14 ifeq1d
16 15 mpoeq3dv
17 16 fveq2d
18 12 17 eqeq12d
19 mpteq1
20 19 oveq2d
21 eleq2 ${⊢}{c}={d}\to \left({b}\in {c}↔{b}\in {d}\right)$
22 21 ifbid
23 22 ifeq1d
24 23 mpoeq3dv
25 24 fveq2d
26 20 25 eqeq12d
27 mpteq1
28 27 oveq2d
29 eleq2 ${⊢}{c}={d}\cup \left\{{e}\right\}\to \left({b}\in {c}↔{b}\in \left({d}\cup \left\{{e}\right\}\right)\right)$
30 29 ifbid
31 30 ifeq1d
32 31 mpoeq3dv
33 32 fveq2d
34 28 33 eqeq12d
35 mpteq1
36 35 oveq2d
37 eleq2 ${⊢}{c}={N}\to \left({b}\in {c}↔{b}\in {N}\right)$
38 37 ifbid
39 38 ifeq1d
40 39 mpoeq3dv
41 40 fveq2d
42 36 41 eqeq12d
43 noel ${⊢}¬{b}\in \varnothing$
44 iffalse
45 43 44 mp1i
46 45 ifeq1d
47 46 mpoeq3ia
48 47 fveq2i
49 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
50 1 3 matrcl ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
51 7 50 syl ${⊢}{\phi }\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
52 51 simpld ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
53 1 6 3 matbas2i ${⊢}{M}\in {B}\to {M}\in \left({{K}}^{\left({N}×{N}\right)}\right)$
54 elmapi ${⊢}{M}\in \left({{K}}^{\left({N}×{N}\right)}\right)\to {M}:{N}×{N}⟶{K}$
55 7 53 54 3syl ${⊢}{\phi }\to {M}:{N}×{N}⟶{K}$
56 55 fovrnda ${⊢}\left({\phi }\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {a}{M}{b}\in {K}$
57 56 3impb ${⊢}\left({\phi }\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {a}{M}{b}\in {K}$
58 4 6 49 8 52 57 10 mdetr0 ${⊢}{\phi }\to {D}\left(\left({a}\in {N},{b}\in {N}⟼if\left({a}={L},{0}_{{R}},{a}{M}{b}\right)\right)\right)={0}_{{R}}$
59 48 58 syl5eq
60 mpt0
61 60 oveq2i
62 49 gsum0 ${⊢}{\sum }_{{R}}\varnothing ={0}_{{R}}$
63 61 62 eqtri
64 59 63 syl6reqr
65 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
66 8 adantr ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {R}\in \mathrm{CRing}$
67 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
68 66 67 syl ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {R}\in \mathrm{Ring}$
69 ringcmn ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{CMnd}$
70 68 69 syl ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {R}\in \mathrm{CMnd}$
71 52 adantr ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {N}\in \mathrm{Fin}$
72 simprl ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {d}\subseteq {N}$
73 71 72 ssfid ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {d}\in \mathrm{Fin}$
74 68 adantr ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {b}\in {d}\right)\to {R}\in \mathrm{Ring}$
75 72 sselda ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {b}\in {d}\right)\to {b}\in {N}$
76 9 ralrimiva ${⊢}{\phi }\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}{X}\in {K}$
77 76 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {b}\in {d}\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}{X}\in {K}$
78 rspcsbela
79 75 77 78 syl2anc
80 1 2 3 maduf ${⊢}{R}\in \mathrm{CRing}\to {J}:{B}⟶{B}$
81 8 80 syl ${⊢}{\phi }\to {J}:{B}⟶{B}$
82 81 7 ffvelrnd ${⊢}{\phi }\to {J}\left({M}\right)\in {B}$
83 1 6 3 matbas2i ${⊢}{J}\left({M}\right)\in {B}\to {J}\left({M}\right)\in \left({{K}}^{\left({N}×{N}\right)}\right)$
84 elmapi ${⊢}{J}\left({M}\right)\in \left({{K}}^{\left({N}×{N}\right)}\right)\to {J}\left({M}\right):{N}×{N}⟶{K}$
85 82 83 84 3syl ${⊢}{\phi }\to {J}\left({M}\right):{N}×{N}⟶{K}$
86 85 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {b}\in {d}\right)\to {J}\left({M}\right):{N}×{N}⟶{K}$
87 10 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {b}\in {d}\right)\to {L}\in {N}$
88 86 75 87 fovrnd ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {b}\in {d}\right)\to {b}{J}\left({M}\right){L}\in {K}$
89 6 5 ringcl
90 74 79 88 89 syl3anc
91 vex ${⊢}{e}\in \mathrm{V}$
92 91 a1i ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {e}\in \mathrm{V}$
93 eldifn ${⊢}{e}\in \left({N}\setminus {d}\right)\to ¬{e}\in {d}$
94 93 ad2antll ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to ¬{e}\in {d}$
95 eldifi ${⊢}{e}\in \left({N}\setminus {d}\right)\to {e}\in {N}$
96 95 ad2antll ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {e}\in {N}$
97 76 adantr ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}{X}\in {K}$
98 rspcsbela
99 96 97 98 syl2anc
100 85 adantr ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {J}\left({M}\right):{N}×{N}⟶{K}$
101 10 adantr ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {L}\in {N}$
102 100 96 101 fovrnd ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {e}{J}\left({M}\right){L}\in {K}$
103 6 5 ringcl
104 68 99 102 103 syl3anc
105 csbeq1
106 oveq1 ${⊢}{b}={e}\to {b}{J}\left({M}\right){L}={e}{J}\left({M}\right){L}$
107 105 106 oveq12d
108 6 65 70 73 90 92 94 104 107 gsumunsn
110 oveq1
112 elun ${⊢}{b}\in \left({d}\cup \left\{{e}\right\}\right)↔\left({b}\in {d}\vee {b}\in \left\{{e}\right\}\right)$
113 velsn ${⊢}{b}\in \left\{{e}\right\}↔{b}={e}$
114 113 orbi2i ${⊢}\left({b}\in {d}\vee {b}\in \left\{{e}\right\}\right)↔\left({b}\in {d}\vee {b}={e}\right)$
115 112 114 bitri ${⊢}{b}\in \left({d}\cup \left\{{e}\right\}\right)↔\left({b}\in {d}\vee {b}={e}\right)$
116 ifbi
117 115 116 ax-mp
118 ringmnd ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Mnd}$
119 68 118 syl ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {R}\in \mathrm{Mnd}$
120 119 3ad2ant1 ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {R}\in \mathrm{Mnd}$
121 simp3 ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {b}\in {N}$
122 97 3ad2ant1 ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}{X}\in {K}$
123 121 122 78 syl2anc
124 elequ1 ${⊢}{b}={e}\to \left({b}\in {d}↔{e}\in {d}\right)$
125 124 biimpac ${⊢}\left({b}\in {d}\wedge {b}={e}\right)\to {e}\in {d}$
126 94 125 nsyl ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to ¬\left({b}\in {d}\wedge {b}={e}\right)$
127 126 3ad2ant1 ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to ¬\left({b}\in {d}\wedge {b}={e}\right)$
128 6 49 65 mndifsplit
129 120 123 127 128 syl3anc
130 117 129 syl5eq
132 131 ifeq1da
133 ovif2
134 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
135 6 5 134 ringridm
136 68 99 135 syl2anc
137 6 5 49 ringrz
138 68 99 137 syl2anc
139 136 138 ifeq12d
140 133 139 syl5eq
141 132 140 eqtr4d
142 141 oveq2d
144 130 143 eqtrd
145 144 ifeq1d
146 145 mpoeq3dva
147 146 fveq2d
148 6 49 ring0cl ${⊢}{R}\in \mathrm{Ring}\to {0}_{{R}}\in {K}$
149 68 148 syl ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {0}_{{R}}\in {K}$
150 149 3ad2ant1 ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {0}_{{R}}\in {K}$
151 123 150 ifcld
152 6 134 ringidcl ${⊢}{R}\in \mathrm{Ring}\to {1}_{{R}}\in {K}$
153 68 152 syl ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {1}_{{R}}\in {K}$
154 153 149 ifcld ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to if\left({b}={e},{1}_{{R}},{0}_{{R}}\right)\in {K}$
155 6 5 ringcl
156 68 99 154 155 syl3anc
158 55 adantr ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {M}:{N}×{N}⟶{K}$
159 158 fovrnda ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {a}{M}{b}\in {K}$
160 159 3impb ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {a}{M}{b}\in {K}$
161 4 6 65 66 71 151 157 160 101 mdetrlin2
162 154 3ad2ant1 ${⊢}\left(\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to if\left({b}={e},{1}_{{R}},{0}_{{R}}\right)\in {K}$
163 4 6 5 66 71 162 160 99 101 mdetrsca2
164 7 adantr ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {M}\in {B}$
165 1 4 2 3 134 49 maducoeval ${⊢}\left({M}\in {B}\wedge {e}\in {N}\wedge {L}\in {N}\right)\to {e}{J}\left({M}\right){L}={D}\left(\left({a}\in {N},{b}\in {N}⟼if\left({a}={L},if\left({b}={e},{1}_{{R}},{0}_{{R}}\right),{a}{M}{b}\right)\right)\right)$
166 164 96 101 165 syl3anc ${⊢}\left({\phi }\wedge \left({d}\subseteq {N}\wedge {e}\in \left({N}\setminus {d}\right)\right)\right)\to {e}{J}\left({M}\right){L}={D}\left(\left({a}\in {N},{b}\in {N}⟼if\left({a}={L},if\left({b}={e},{1}_{{R}},{0}_{{R}}\right),{a}{M}{b}\right)\right)\right)$
167 166 oveq2d
168 163 167 eqtr4d
169 168 oveq2d
170 147 161 169 3eqtrrd
172 109 111 171 3eqtrd
173 172 ex
174 18 26 34 42 64 173 52 findcard2d
175 nfcv
176 nfcsb1v
177 nfcv
178 nfcv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}\left({b}{J}\left({M}\right){L}\right)$
179 176 177 178 nfov
180 csbeq1a
181 oveq1 ${⊢}{i}={b}\to {i}{J}\left({M}\right){L}={b}{J}\left({M}\right){L}$
182 180 181 oveq12d
183 175 179 182 cbvmpt
184 183 oveq2i
185 nfcv ${⊢}\underset{_}{Ⅎ}{a}\phantom{\rule{.4em}{0ex}}if\left({j}={L},{X},{j}{M}{i}\right)$
186 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}if\left({j}={L},{X},{j}{M}{i}\right)$
187 nfcv
188 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{a}={L}$
189 nfcv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}\left({a}{M}{b}\right)$
190 188 176 189 nfif
191 eqeq1 ${⊢}{j}={a}\to \left({j}={L}↔{a}={L}\right)$
192 191 adantr ${⊢}\left({j}={a}\wedge {i}={b}\right)\to \left({j}={L}↔{a}={L}\right)$
194 oveq12 ${⊢}\left({j}={a}\wedge {i}={b}\right)\to {j}{M}{i}={a}{M}{b}$