Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cpmidg2sum Structured version   Visualization version   GIF version

Theorem cpmidg2sum 20504
 Description: Equality of two sums representing the identity matrix multiplied with the characteristic polynomial of a matrix. (Contributed by AV, 11-Nov-2019.)
Hypotheses
Ref Expression
cpmadugsum.a 𝐴 = (𝑁 Mat 𝑅)
cpmadugsum.y 𝑌 = (𝑁 Mat 𝑃)
cpmadugsum.t 𝑇 = (𝑁 matToPolyMat 𝑅)
cpmadugsum.i 𝐼 = ((𝑋 · 1 ) (𝑇𝑀))
cpmadugsum.g2 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))))
cpmidgsum2.c 𝐶 = (𝑁 CharPlyMat 𝑅)
cpmidgsum2.k 𝐾 = (𝐶𝑀)
cpmidg2sum.u 𝑈 = (algSc‘𝑃)
Assertion
Ref Expression
cpmidg2sum ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵𝑚 (0...𝑠))(𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · ((𝑈‘((coe1𝐾)‘𝑖)) · 1 )))) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))
Distinct variable groups:   𝐵,𝑖   𝑖,𝑀   𝑖,𝑁   𝑅,𝑖   𝑖,𝑋   𝑖,𝑌   × ,𝑖   · ,𝑖   1 ,𝑖   𝑖,𝑏,𝑠,𝑇   ,𝑖   ,𝑖   𝐴,𝑏,𝑛,𝑠   𝐵,𝑏,𝑛,𝑠   𝐼,𝑏,𝑖,𝑛,𝑠   𝐽,𝑏,𝑖,𝑛,𝑠   𝑀,𝑏,𝑛,𝑠   𝑁,𝑏,𝑛,𝑠   𝑃,𝑖,𝑛   𝑅,𝑏,𝑛,𝑠   𝑇,𝑏,𝑛,𝑠   𝑋,𝑏,𝑛,𝑠   𝑌,𝑏,𝑛,𝑠   ,𝑛,𝑠,𝑏   · ,𝑏,𝑛,𝑠   𝑖,𝐺   × ,𝑛   0 ,𝑛   ,𝑛   𝐴,𝑖   𝑖,𝐾
Allowed substitution hints:   𝐶(𝑖,𝑛,𝑠,𝑏)   𝑃(𝑠,𝑏)   + (𝑖,𝑛,𝑠,𝑏)   × (𝑠,𝑏)   𝑈(𝑖,𝑛,𝑠,𝑏)   1 (𝑛,𝑠,𝑏)   𝐺(𝑛,𝑠,𝑏)   𝐾(𝑛,𝑠,𝑏)   (𝑠,𝑏)   0 (𝑖,𝑠,𝑏)

Proof of Theorem cpmidg2sum
StepHypRef Expression
1 cpmadugsum.a . . . . . 6 𝐴 = (𝑁 Mat 𝑅)
2 cpmadugsum.b . . . . . 6 𝐵 = (Base‘𝐴)
3 cpmadugsum.p . . . . . 6 𝑃 = (Poly1𝑅)
4 cpmadugsum.y . . . . . 6 𝑌 = (𝑁 Mat 𝑃)
5 cpmadugsum.x . . . . . 6 𝑋 = (var1𝑅)
6 cpmadugsum.e . . . . . 6 = (.g‘(mulGrp‘𝑃))
7 cpmadugsum.m . . . . . 6 · = ( ·𝑠𝑌)
8 cpmadugsum.1 . . . . . 6 1 = (1r𝑌)
9 cpmidg2sum.u . . . . . 6 𝑈 = (algSc‘𝑃)
10 cpmidgsum2.c . . . . . 6 𝐶 = (𝑁 CharPlyMat 𝑅)
11 cpmidgsum2.k . . . . . 6 𝐾 = (𝐶𝑀)
12 eqid 2610 . . . . . 6 (𝐾 · 1 ) = (𝐾 · 1 )
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12cpmidgsum 20492 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝐾 · 1 ) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · ((𝑈‘((coe1𝐾)‘𝑖)) · 1 )))))
1413eqcomd 2616 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · ((𝑈‘((coe1𝐾)‘𝑖)) · 1 )))) = (𝐾 · 1 ))
1514ad3antrrr 762 . . 3 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ (𝐾 · 1 ) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · ((𝑈‘((coe1𝐾)‘𝑖)) · 1 )))) = (𝐾 · 1 ))
16 simpr 476 . . 3 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ (𝐾 · 1 ) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))) → (𝐾 · 1 ) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))
1715, 16eqtrd 2644 . 2 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ (𝐾 · 1 ) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · ((𝑈‘((coe1𝐾)‘𝑖)) · 1 )))) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))
18 cpmadugsum.t . . 3 𝑇 = (𝑁 matToPolyMat 𝑅)
19 cpmadugsum.r . . 3 × = (.r𝑌)
20 cpmadugsum.g . . 3 + = (+g𝑌)
21 cpmadugsum.s . . 3 = (-g𝑌)
22 cpmadugsum.i . . 3 𝐼 = ((𝑋 · 1 ) (𝑇𝑀))