Metamath Proof Explorer


Theorem smadiadet

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)

Ref Expression
Hypotheses smadiadet.a A=NMatR
smadiadet.b B=BaseA
smadiadet.r RCRing
smadiadet.d D=NmaDetR
smadiadet.h E=NKmaDetR
Assertion smadiadet MBKNEKNsubMatRMK=DKNminMatR1RMK

Proof

Step Hyp Ref Expression
1 smadiadet.a A=NMatR
2 smadiadet.b B=BaseA
3 smadiadet.r RCRing
4 smadiadet.d D=NmaDetR
5 smadiadet.h E=NKmaDetR
6 eqid NsubMatR=NsubMatR
7 1 6 2 submaval MBKNKNKNsubMatRMK=iNK,jNKiMj
8 7 3anidm23 MBKNKNsubMatRMK=iNK,jNKiMj
9 8 fveq2d MBKNEKNsubMatRMK=EiNK,jNKiMj
10 eqid NminMatR1R=NminMatR1R
11 eqid 1R=1R
12 eqid 0R=0R
13 1 2 10 11 12 minmar1val MBKNKNKNminMatR1RMK=iN,jNifi=Kifj=K1R0RiMj
14 13 3anidm23 MBKNKNminMatR1RMK=iN,jNifi=Kifj=K1R0RiMj
15 14 fveq2d MBKNDKNminMatR1RMK=DiN,jNifi=Kifj=K1R0RiMj
16 1 2 3 12 11 marep01ma MBiN,jNifi=Kifj=K1R0RiMjB
17 eqid BaseSymGrpN=BaseSymGrpN
18 eqid ℤRHomR=ℤRHomR
19 eqid pmSgnN=pmSgnN
20 eqid R=R
21 eqid mulGrpR=mulGrpR
22 4 1 2 17 18 19 20 21 mdetleib2 RCRingiN,jNifi=Kifj=K1R0RiMjBDiN,jNifi=Kifj=K1R0RiMj=RpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRnNniN,jNifi=Kifj=K1R0RiMjpn
23 3 16 22 sylancr MBDiN,jNifi=Kifj=K1R0RiMj=RpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRnNniN,jNifi=Kifj=K1R0RiMjpn
24 23 adantr MBKNDiN,jNifi=Kifj=K1R0RiMj=RpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRnNniN,jNifi=Kifj=K1R0RiMjpn
25 eqid BaseR=BaseR
26 eqid +R=+R
27 crngring RCRingRRing
28 ringcmn RRingRCMnd
29 3 27 28 mp2b RCMnd
30 29 a1i MBKNRCMnd
31 1 2 matrcl MBNFinRV
32 31 simpld MBNFin
33 eqid SymGrpN=SymGrpN
34 33 17 symgbasfi NFinBaseSymGrpNFin
35 32 34 syl MBBaseSymGrpNFin
36 35 adantr MBKNBaseSymGrpNFin
37 1 2 3 12 11 17 21 18 19 20 smadiadetlem1 MBKNpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRnNniN,jNifi=Kifj=K1R0RiMjpnBaseR
38 disjdif qBaseSymGrpN|qK=KBaseSymGrpNqBaseSymGrpN|qK=K=
39 38 a1i MBKNqBaseSymGrpN|qK=KBaseSymGrpNqBaseSymGrpN|qK=K=
40 ssrab2 qBaseSymGrpN|qK=KBaseSymGrpN
41 40 a1i MBKNqBaseSymGrpN|qK=KBaseSymGrpN
42 undif qBaseSymGrpN|qK=KBaseSymGrpNqBaseSymGrpN|qK=KBaseSymGrpNqBaseSymGrpN|qK=K=BaseSymGrpN
43 41 42 sylib MBKNqBaseSymGrpN|qK=KBaseSymGrpNqBaseSymGrpN|qK=K=BaseSymGrpN
44 43 eqcomd MBKNBaseSymGrpN=qBaseSymGrpN|qK=KBaseSymGrpNqBaseSymGrpN|qK=K
45 25 26 30 36 37 39 44 gsummptfidmsplit MBKNRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRnNniN,jNifi=Kifj=K1R0RiMjpn=RpqBaseSymGrpN|qK=KℤRHomRpmSgnNpRmulGrpRnNniN,jNifi=Kifj=K1R0RiMjpn+RRpBaseSymGrpNqBaseSymGrpN|qK=KℤRHomRpmSgnNpRmulGrpRnNniN,jNifi=Kifj=K1R0RiMjpn
46 eqid BaseSymGrpNK=BaseSymGrpNK
47 eqid pmSgnNK=pmSgnNK
48 1 2 3 12 11 17 21 18 19 20 46 47 smadiadetlem4 MBKNRpqBaseSymGrpN|qK=KℤRHomRpmSgnNpRmulGrpRnNniN,jNifi=Kifj=K1R0RiMjpn=RpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpn
49 1 2 3 12 11 17 21 18 19 20 smadiadetlem2 MBKNRpBaseSymGrpNqBaseSymGrpN|qK=KℤRHomRpmSgnNpRmulGrpRnNniN,jNifi=Kifj=K1R0RiMjpn=0R
50 48 49 oveq12d MBKNRpqBaseSymGrpN|qK=KℤRHomRpmSgnNpRmulGrpRnNniN,jNifi=Kifj=K1R0RiMjpn+RRpBaseSymGrpNqBaseSymGrpN|qK=KℤRHomRpmSgnNpRmulGrpRnNniN,jNifi=Kifj=K1R0RiMjpn=RpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpn+R0R
51 ringmnd RRingRMnd
52 3 27 51 mp2b RMnd
53 diffi NFinNKFin
54 32 53 syl MBNKFin
55 54 adantr MBKNNKFin
56 eqid SymGrpNK=SymGrpNK
57 56 46 symgbasfi NKFinBaseSymGrpNKFin
58 55 57 syl MBKNBaseSymGrpNKFin
59 simpll MBKNpBaseSymGrpNKMB
60 difssd MBKNpBaseSymGrpNKNKN
61 1 2 submabas MBNKNiNK,jNKiMjBaseNKMatR
62 59 60 61 syl2anc MBKNpBaseSymGrpNKiNK,jNKiMjBaseNKMatR
63 simpr MBKNpBaseSymGrpNKpBaseSymGrpNK
64 eqid NKMatR=NKMatR
65 eqid BaseNKMatR=BaseNKMatR
66 46 47 18 64 65 21 madetsmelbas2 RCRingiNK,jNKiMjBaseNKMatRpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpnBaseR
67 3 62 63 66 mp3an2i MBKNpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpnBaseR
68 67 ralrimiva MBKNpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpnBaseR
69 25 30 58 68 gsummptcl MBKNRpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpnBaseR
70 25 26 12 mndrid RMndRpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpnBaseRRpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpn+R0R=RpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpn
71 52 69 70 sylancr MBKNRpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpn+R0R=RpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpn
72 difssd KNNKN
73 61 3 jctil MBNKNRCRingiNK,jNKiMjBaseNKMatR
74 72 73 sylan2 MBKNRCRingiNK,jNKiMjBaseNKMatR
75 5 64 65 46 18 47 20 21 mdetleib2 RCRingiNK,jNKiMjBaseNKMatREiNK,jNKiMj=RpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpn
76 74 75 syl MBKNEiNK,jNKiMj=RpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpn
77 71 76 eqtr4d MBKNRpBaseSymGrpNKℤRHomRpmSgnNKpRmulGrpRnNKniNK,jNKiMjpn+R0R=EiNK,jNKiMj
78 45 50 77 3eqtrd MBKNRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRnNniN,jNifi=Kifj=K1R0RiMjpn=EiNK,jNKiMj
79 15 24 78 3eqtrd MBKNDKNminMatR1RMK=EiNK,jNKiMj
80 9 79 eqtr4d MBKNEKNsubMatRMK=DKNminMatR1RMK