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 = N Mat R
smadiadet.b ⊢ B = Base A
smadiadet.r ⊢ R ∈ CRing
smadiadet.d ⊢ D = N maDet R
smadiadet.h ⊢ E = N ∖ K maDet R
Assertion smadiadet ⊢ M ∈ B ∧ K ∈ N → E ⁡ K N subMat R ⁡ M K = D ⁡ K N minMatR1 R ⁡ M K

Proof

Step Hyp Ref Expression
1 smadiadet.a ⊢ A = N Mat R
2 smadiadet.b ⊢ B = Base A
3 smadiadet.r ⊢ R ∈ CRing
4 smadiadet.d ⊢ D = N maDet R
5 smadiadet.h ⊢ E = N ∖ K maDet R
6 eqid ⊢ N subMat R = N subMat R
7 1 6 2 submaval ⊢ M ∈ B ∧ K ∈ N ∧ K ∈ N → K N subMat R ⁡ M K = i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j
8 7 3anidm23 ⊢ M ∈ B ∧ K ∈ N → K N subMat R ⁡ M K = i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j
9 8 fveq2d ⊢ M ∈ B ∧ K ∈ N → E ⁡ K N subMat R ⁡ M K = E ⁡ i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j
10 eqid ⊢ N minMatR1 R = N minMatR1 R
11 eqid ⊢ 1 R = 1 R
12 eqid ⊢ 0 R = 0 R
13 1 2 10 11 12 minmar1val ⊢ M ∈ B ∧ K ∈ N ∧ K ∈ N → K N minMatR1 R ⁡ M K = i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j
14 13 3anidm23 ⊢ M ∈ B ∧ K ∈ N → K N minMatR1 R ⁡ M K = i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j
15 14 fveq2d ⊢ M ∈ B ∧ K ∈ N → D ⁡ K N minMatR1 R ⁡ M K = D ⁡ i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j
16 1 2 3 12 11 marep01ma ⊢ M ∈ B → i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j ∈ B
17 eqid ⊢ Base SymGrp ⁡ N = Base SymGrp ⁡ N
18 eqid ⊢ ℤRHom ⁡ R = ℤRHom ⁡ R
19 eqid ⊢ pmSgn ⁡ N = pmSgn ⁡ N
20 eqid ⊢ ⋅ R = ⋅ R
21 eqid ⊢ mulGrp R = mulGrp R
22 4 1 2 17 18 19 20 21 mdetleib2 ⊢ R ∈ CRing ∧ i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j ∈ B → D ⁡ i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j = ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j p ⁡ n
23 3 16 22 sylancr ⊢ M ∈ B → D ⁡ i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j = ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j p ⁡ n
24 23 adantr ⊢ M ∈ B ∧ K ∈ N → D ⁡ i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j = ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j p ⁡ n
25 eqid ⊢ Base R = Base R
26 eqid ⊢ + R = + R
27 crngring ⊢ R ∈ CRing → R ∈ Ring
28 ringcmn ⊢ R ∈ Ring → R ∈ CMnd
29 3 27 28 mp2b ⊢ R ∈ CMnd
30 29 a1i ⊢ M ∈ B ∧ K ∈ N → R ∈ CMnd
31 1 2 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
32 31 simpld ⊢ M ∈ B → N ∈ Fin
33 eqid ⊢ SymGrp ⁡ N = SymGrp ⁡ N
34 33 17 symgbasfi ⊢ N ∈ Fin → Base SymGrp ⁡ N ∈ Fin
35 32 34 syl ⊢ M ∈ B → Base SymGrp ⁡ N ∈ Fin
36 35 adantr ⊢ M ∈ B ∧ K ∈ N → Base SymGrp ⁡ N ∈ Fin
37 1 2 3 12 11 17 21 18 19 20 smadiadetlem1 ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ Base SymGrp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j p ⁡ n ∈ Base R
38 disjdif ⊢ q ∈ Base SymGrp ⁡ N | q ⁡ K = K ∩ Base SymGrp ⁡ N ∖ q ∈ Base SymGrp ⁡ N | q ⁡ K = K = ∅
39 38 a1i ⊢ M ∈ B ∧ K ∈ N → q ∈ Base SymGrp ⁡ N | q ⁡ K = K ∩ Base SymGrp ⁡ N ∖ q ∈ Base SymGrp ⁡ N | q ⁡ K = K = ∅
40 ssrab2 ⊢ q ∈ Base SymGrp ⁡ N | q ⁡ K = K ⊆ Base SymGrp ⁡ N
41 40 a1i ⊢ M ∈ B ∧ K ∈ N → q ∈ Base SymGrp ⁡ N | q ⁡ K = K ⊆ Base SymGrp ⁡ N
42 undif ⊢ q ∈ Base SymGrp ⁡ N | q ⁡ K = K ⊆ Base SymGrp ⁡ N ↔ q ∈ Base SymGrp ⁡ N | q ⁡ K = K ∪ Base SymGrp ⁡ N ∖ q ∈ Base SymGrp ⁡ N | q ⁡ K = K = Base SymGrp ⁡ N
43 41 42 sylib ⊢ M ∈ B ∧ K ∈ N → q ∈ Base SymGrp ⁡ N | q ⁡ K = K ∪ Base SymGrp ⁡ N ∖ q ∈ Base SymGrp ⁡ N | q ⁡ K = K = Base SymGrp ⁡ N
44 43 eqcomd ⊢ M ∈ B ∧ K ∈ N → Base SymGrp ⁡ N = q ∈ Base SymGrp ⁡ N | q ⁡ K = K ∪ Base SymGrp ⁡ N ∖ q ∈ Base SymGrp ⁡ N | q ⁡ K = K
45 25 26 30 36 37 39 44 gsummptfidmsplit ⊢ M ∈ B ∧ K ∈ N → ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j p ⁡ n = ∑ R p ∈ q ∈ Base SymGrp ⁡ N | q ⁡ K = K ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j p ⁡ n + R ∑ R p ∈ Base SymGrp ⁡ N ∖ q ∈ Base SymGrp ⁡ N | q ⁡ K = K ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j p ⁡ n
46 eqid ⊢ Base SymGrp ⁡ N ∖ K = Base SymGrp ⁡ N ∖ K
47 eqid ⊢ pmSgn ⁡ N ∖ K = pmSgn ⁡ N ∖ K
48 1 2 3 12 11 17 21 18 19 20 46 47 smadiadetlem4 ⊢ M ∈ B ∧ K ∈ N → ∑ R p ∈ q ∈ Base SymGrp ⁡ N | q ⁡ K = K ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j p ⁡ n = ∑ R p ∈ Base SymGrp ⁡ N ∖ K ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
49 1 2 3 12 11 17 21 18 19 20 smadiadetlem2 ⊢ M ∈ B ∧ K ∈ N → ∑ R p ∈ Base SymGrp ⁡ N ∖ q ∈ Base SymGrp ⁡ N | q ⁡ K = K ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j p ⁡ n = 0 R
50 48 49 oveq12d ⊢ M ∈ B ∧ K ∈ N → ∑ R p ∈ q ∈ Base SymGrp ⁡ N | q ⁡ K = K ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j p ⁡ n + R ∑ R p ∈ Base SymGrp ⁡ N ∖ q ∈ Base SymGrp ⁡ N | q ⁡ K = K ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j p ⁡ n = ∑ R p ∈ Base SymGrp ⁡ N ∖ K ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n + R 0 R
51 ringmnd ⊢ R ∈ Ring → R ∈ Mnd
52 3 27 51 mp2b ⊢ R ∈ Mnd
53 diffi ⊢ N ∈ Fin → N ∖ K ∈ Fin
54 32 53 syl ⊢ M ∈ B → N ∖ K ∈ Fin
55 54 adantr ⊢ M ∈ B ∧ K ∈ N → N ∖ K ∈ Fin
56 eqid ⊢ SymGrp ⁡ N ∖ K = SymGrp ⁡ N ∖ K
57 56 46 symgbasfi ⊢ N ∖ K ∈ Fin → Base SymGrp ⁡ N ∖ K ∈ Fin
58 55 57 syl ⊢ M ∈ B ∧ K ∈ N → Base SymGrp ⁡ N ∖ K ∈ Fin
59 simpll ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ Base SymGrp ⁡ N ∖ K → M ∈ B
60 difssd ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ Base SymGrp ⁡ N ∖ K → N ∖ K ⊆ N
61 1 2 submabas ⊢ M ∈ B ∧ N ∖ K ⊆ N → i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j ∈ Base N ∖ K Mat R
62 59 60 61 syl2anc ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ Base SymGrp ⁡ N ∖ K → i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j ∈ Base N ∖ K Mat R
63 simpr ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ Base SymGrp ⁡ N ∖ K → p ∈ Base SymGrp ⁡ N ∖ K
64 eqid ⊢ N ∖ K Mat R = N ∖ K Mat R
65 eqid ⊢ Base N ∖ K Mat R = Base N ∖ K Mat R
66 46 47 18 64 65 21 madetsmelbas2 ⊢ R ∈ CRing ∧ i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j ∈ Base N ∖ K Mat R ∧ p ∈ Base SymGrp ⁡ N ∖ K → ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ∈ Base R
67 3 62 63 66 mp3an2i ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ Base SymGrp ⁡ N ∖ K → ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ∈ Base R
68 67 ralrimiva ⊢ M ∈ B ∧ K ∈ N → ∀ p ∈ Base SymGrp ⁡ N ∖ K ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ∈ Base R
69 25 30 58 68 gsummptcl ⊢ M ∈ B ∧ K ∈ N → ∑ R p ∈ Base SymGrp ⁡ N ∖ K ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ∈ Base R
70 25 26 12 mndrid ⊢ R ∈ Mnd ∧ ∑ R p ∈ Base SymGrp ⁡ N ∖ K ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ∈ Base R → ∑ R p ∈ Base SymGrp ⁡ N ∖ K ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n + R 0 R = ∑ R p ∈ Base SymGrp ⁡ N ∖ K ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
71 52 69 70 sylancr ⊢ M ∈ B ∧ K ∈ N → ∑ R p ∈ Base SymGrp ⁡ N ∖ K ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n + R 0 R = ∑ R p ∈ Base SymGrp ⁡ N ∖ K ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
72 difssd ⊢ K ∈ N → N ∖ K ⊆ N
73 61 3 jctil ⊢ M ∈ B ∧ N ∖ K ⊆ N → R ∈ CRing ∧ i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j ∈ Base N ∖ K Mat R
74 72 73 sylan2 ⊢ M ∈ B ∧ K ∈ N → R ∈ CRing ∧ i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j ∈ Base N ∖ K Mat R
75 5 64 65 46 18 47 20 21 mdetleib2 ⊢ R ∈ CRing ∧ i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j ∈ Base N ∖ K Mat R → E ⁡ i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j = ∑ R p ∈ Base SymGrp ⁡ N ∖ K ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
76 74 75 syl ⊢ M ∈ B ∧ K ∈ N → E ⁡ i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j = ∑ R p ∈ Base SymGrp ⁡ N ∖ K ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
77 71 76 eqtr4d ⊢ M ∈ B ∧ K ∈ N → ∑ R p ∈ Base SymGrp ⁡ N ∖ K ℤRHom ⁡ R ∘ pmSgn ⁡ N ∖ K ⁡ p ⋅ R ∑ mulGrp R n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n + R 0 R = E ⁡ i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j
78 45 50 77 3eqtrd ⊢ M ∈ B ∧ K ∈ N → ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 R 0 R i M j p ⁡ n = E ⁡ i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j
79 15 24 78 3eqtrd ⊢ M ∈ B ∧ K ∈ N → D ⁡ K N minMatR1 R ⁡ M K = E ⁡ i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j
80 9 79 eqtr4d ⊢ M ∈ B ∧ K ∈ N → E ⁡ K N subMat R ⁡ M K = D ⁡ K N minMatR1 R ⁡ M K