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 9 24 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
26 6 zrhrhm ⊢ ( 𝑅 ∈ Ring → 𝑍 ∈ ( ℤring RingHom 𝑅 ) )
27 zringbas ⊢ ℤ = ( Base ‘ ℤring )
28 27 22 rhmf ⊢ ( 𝑍 ∈ ( ℤring RingHom 𝑅 ) → 𝑍 : ℤ ⟶ ( Base ‘ 𝑅 ) )
29 25 26 28 3syl ⊢ ( 𝜑 → 𝑍 : ℤ ⟶ ( Base ‘ 𝑅 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑍 : ℤ ⟶ ( Base ‘ 𝑅 ) )
31 1zzd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℤ )
32 31 znegcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → - 1 ∈ ℤ )
33 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
34 33 17 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐼 ∈ ℕ )
35 33 18 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ℕ )
36 34 35 nnaddcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐼 + 𝑗 ) ∈ ℕ )
37 36 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐼 + 𝑗 ) ∈ ℕ0 )
38 zexpcl ⊢ ( ( - 1 ∈ ℤ ∧ ( 𝐼 + 𝑗 ) ∈ ℕ0 ) → ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ∈ ℤ )
39 32 37 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ∈ ℤ )
40 30 39 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) )
41 22 5 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) )
42 16 23 40 41 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) )
43 42 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) )
44 16 24 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑅 ∈ Ring )
45 eqid ⊢ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) )
46 eqid ⊢ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) = ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 )
47 2 1 45 46 15 17 18 19 smatcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
48 eqid ⊢ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) = ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 )
49 7 48 45 22 mdetcl ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ) → ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
50 16 47 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
51 22 5 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( 𝐼 𝑀 𝑗 ) · ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
52 44 23 40 50 51 syl13anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( 𝐼 𝑀 𝑗 ) · ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
53 22 5 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
54 44 40 23 50 53 syl13anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
55 43 52 54 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
56 21 55 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
57 56 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) = ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) ) )
58 57 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) ) ) )
59 14 58 eqtrd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) ) ) )