Metamath Proof Explorer

Theorem mdetlap

Description: Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-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 mdetlap ( 𝜑 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑍 ‘ ( - 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 2 1 3 4 5 mdetlap1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ ( 1 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) ) )
14 9 12 10 13 syl3anc ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) ) )
15 8 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℕ )
16 9 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑅 ∈ CRing )
17 10 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐼 ∈ ( 1 ... 𝑁 ) )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
19 12 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑀 ∈ 𝐵 )
20 1 2 3 4 5 6 7 15 16 17 18 19 madjusmdet ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) )
21 20 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝐼 𝑀 𝑗 ) · ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
22 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
23 2 22 1 17 18 19 matecld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
24 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
25 6 zrhrhm ⊢ ( 𝑅 ∈ Ring → 𝑍 ∈ ( ℤring RingHom 𝑅 ) )
26 zringbas ⊢ ℤ = ( Base ‘ ℤring )
27 26 22 rhmf ⊢ ( 𝑍 ∈ ( ℤring RingHom 𝑅 ) → 𝑍 : ℤ ⟶ ( Base ‘ 𝑅 ) )
28 9 24 25 27 4syl ⊢ ( 𝜑 → 𝑍 : ℤ ⟶ ( Base ‘ 𝑅 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑍 : ℤ ⟶ ( Base ‘ 𝑅 ) )
30 1zzd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℤ )
31 30 znegcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → - 1 ∈ ℤ )
32 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
33 32 17 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐼 ∈ ℕ )
34 32 18 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ℕ )
35 33 34 nnaddcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐼 + 𝑗 ) ∈ ℕ )
36 35 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐼 + 𝑗 ) ∈ ℕ0 )
37 zexpcl ⊢ ( ( - 1 ∈ ℤ ∧ ( 𝐼 + 𝑗 ) ∈ ℕ0 ) → ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ∈ ℤ )
38 31 36 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ∈ ℤ )
39 29 38 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) )
40 22 5 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) )
41 16 23 39 40 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) )
42 41 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) )
43 16 24 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑅 ∈ Ring )
44 eqid ⊢ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) )
45 eqid ⊢ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) = ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 )
46 2 1 44 45 15 17 18 19 smatcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
47 eqid ⊢ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) = ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 )
48 7 47 44 22 mdetcl ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ) → ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
49 16 46 48 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
50 22 5 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( 𝐼 𝑀 𝑗 ) · ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
51 43 23 39 49 50 syl13anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( 𝐼 𝑀 𝑗 ) · ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
52 22 5 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
53 43 39 23 49 52 syl13anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
54 42 51 53 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
55 21 54 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
56 55 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) = ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) ) )
57 56 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) ) ) )
58 14 57 eqtrd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) ) ) )