Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  madugsum Structured version   Unicode version

 Description: The determinant of a matrix with a row consisting of the same element is the sum of the elements of the -th column of the adjunct of the matrix multiplied with . (Contributed by Stefan O'Rear, 16-Jul-2018.)
Hypotheses
Ref Expression
Assertion
Ref Expression
Distinct variable groups:   ,,   ,,   ,,   ,,   ,   ,,   ,,   ,   ,   ,,
Allowed substitution hints:   (,)   (,)   ()   ()   ()

Proof of Theorem madugsum
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mpteq1 4527 . . . . 5
21oveq2d 6298 . . . 4 g g
3 eleq2 2540 . . . . . . . 8
43ifbid 3961 . . . . . . 7
54ifeq1d 3957 . . . . . 6
65mpt2eq3dv 6345 . . . . 5
76fveq2d 5868 . . . 4
82, 7eqeq12d 2489 . . 3 g g
9 mpteq1 4527 . . . . 5
109oveq2d 6298 . . . 4 g g
11 eleq2 2540 . . . . . . . 8
1211ifbid 3961 . . . . . . 7
1312ifeq1d 3957 . . . . . 6
1413mpt2eq3dv 6345 . . . . 5
1514fveq2d 5868 . . . 4
1610, 15eqeq12d 2489 . . 3 g g
17 mpteq1 4527 . . . . 5
1817oveq2d 6298 . . . 4 g g
19 eleq2 2540 . . . . . . . 8
2019ifbid 3961 . . . . . . 7
2120ifeq1d 3957 . . . . . 6
2221mpt2eq3dv 6345 . . . . 5
2322fveq2d 5868 . . . 4
2418, 23eqeq12d 2489 . . 3 g g
25 mpteq1 4527 . . . . 5
2625oveq2d 6298 . . . 4 g g
27 eleq2 2540 . . . . . . . 8
2827ifbid 3961 . . . . . . 7
2928ifeq1d 3957 . . . . . 6
3029mpt2eq3dv 6345 . . . . 5
3130fveq2d 5868 . . . 4
3226, 31eqeq12d 2489 . . 3 g g
33 noel 3789 . . . . . . . . 9
34 iffalse 3948 . . . . . . . . 9
3533, 34mp1i 12 . . . . . . . 8
3635ifeq1d 3957 . . . . . . 7
3736mpt2eq3ia 6344 . . . . . 6
3837fveq2i 5867 . . . . 5
39 madugsum.d . . . . . 6 maDet
40 madugsum.k . . . . . 6
41 eqid 2467 . . . . . 6
42 madugsum.r . . . . . 6
43 madugsum.m . . . . . . . 8
44 maduf.a . . . . . . . . 9 Mat
45 maduf.b . . . . . . . . 9
4644, 45matrcl 18681 . . . . . . . 8
4743, 46syl 16 . . . . . . 7
4847simpld 459 . . . . . 6
4944, 40, 45matbas2i 18691 . . . . . . . . 9
50 elmapi 7437 . . . . . . . . 9
5143, 49, 503syl 20 . . . . . . . 8
5251fovrnda 6428 . . . . . . 7
53523impb 1192 . . . . . 6
54 madugsum.l . . . . . 6
5539, 40, 41, 42, 48, 53, 54mdetr0 18874 . . . . 5
5638, 55syl5eq 2520 . . . 4
57 mpt0 5706 . . . . . 6
5857oveq2i 6293 . . . . 5 g g
5941gsum0 15823 . . . . 5 g
6058, 59eqtri 2496 . . . 4 g
6156, 60syl6reqr 2527 . . 3 g
62 eqid 2467 . . . . . . 7
6342adantr 465 . . . . . . . . 9
64 crngrng 16996 . . . . . . . . 9
6563, 64syl 16 . . . . . . . 8
66 rngcmn 17016 . . . . . . . 8 CMnd
6765, 66syl 16 . . . . . . 7 CMnd
6848adantr 465 . . . . . . . 8
69 simprl 755 . . . . . . . 8
70 ssfi 7737 . . . . . . . 8
7168, 69, 70syl2anc 661 . . . . . . 7
7265adantr 465 . . . . . . . 8
7369sselda 3504 . . . . . . . . 9
74 madugsum.x . . . . . . . . . . 11
7574ralrimiva 2878 . . . . . . . . . 10
7675ad2antrr 725 . . . . . . . . 9
77 rspcsbela 3853 . . . . . . . . 9
7873, 76, 77syl2anc 661 . . . . . . . 8
79 maduf.j . . . . . . . . . . . . . 14 maAdju
8044, 79, 45maduf 18910 . . . . . . . . . . . . 13
8142, 80syl 16 . . . . . . . . . . . 12
8281, 43ffvelrnd 6020 . . . . . . . . . . 11
8344, 40, 45matbas2i 18691 . . . . . . . . . . 11
84 elmapi 7437 . . . . . . . . . . 11
8582, 83, 843syl 20 . . . . . . . . . 10
8685ad2antrr 725 . . . . . . . . 9
8754ad2antrr 725 . . . . . . . . 9
8886, 73, 87fovrnd 6429 . . . . . . . 8
89 madugsum.t . . . . . . . . 9
9040, 89rngcl 16999 . . . . . . . 8
9172, 78, 88, 90syl3anc 1228 . . . . . . 7
92 vex 3116 . . . . . . . 8
9392a1i 11 . . . . . . 7
94 eldifn 3627 . . . . . . . 8
9594ad2antll 728 . . . . . . 7
96 eldifi 3626 . . . . . . . . . 10
9796ad2antll 728 . . . . . . . . 9
9875adantr 465 . . . . . . . . 9
99 rspcsbela 3853 . . . . . . . . 9
10097, 98, 99syl2anc 661 . . . . . . . 8
10185adantr 465 . . . . . . . . 9
10254adantr 465 . . . . . . . . 9
103101, 97, 102fovrnd 6429 . . . . . . . 8
10440, 89rngcl 16999 . . . . . . . 8
10565, 100, 103, 104syl3anc 1228 . . . . . . 7
106 csbeq1 3438 . . . . . . . 8
107 oveq1 6289 . . . . . . . 8
108106, 107oveq12d 6300 . . . . . . 7
10940, 62, 67, 71, 91, 93, 95, 105, 108gsumunsn 16777 . . . . . 6 g g
110109adantr 465 . . . . 5 g g g
111 oveq1 6289 . . . . . 6 g g
112111adantl 466 . . . . 5 g g
113 elun 3645 . . . . . . . . . . . . . 14
114 elsn 4041 . . . . . . . . . . . . . . 15
115114orbi2i 519 . . . . . . . . . . . . . 14
116113, 115bitri 249 . . . . . . . . . . . . 13
117 ifbi 3960 . . . . . . . . . . . . 13
118116, 117ax-mp 5 . . . . . . . . . . . 12
119 rngmnd 16995 . . . . . . . . . . . . . . 15
12065, 119syl 16 . . . . . . . . . . . . . 14
1211203ad2ant1 1017 . . . . . . . . . . . . 13
122 simp3 998 . . . . . . . . . . . . . 14
123983ad2ant1 1017 . . . . . . . . . . . . . 14
124122, 123, 77syl2anc 661 . . . . . . . . . . . . 13
125 elequ1 1770 . . . . . . . . . . . . . . . 16
126125biimpac 486 . . . . . . . . . . . . . . 15
12795, 126nsyl 121 . . . . . . . . . . . . . 14
1281273ad2ant1 1017 . . . . . . . . . . . . 13
12940, 41, 62mndifsplit 18905 . . . . . . . . . . . . 13
130121, 124, 128, 129syl3anc 1228 . . . . . . . . . . . 12
131118, 130syl5eq 2520 . . . . . . . . . . 11
132106adantl 466 . . . . . . . . . . . . . . 15
133132ifeq1da 3969 . . . . . . . . . . . . . 14
134 oveq2 6290 . . . . . . . . . . . . . . . 16
135 oveq2 6290 . . . . . . . . . . . . . . . 16
136134, 135ifsb 3952 . . . . . . . . . . . . . . 15
137 eqid 2467 . . . . . . . . . . . . . . . . . 18
13840, 89, 137rngridm 17010 . . . . . . . . . . . . . . . . 17
13965, 100, 138syl2anc 661 . . . . . . . . . . . . . . . 16
14040, 89, 41rngrz 17023 . . . . . . . . . . . . . . . . 17
14165, 100, 140syl2anc 661 . . . . . . . . . . . . . . . 16
142139, 141ifeq12d 3959 . . . . . . . . . . . . . . 15
143136, 142syl5eq 2520 . . . . . . . . . . . . . 14
144133, 143eqtr4d 2511 . . . . . . . . . . . . 13
145144oveq2d 6298 . . . . . . . . . . . 12
1461453ad2ant1 1017 . . . . . . . . . . 11
147131, 146eqtrd 2508 . . . . . . . . . 10
148147ifeq1d 3957 . . . . . . . . 9
149148mpt2eq3dva 6343 . . . . . . . 8
150149fveq2d 5868 . . . . . . 7
15140, 41rng0cl 17007 . . . . . . . . . . 11
15265, 151syl 16 . . . . . . . . . 10
1531523ad2ant1 1017 . . . . . . . . 9
154124, 153ifcld 3982 . . . . . . . 8
15540, 137rngidcl 17006 . . . . . . . . . . . 12
15665, 155syl 16 . . . . . . . . . . 11
157156, 152ifcld 3982 . . . . . . . . . 10
15840, 89rngcl 16999 . . . . . . . . . 10
15965, 100, 157, 158syl3anc 1228 . . . . . . . . 9
1601593ad2ant1 1017 . . . . . . . 8
16151adantr 465 . . . . . . . . . 10
162161fovrnda 6428 . . . . . . . . 9
1631623impb 1192 . . . . . . . 8
16439, 40, 62, 63, 68, 154, 160, 163, 102mdetrlin2 18876 . . . . . . 7
1651573ad2ant1 1017 . . . . . . . . . 10
16639, 40, 89, 63, 68, 165, 163, 100, 102mdetrsca2 18873 . . . . . . . . 9
16743adantr 465 . . . . . . . . . . 11
16844, 39, 79, 45, 137, 41maducoeval 18908 . . . . . . . . . . 11
169167, 97, 102, 168syl3anc 1228 . . . . . . . . . 10
170169oveq2d 6298 . . . . . . . . 9
171166, 170eqtr4d 2511 . . . . . . . 8
172171oveq2d 6298 . . . . . . 7
173150, 164, 1723eqtrrd 2513 . . . . . 6
174173adantr 465 . . . . 5 g
175110, 112, 1743eqtrd 2512 . . . 4 g g
176175ex 434 . . 3 g g
1778, 16, 24, 32, 61, 176, 48findcard2d 7758 . 2 g
178 nfcv 2629 . . . 4
179 nfcsb1v 3451 . . . . 5
180 nfcv 2629 . . . . 5
181 nfcv 2629 . . . . 5
182179, 180, 181nfov 6305 . . . 4
183 csbeq1a 3444 . . . . 5
184 oveq1 6289 . . . . 5
185183, 184oveq12d 6300 . . . 4
186178, 182, 185cbvmpt 4537 . . 3
187186oveq2i 6293 . 2 g g
188 nfcv 2629 . . . . 5
189 nfcv 2629 . . . . 5
190 nfcv 2629 . . . . 5
191 nfv 1683 . . . . . 6
192 nfcv 2629 . . . . . 6
193191, 179, 192nfif 3968 . . . . 5
194 eqeq1 2471 . . . . . . 7
195194adantr 465 . . . . . 6
196183adantl 466 . . . . . 6
197 oveq12 6291 . . . . . 6
198195, 196, 197ifbieq12d 3966 . . . . 5
199188, 189, 190, 193, 198cbvmpt2 6358 . . . 4
200 iftrue 3945 . . . . . . . 8
201200eqcomd 2475 . . . . . . 7
202201adantl 466 . . . . . 6
203202ifeq1d 3957 . . . . 5
204203mpt2eq3ia 6344 . . . 4
205199, 204eqtri 2496 . . 3
206205fveq2i 5867 . 2
207177, 187, 2063eqtr4g 2533 1 g