Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mdetlap Structured version   Visualization version   GIF version

Theorem mdetlap 29226
 Description: Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-Aug-2020.)
Hypotheses
Ref Expression
madjusmdet.a 𝐴 = ((1...𝑁) Mat 𝑅)
Assertion
Ref Expression
mdetlap (𝜑 → (𝐷𝑀) = (𝑅 Σg (𝑗 ∈ (1...𝑁) ↦ ((𝑍‘(-1↑(𝐼 + 𝑗))) · ((𝐼𝑀𝑗) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗)))))))
Distinct variable groups:   𝐵,𝑗   𝑗,𝐼   𝑗,𝐽   𝑗,𝑀   𝑗,𝑁   𝑅,𝑗   𝜑,𝑗   · ,𝑗   𝐴,𝑗   𝑗,𝐾
Allowed substitution hints:   𝐷(𝑗)   𝐸(𝑗)   𝑍(𝑗)

Proof of Theorem mdetlap
StepHypRef Expression
1 madjusmdet.r . . 3 (𝜑𝑅 ∈ CRing)
2 madjusmdet.m . . 3 (𝜑𝑀𝐵)
3 madjusmdet.i . . 3 (𝜑𝐼 ∈ (1...𝑁))
4 madjusmdet.a . . . 4 𝐴 = ((1...𝑁) Mat 𝑅)
5 madjusmdet.b . . . 4 𝐵 = (Base‘𝐴)
8 madjusmdet.t . . . 4 · = (.r𝑅)
94, 5, 6, 7, 8mdetlap1 29220 . . 3 ((𝑅 ∈ CRing ∧ 𝑀𝐵𝐼 ∈ (1...𝑁)) → (𝐷𝑀) = (𝑅 Σg (𝑗 ∈ (1...𝑁) ↦ ((𝐼𝑀𝑗) · (𝑗(𝐾𝑀)𝐼)))))
101, 2, 3, 9syl3anc 1318 . 2 (𝜑 → (𝐷𝑀) = (𝑅 Σg (𝑗 ∈ (1...𝑁) ↦ ((𝐼𝑀𝑗) · (𝑗(𝐾𝑀)𝐼)))))
11 madjusmdet.z . . . . . . 7 𝑍 = (ℤRHom‘𝑅)
12 madjusmdet.e . . . . . . 7 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅)
13 madjusmdet.n . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
1413adantr 480 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ∈ ℕ)
151adantr 480 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑅 ∈ CRing)
163adantr 480 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → 𝐼 ∈ (1...𝑁))
17 simpr 476 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
182adantr 480 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑀𝐵)
195, 4, 6, 7, 8, 11, 12, 14, 15, 16, 17, 18madjusmdet 29225 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗(𝐾𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝑗))) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗))))
2019oveq2d 6565 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → ((𝐼𝑀𝑗) · (𝑗(𝐾𝑀)𝐼)) = ((𝐼𝑀𝑗) · ((𝑍‘(-1↑(𝐼 + 𝑗))) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗)))))
21 eqid 2610 . . . . . . . . 9 (Base‘𝑅) = (Base‘𝑅)
224, 21, 5, 16, 17, 18matecld 20051 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐼𝑀𝑗) ∈ (Base‘𝑅))
23 crngring 18381 . . . . . . . . . . . 12 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
241, 23syl 17 . . . . . . . . . . 11 (𝜑𝑅 ∈ Ring)
2511zrhrhm 19679 . . . . . . . . . . 11 (𝑅 ∈ Ring → 𝑍 ∈ (ℤring RingHom 𝑅))
26 zringbas 19643 . . . . . . . . . . . 12 ℤ = (Base‘ℤring)
2726, 21rhmf 18549 . . . . . . . . . . 11 (𝑍 ∈ (ℤring RingHom 𝑅) → 𝑍:ℤ⟶(Base‘𝑅))
2824, 25, 273syl 18 . . . . . . . . . 10 (𝜑𝑍:ℤ⟶(Base‘𝑅))
2928adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑍:ℤ⟶(Base‘𝑅))
30 1zzd 11285 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → 1 ∈ ℤ)
3130znegcld 11360 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → -1 ∈ ℤ)
32 fz1ssnn 12243 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℕ
3332, 16sseldi 3566 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑁)) → 𝐼 ∈ ℕ)
3432, 17sseldi 3566 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
3533, 34nnaddcld 10944 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐼 + 𝑗) ∈ ℕ)
3635nnnn0d 11228 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐼 + 𝑗) ∈ ℕ0)
37 zexpcl 12737 . . . . . . . . . 10 ((-1 ∈ ℤ ∧ (𝐼 + 𝑗) ∈ ℕ0) → (-1↑(𝐼 + 𝑗)) ∈ ℤ)
3831, 36, 37syl2anc 691 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → (-1↑(𝐼 + 𝑗)) ∈ ℤ)
3929, 38ffvelrnd 6268 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑍‘(-1↑(𝐼 + 𝑗))) ∈ (Base‘𝑅))
4021, 8crngcom 18385 . . . . . . . 8 ((𝑅 ∈ CRing ∧ (𝐼𝑀𝑗) ∈ (Base‘𝑅) ∧ (𝑍‘(-1↑(𝐼 + 𝑗))) ∈ (Base‘𝑅)) → ((𝐼𝑀𝑗) · (𝑍‘(-1↑(𝐼 + 𝑗)))) = ((𝑍‘(-1↑(𝐼 + 𝑗))) · (𝐼𝑀𝑗)))
4115, 22, 39, 40syl3anc 1318 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → ((𝐼𝑀𝑗) · (𝑍‘(-1↑(𝐼 + 𝑗)))) = ((𝑍‘(-1↑(𝐼 + 𝑗))) · (𝐼𝑀𝑗)))
4241oveq1d 6564 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → (((𝐼𝑀𝑗) · (𝑍‘(-1↑(𝐼 + 𝑗)))) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗))) = (((𝑍‘(-1↑(𝐼 + 𝑗))) · (𝐼𝑀𝑗)) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗))))
4315, 23syl 17 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑅 ∈ Ring)
44 eqid 2610 . . . . . . . . 9 (Base‘((1...(𝑁 − 1)) Mat 𝑅)) = (Base‘((1...(𝑁 − 1)) Mat 𝑅))
45 eqid 2610 . . . . . . . . 9 (𝐼(subMat1‘𝑀)𝑗) = (𝐼(subMat1‘𝑀)𝑗)
464, 5, 44, 45, 14, 16, 17, 18smatcl 29196 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐼(subMat1‘𝑀)𝑗) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)))
47 eqid 2610 . . . . . . . . 9 ((1...(𝑁 − 1)) Mat 𝑅) = ((1...(𝑁 − 1)) Mat 𝑅)
4812, 47, 44, 21mdetcl 20221 . . . . . . . 8 ((𝑅 ∈ CRing ∧ (𝐼(subMat1‘𝑀)𝑗) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) → (𝐸‘(𝐼(subMat1‘𝑀)𝑗)) ∈ (Base‘𝑅))
4915, 46, 48syl2anc 691 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐸‘(𝐼(subMat1‘𝑀)𝑗)) ∈ (Base‘𝑅))
5021, 8ringass 18387 . . . . . . 7 ((𝑅 ∈ Ring ∧ ((𝐼𝑀𝑗) ∈ (Base‘𝑅) ∧ (𝑍‘(-1↑(𝐼 + 𝑗))) ∈ (Base‘𝑅) ∧ (𝐸‘(𝐼(subMat1‘𝑀)𝑗)) ∈ (Base‘𝑅))) → (((𝐼𝑀𝑗) · (𝑍‘(-1↑(𝐼 + 𝑗)))) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗))) = ((𝐼𝑀𝑗) · ((𝑍‘(-1↑(𝐼 + 𝑗))) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗)))))
5143, 22, 39, 49, 50syl13anc 1320 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → (((𝐼𝑀𝑗) · (𝑍‘(-1↑(𝐼 + 𝑗)))) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗))) = ((𝐼𝑀𝑗) · ((𝑍‘(-1↑(𝐼 + 𝑗))) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗)))))
5221, 8ringass 18387 . . . . . . 7 ((𝑅 ∈ Ring ∧ ((𝑍‘(-1↑(𝐼 + 𝑗))) ∈ (Base‘𝑅) ∧ (𝐼𝑀𝑗) ∈ (Base‘𝑅) ∧ (𝐸‘(𝐼(subMat1‘𝑀)𝑗)) ∈ (Base‘𝑅))) → (((𝑍‘(-1↑(𝐼 + 𝑗))) · (𝐼𝑀𝑗)) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗))) = ((𝑍‘(-1↑(𝐼 + 𝑗))) · ((𝐼𝑀𝑗) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗)))))
5343, 39, 22, 49, 52syl13anc 1320 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → (((𝑍‘(-1↑(𝐼 + 𝑗))) · (𝐼𝑀𝑗)) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗))) = ((𝑍‘(-1↑(𝐼 + 𝑗))) · ((𝐼𝑀𝑗) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗)))))
5442, 51, 533eqtr3d 2652 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → ((𝐼𝑀𝑗) · ((𝑍‘(-1↑(𝐼 + 𝑗))) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗)))) = ((𝑍‘(-1↑(𝐼 + 𝑗))) · ((𝐼𝑀𝑗) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗)))))
5520, 54eqtrd 2644 . . . 4 ((𝜑𝑗 ∈ (1...𝑁)) → ((𝐼𝑀𝑗) · (𝑗(𝐾𝑀)𝐼)) = ((𝑍‘(-1↑(𝐼 + 𝑗))) · ((𝐼𝑀𝑗) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗)))))
5655mpteq2dva 4672 . . 3 (𝜑 → (𝑗 ∈ (1...𝑁) ↦ ((𝐼𝑀𝑗) · (𝑗(𝐾𝑀)𝐼))) = (𝑗 ∈ (1...𝑁) ↦ ((𝑍‘(-1↑(𝐼 + 𝑗))) · ((𝐼𝑀𝑗) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗))))))
5756oveq2d 6565 . 2 (𝜑 → (𝑅 Σg (𝑗 ∈ (1...𝑁) ↦ ((𝐼𝑀𝑗) · (𝑗(𝐾𝑀)𝐼)))) = (𝑅 Σg (𝑗 ∈ (1...𝑁) ↦ ((𝑍‘(-1↑(𝐼 + 𝑗))) · ((𝐼𝑀𝑗) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗)))))))
5810, 57eqtrd 2644 1 (𝜑 → (𝐷𝑀) = (𝑅 Σg (𝑗 ∈ (1...𝑁) ↦ ((𝑍‘(-1↑(𝐼 + 𝑗))) · ((𝐼𝑀𝑗) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗)))))))