Metamath Proof Explorer

Theorem madjusmdet

Description: Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrices. (Contributed by Thierry Arnoux, 23-Aug-2020)

Ref Expression
Hypotheses madjusmdet.b ⊢ B = Base A
madjusmdet.a ⊢ A = 1 … N Mat R
madjusmdet.d ⊢ D = 1 … N maDet R
madjusmdet.k ⊢ K = 1 … N maAdju R
madjusmdet.t ⊢ · ˙ = ⋅ R
madjusmdet.z ⊢ Z = ℤRHom ⁡ R
madjusmdet.e ⊢ E = 1 … N − 1 maDet R
madjusmdet.n ⊢ φ → N ∈ ℕ
madjusmdet.r ⊢ φ → R ∈ CRing
madjusmdet.i ⊢ φ → I ∈ 1 … N
madjusmdet.j ⊢ φ → J ∈ 1 … N
madjusmdet.m ⊢ φ → M ∈ B
Assertion madjusmdet ⊢ φ → J K ⁡ M I = Z ⁡ − 1 I + J · ˙ E ⁡ I subMat 1 ⁡ M J

Proof

Step Hyp Ref Expression
1 madjusmdet.b ⊢ B = Base A
2 madjusmdet.a ⊢ A = 1 … N Mat R
3 madjusmdet.d ⊢ D = 1 … N maDet R
4 madjusmdet.k ⊢ K = 1 … N maAdju R
5 madjusmdet.t ⊢ · ˙ = ⋅ R
6 madjusmdet.z ⊢ Z = ℤRHom ⁡ R
7 madjusmdet.e ⊢ E = 1 … N − 1 maDet R
8 madjusmdet.n ⊢ φ → N ∈ ℕ
9 madjusmdet.r ⊢ φ → R ∈ CRing
10 madjusmdet.i ⊢ φ → I ∈ 1 … N
11 madjusmdet.j ⊢ φ → J ∈ 1 … N
12 madjusmdet.m ⊢ φ → M ∈ B
13 eqeq1 ⊢ k = i → k = 1 ↔ i = 1
14 breq1 ⊢ k = i → k ≤ I ↔ i ≤ I
15 oveq1 ⊢ k = i → k − 1 = i − 1
16 id ⊢ k = i → k = i
17 14 15 16 ifbieq12d ⊢ k = i → if k ≤ I k − 1 k = if i ≤ I i − 1 i
18 13 17 ifbieq2d ⊢ k = i → if k = 1 I if k ≤ I k − 1 k = if i = 1 I if i ≤ I i − 1 i
19 18 cbvmptv ⊢ k ∈ 1 … N ⟼ if k = 1 I if k ≤ I k − 1 k = i ∈ 1 … N ⟼ if i = 1 I if i ≤ I i − 1 i
20 breq1 ⊢ k = i → k ≤ N ↔ i ≤ N
21 20 15 16 ifbieq12d ⊢ k = i → if k ≤ N k − 1 k = if i ≤ N i − 1 i
22 13 21 ifbieq2d ⊢ k = i → if k = 1 N if k ≤ N k − 1 k = if i = 1 N if i ≤ N i − 1 i
23 22 cbvmptv ⊢ k ∈ 1 … N ⟼ if k = 1 N if k ≤ N k − 1 k = i ∈ 1 … N ⟼ if i = 1 N if i ≤ N i − 1 i
24 eqeq1 ⊢ l = j → l = 1 ↔ j = 1
25 breq1 ⊢ l = j → l ≤ J ↔ j ≤ J
26 oveq1 ⊢ l = j → l − 1 = j − 1
27 id ⊢ l = j → l = j
28 25 26 27 ifbieq12d ⊢ l = j → if l ≤ J l − 1 l = if j ≤ J j − 1 j
29 24 28 ifbieq2d ⊢ l = j → if l = 1 J if l ≤ J l − 1 l = if j = 1 J if j ≤ J j − 1 j
30 29 cbvmptv ⊢ l ∈ 1 … N ⟼ if l = 1 J if l ≤ J l − 1 l = j ∈ 1 … N ⟼ if j = 1 J if j ≤ J j − 1 j
31 breq1 ⊢ l = j → l ≤ N ↔ j ≤ N
32 31 26 27 ifbieq12d ⊢ l = j → if l ≤ N l − 1 l = if j ≤ N j − 1 j
33 24 32 ifbieq2d ⊢ l = j → if l = 1 N if l ≤ N l − 1 l = if j = 1 N if j ≤ N j − 1 j
34 33 cbvmptv ⊢ l ∈ 1 … N ⟼ if l = 1 N if l ≤ N l − 1 l = j ∈ 1 … N ⟼ if j = 1 N if j ≤ N j − 1 j
35 1 2 3 4 5 6 7 8 9 10 11 12 19 23 30 34 madjusmdetlem4 ⊢ φ → J K ⁡ M I = Z ⁡ − 1 I + J · ˙ E ⁡ I subMat 1 ⁡ M J