Metamath Proof Explorer


Theorem madugsum

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 Mat R
maduf.j J = N maAdju R
maduf.b B = Base A
madugsum.d D = N maDet R
madugsum.t · ˙ = R
madugsum.k K = Base R
madugsum.m φ M B
madugsum.r φ R CRing
madugsum.x φ i N X K
madugsum.l φ L N
Assertion madugsum φ R i N X · ˙ i J M L = D j N , i N if j = L X j M i

Proof

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