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

 Description: The determinant of a submatrix of a square matrix obtained by removing a row and a column at the same index equals the determinant of the original matrix with the row replaced with 0's and a 1 at the diagonal position. (Contributed by AV, 31-Jan-2019.) (Proof shortened by AV, 24-Jul-2019.)
Hypotheses
Ref Expression
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
2 eqid 2402 . . . . 5 subMat subMat
41, 2, 3submaval 19267 . . . 4 subMat
543anidm23 1289 . . 3 subMat
65fveq2d 5809 . 2 subMat
7 eqid 2402 . . . . . 6 minMatR1 minMatR1
8 eqid 2402 . . . . . 6
9 eqid 2402 . . . . . 6
101, 3, 7, 8, 9minmar1val 19334 . . . . 5 minMatR1
11103anidm23 1289 . . . 4 minMatR1
1211fveq2d 5809 . . 3 minMatR1
141, 3, 13, 9, 8marep01ma 19346 . . . . 5
16 eqid 2402 . . . . . 6
17 eqid 2402 . . . . . 6 RHom RHom
18 eqid 2402 . . . . . 6 pmSgn pmSgn
19 eqid 2402 . . . . . 6
20 eqid 2402 . . . . . 6 mulGrp mulGrp
2115, 1, 3, 16, 17, 18, 19, 20mdetleib2 19274 . . . . 5 g RHom pmSgnmulGrp g
2213, 14, 21sylancr 661 . . . 4 g RHom pmSgnmulGrp g
2322adantr 463 . . 3 g RHom pmSgnmulGrp g
24 eqid 2402 . . . . 5
25 eqid 2402 . . . . 5
26 crngring 17421 . . . . . . 7
27 ringcmn 17441 . . . . . . 7 CMnd
2813, 26, 27mp2b 10 . . . . . 6 CMnd
2928a1i 11 . . . . 5 CMnd
301, 3matrcl 19098 . . . . . . . 8
3130simpld 457 . . . . . . 7
32 eqid 2402 . . . . . . . 8
3332, 16symgbasfi 16627 . . . . . . 7
3431, 33syl 17 . . . . . 6
3534adantr 463 . . . . 5
361, 3, 13, 9, 8, 16, 20, 17, 18, 19smadiadetlem1 19348 . . . . 5 RHom pmSgnmulGrp g
37 disjdif 3843 . . . . . 6
3837a1i 11 . . . . 5
39 ssrab2 3523 . . . . . . . 8
4039a1i 11 . . . . . . 7
41 undif 3851 . . . . . . 7
4240, 41sylib 196 . . . . . 6
4342eqcomd 2410 . . . . 5
4424, 25, 29, 35, 36, 38, 43gsummptfidmsplit 17165 . . . 4 g RHom pmSgnmulGrp g g RHom pmSgnmulGrp g g RHom pmSgnmulGrp g
45 eqid 2402 . . . . . 6
46 eqid 2402 . . . . . 6 pmSgn pmSgn
471, 3, 13, 9, 8, 16, 20, 17, 18, 19, 45, 46smadiadetlem4 19355 . . . . 5 g RHom pmSgnmulGrp g g RHom pmSgn mulGrp g
481, 3, 13, 9, 8, 16, 20, 17, 18, 19smadiadetlem2 19350 . . . . 5 g RHom pmSgnmulGrp g
4947, 48oveq12d 6252 . . . 4 g RHom pmSgnmulGrp g g RHom pmSgnmulGrp g g RHom pmSgn mulGrp g
50 ringmnd 17419 . . . . . . 7
5113, 26, 50mp2b 10 . . . . . 6
52 diffi 7706 . . . . . . . . . 10
5331, 52syl 17 . . . . . . . . 9
5453adantr 463 . . . . . . . 8
55 eqid 2402 . . . . . . . . 9
5655, 45symgbasfi 16627 . . . . . . . 8
5754, 56syl 17 . . . . . . 7
5813a1i 11 . . . . . . . . 9
59 simpll 752 . . . . . . . . . 10
60 difssd 3570 . . . . . . . . . 10
611, 3submabas 19264 . . . . . . . . . 10 Mat
6259, 60, 61syl2anc 659 . . . . . . . . 9 Mat
63 simpr 459 . . . . . . . . 9
64 eqid 2402 . . . . . . . . . 10 Mat Mat
65 eqid 2402 . . . . . . . . . 10 Mat Mat
6645, 46, 17, 64, 65, 20madetsmelbas2 19151 . . . . . . . . 9 Mat RHom pmSgn mulGrp g
6758, 62, 63, 66syl3anc 1230 . . . . . . . 8 RHom pmSgn mulGrp g
6867ralrimiva 2817 . . . . . . 7 RHom pmSgn mulGrp g
6924, 29, 57, 68gsummptcl 17207 . . . . . 6 g RHom pmSgn mulGrp g
7024, 25, 9mndrid 16158 . . . . . 6 g RHom pmSgn mulGrp g g RHom pmSgn mulGrp g g RHom pmSgn mulGrp g
7151, 69, 70sylancr 661 . . . . 5 g RHom pmSgn mulGrp g g RHom pmSgn mulGrp g
72 difssd 3570 . . . . . . 7
7361, 13jctil 535 . . . . . . 7 Mat
7472, 73sylan2 472 . . . . . 6 Mat