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={\mathrm{Base}}_A$$
	madjusmdet.a	$$⊢A=\left(1\dots N\right)\mathrm{Mat}R$$
	madjusmdet.d	$$⊢D=\left(1\dots N\right)\mathrm{maDet}R$$
	madjusmdet.k	$$⊢K=\left(1\dots N\right)\mathrm{maAdju}R$$
	madjusmdet.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	madjusmdet.z	$$⊢Z=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	madjusmdet.e	$$⊢E=\left(1\dots N-1\right)\mathrm{maDet}R$$
	madjusmdet.n	$$⊢\phi \to N\in \mathbb{N}$$
	madjusmdet.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	madjusmdet.i	$$⊢\phi \to I\in \left(1\dots N\right)$$
	madjusmdet.j	$$⊢\phi \to J\in \left(1\dots N\right)$$
	madjusmdet.m	$$⊢\phi \to M\in B$$
Assertion	madjusmdet	$$⊢\phi \to JK\left(M\right)I=Z\left({\left(-1\right)}^{I+J}\right)\underset{\dot{}}{·}E\left(I{\mathrm{subMat}}_1\left(M\right)J\right)$$

Proof

Step	Hyp	Ref	Expression
1		madjusmdet.b	$$⊢B={\mathrm{Base}}_A$$
2		madjusmdet.a	$$⊢A=\left(1\dots N\right)\mathrm{Mat}R$$
3		madjusmdet.d	$$⊢D=\left(1\dots N\right)\mathrm{maDet}R$$
4		madjusmdet.k	$$⊢K=\left(1\dots N\right)\mathrm{maAdju}R$$
5		madjusmdet.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6		madjusmdet.z	$$⊢Z=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
7		madjusmdet.e	$$⊢E=\left(1\dots N-1\right)\mathrm{maDet}R$$
8		madjusmdet.n	$$⊢\phi \to N\in \mathbb{N}$$
9		madjusmdet.r	$$⊢\phi \to R\in \mathrm{CRing}$$
10		madjusmdet.i	$$⊢\phi \to I\in \left(1\dots N\right)$$
11		madjusmdet.j	$$⊢\phi \to J\in \left(1\dots N\right)$$
12		madjusmdet.m	$$⊢\phi \to M\in B$$
13		eqeq1	$$⊢k=i\to \left(k=1\leftrightarrow i=1\right)$$
14		breq1	$$⊢k=i\to \left(k\le I\leftrightarrow i\le I\right)$$
15		oveq1	$$⊢k=i\to k-1=i-1$$
16		id	$$⊢k=i\to k=i$$
17	14 15 16	ifbieq12d	$$⊢k=i\to if\left(k\le I,k-1,k\right)=if\left(i\le I,i-1,i\right)$$
18	13 17	ifbieq2d	$$⊢k=i\to if\left(k=1,I,if\left(k\le I,k-1,k\right)\right)=if\left(i=1,I,if\left(i\le I,i-1,i\right)\right)$$
19	18	cbvmptv	$$⊢\left(k\in \left(1\dots N\right)⟼if\left(k=1,I,if\left(k\le I,k-1,k\right)\right)\right)=\left(i\in \left(1\dots N\right)⟼if\left(i=1,I,if\left(i\le I,i-1,i\right)\right)\right)$$
20		breq1	$$⊢k=i\to \left(k\le N\leftrightarrow i\le N\right)$$
21	20 15 16	ifbieq12d	$$⊢k=i\to if\left(k\le N,k-1,k\right)=if\left(i\le N,i-1,i\right)$$
22	13 21	ifbieq2d	$$⊢k=i\to if\left(k=1,N,if\left(k\le N,k-1,k\right)\right)=if\left(i=1,N,if\left(i\le N,i-1,i\right)\right)$$
23	22	cbvmptv	$$⊢\left(k\in \left(1\dots N\right)⟼if\left(k=1,N,if\left(k\le N,k-1,k\right)\right)\right)=\left(i\in \left(1\dots N\right)⟼if\left(i=1,N,if\left(i\le N,i-1,i\right)\right)\right)$$
24		eqeq1	$$⊢l=j\to \left(l=1\leftrightarrow j=1\right)$$
25		breq1	$$⊢l=j\to \left(l\le J\leftrightarrow j\le J\right)$$
26		oveq1	$$⊢l=j\to l-1=j-1$$
27		id	$$⊢l=j\to l=j$$
28	25 26 27	ifbieq12d	$$⊢l=j\to if\left(l\le J,l-1,l\right)=if\left(j\le J,j-1,j\right)$$
29	24 28	ifbieq2d	$$⊢l=j\to if\left(l=1,J,if\left(l\le J,l-1,l\right)\right)=if\left(j=1,J,if\left(j\le J,j-1,j\right)\right)$$
30	29	cbvmptv	$$⊢\left(l\in \left(1\dots N\right)⟼if\left(l=1,J,if\left(l\le J,l-1,l\right)\right)\right)=\left(j\in \left(1\dots N\right)⟼if\left(j=1,J,if\left(j\le J,j-1,j\right)\right)\right)$$
31		breq1	$$⊢l=j\to \left(l\le N\leftrightarrow j\le N\right)$$
32	31 26 27	ifbieq12d	$$⊢l=j\to if\left(l\le N,l-1,l\right)=if\left(j\le N,j-1,j\right)$$
33	24 32	ifbieq2d	$$⊢l=j\to if\left(l=1,N,if\left(l\le N,l-1,l\right)\right)=if\left(j=1,N,if\left(j\le N,j-1,j\right)\right)$$
34	33	cbvmptv	$$⊢\left(l\in \left(1\dots N\right)⟼if\left(l=1,N,if\left(l\le N,l-1,l\right)\right)\right)=\left(j\in \left(1\dots N\right)⟼if\left(j=1,N,if\left(j\le N,j-1,j\right)\right)\right)$$
35	1 2 3 4 5 6 7 8 9 10 11 12 19 23 30 34	madjusmdetlem4	$$⊢\phi \to JK\left(M\right)I=Z\left({\left(-1\right)}^{I+J}\right)\underset{\dot{}}{·}E\left(I{\mathrm{subMat}}_1\left(M\right)J\right)$$