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	⊢ 𝐵 = ( Base ‘ 𝐴 )
	madjusmdet.a	⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
	madjusmdet.d	⊢ 𝐷 = ( ( 1 ... 𝑁 ) maDet 𝑅 )
	madjusmdet.k	⊢ 𝐾 = ( ( 1 ... 𝑁 ) maAdju 𝑅 )
	madjusmdet.t	⊢ · = ( .r ‘ 𝑅 )
	madjusmdet.z	⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
	madjusmdet.e	⊢ 𝐸 = ( ( 1 ... ( 𝑁 − 1 ) ) maDet 𝑅 )
	madjusmdet.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	madjusmdet.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	madjusmdet.i	⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
	madjusmdet.j	⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
	madjusmdet.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
Assertion	madjusmdet	⊢ ( 𝜑 → ( 𝐽 ( 𝐾 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝐽 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		madjusmdet.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
2		madjusmdet.a	⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
3		madjusmdet.d	⊢ 𝐷 = ( ( 1 ... 𝑁 ) maDet 𝑅 )
4		madjusmdet.k	⊢ 𝐾 = ( ( 1 ... 𝑁 ) maAdju 𝑅 )
5		madjusmdet.t	⊢ · = ( .r ‘ 𝑅 )
6		madjusmdet.z	⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
7		madjusmdet.e	⊢ 𝐸 = ( ( 1 ... ( 𝑁 − 1 ) ) maDet 𝑅 )
8		madjusmdet.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9		madjusmdet.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
10		madjusmdet.i	⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
11		madjusmdet.j	⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
12		madjusmdet.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
13		eqeq1	⊢ ( 𝑘 = 𝑖 → ( 𝑘 = 1 ↔ 𝑖 = 1 ) )
14		breq1	⊢ ( 𝑘 = 𝑖 → ( 𝑘 ≤ 𝐼 ↔ 𝑖 ≤ 𝐼 ) )
15		oveq1	⊢ ( 𝑘 = 𝑖 → ( 𝑘 − 1 ) = ( 𝑖 − 1 ) )
16		id	⊢ ( 𝑘 = 𝑖 → 𝑘 = 𝑖 )
17	14 15 16	ifbieq12d	⊢ ( 𝑘 = 𝑖 → if ( 𝑘 ≤ 𝐼 , ( 𝑘 − 1 ) , 𝑘 ) = if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) )
18	13 17	ifbieq2d	⊢ ( 𝑘 = 𝑖 → if ( 𝑘 = 1 , 𝐼 , if ( 𝑘 ≤ 𝐼 , ( 𝑘 − 1 ) , 𝑘 ) ) = if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) )
19	18	cbvmptv	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑘 = 1 , 𝐼 , if ( 𝑘 ≤ 𝐼 , ( 𝑘 − 1 ) , 𝑘 ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) )
20		breq1	⊢ ( 𝑘 = 𝑖 → ( 𝑘 ≤ 𝑁 ↔ 𝑖 ≤ 𝑁 ) )
21	20 15 16	ifbieq12d	⊢ ( 𝑘 = 𝑖 → if ( 𝑘 ≤ 𝑁 , ( 𝑘 − 1 ) , 𝑘 ) = if ( 𝑖 ≤ 𝑁 , ( 𝑖 − 1 ) , 𝑖 ) )
22	13 21	ifbieq2d	⊢ ( 𝑘 = 𝑖 → if ( 𝑘 = 1 , 𝑁 , if ( 𝑘 ≤ 𝑁 , ( 𝑘 − 1 ) , 𝑘 ) ) = if ( 𝑖 = 1 , 𝑁 , if ( 𝑖 ≤ 𝑁 , ( 𝑖 − 1 ) , 𝑖 ) ) )
23	22	cbvmptv	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑘 = 1 , 𝑁 , if ( 𝑘 ≤ 𝑁 , ( 𝑘 − 1 ) , 𝑘 ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑖 = 1 , 𝑁 , if ( 𝑖 ≤ 𝑁 , ( 𝑖 − 1 ) , 𝑖 ) ) )
24		eqeq1	⊢ ( 𝑙 = 𝑗 → ( 𝑙 = 1 ↔ 𝑗 = 1 ) )
25		breq1	⊢ ( 𝑙 = 𝑗 → ( 𝑙 ≤ 𝐽 ↔ 𝑗 ≤ 𝐽 ) )
26		oveq1	⊢ ( 𝑙 = 𝑗 → ( 𝑙 − 1 ) = ( 𝑗 − 1 ) )
27		id	⊢ ( 𝑙 = 𝑗 → 𝑙 = 𝑗 )
28	25 26 27	ifbieq12d	⊢ ( 𝑙 = 𝑗 → if ( 𝑙 ≤ 𝐽 , ( 𝑙 − 1 ) , 𝑙 ) = if ( 𝑗 ≤ 𝐽 , ( 𝑗 − 1 ) , 𝑗 ) )
29	24 28	ifbieq2d	⊢ ( 𝑙 = 𝑗 → if ( 𝑙 = 1 , 𝐽 , if ( 𝑙 ≤ 𝐽 , ( 𝑙 − 1 ) , 𝑙 ) ) = if ( 𝑗 = 1 , 𝐽 , if ( 𝑗 ≤ 𝐽 , ( 𝑗 − 1 ) , 𝑗 ) ) )
30	29	cbvmptv	⊢ ( 𝑙 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑙 = 1 , 𝐽 , if ( 𝑙 ≤ 𝐽 , ( 𝑙 − 1 ) , 𝑙 ) ) ) = ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑗 = 1 , 𝐽 , if ( 𝑗 ≤ 𝐽 , ( 𝑗 − 1 ) , 𝑗 ) ) )
31		breq1	⊢ ( 𝑙 = 𝑗 → ( 𝑙 ≤ 𝑁 ↔ 𝑗 ≤ 𝑁 ) )
32	31 26 27	ifbieq12d	⊢ ( 𝑙 = 𝑗 → if ( 𝑙 ≤ 𝑁 , ( 𝑙 − 1 ) , 𝑙 ) = if ( 𝑗 ≤ 𝑁 , ( 𝑗 − 1 ) , 𝑗 ) )
33	24 32	ifbieq2d	⊢ ( 𝑙 = 𝑗 → if ( 𝑙 = 1 , 𝑁 , if ( 𝑙 ≤ 𝑁 , ( 𝑙 − 1 ) , 𝑙 ) ) = if ( 𝑗 = 1 , 𝑁 , if ( 𝑗 ≤ 𝑁 , ( 𝑗 − 1 ) , 𝑗 ) ) )
34	33	cbvmptv	⊢ ( 𝑙 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑙 = 1 , 𝑁 , if ( 𝑙 ≤ 𝑁 , ( 𝑙 − 1 ) , 𝑙 ) ) ) = ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑗 = 1 , 𝑁 , if ( 𝑗 ≤ 𝑁 , ( 𝑗 − 1 ) , 𝑗 ) ) )
35	1 2 3 4 5 6 7 8 9 10 11 12 19 23 30 34	madjusmdetlem4	⊢ ( 𝜑 → ( 𝐽 ( 𝐾 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝐽 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) ) ) )