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

Theorem cpmidgsum2 21494
 Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as another group sum. (Contributed by AV, 10-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 𝐾 = (𝐶𝑀)
cpmidgsum2.h 𝐻 = (𝐾 · 1 )
Assertion
Ref Expression
cpmidgsum2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (0...𝑠))𝐻 = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))
Distinct variable groups:   𝐵,𝑖   𝑖,𝑀   𝑖,𝑁   𝑅,𝑖   𝑖,𝑋   𝑖,𝑌   × ,𝑖   · ,𝑖   1 ,𝑖   𝑖,𝑏,𝑠,𝑇   ,𝑖   ,𝑖   𝐴,𝑏,𝑛,𝑠   𝐵,𝑏,𝑛,𝑠   𝐼,𝑏,𝑖,𝑛,𝑠   𝐽,𝑏,𝑖,𝑛,𝑠   𝑀,𝑏,𝑛,𝑠   𝑁,𝑏,𝑛,𝑠   𝑃,𝑖,𝑛   𝑅,𝑏,𝑛,𝑠   𝑇,𝑏,𝑛,𝑠   𝑋,𝑏,𝑛,𝑠   𝑌,𝑏,𝑛,𝑠   ,𝑛,𝑠,𝑏   · ,𝑏,𝑛,𝑠   𝑖,𝐺   × ,𝑛   0 ,𝑛   ,𝑛
Allowed substitution hints:   𝐴(𝑖)   𝐶(𝑖,𝑛,𝑠,𝑏)   𝑃(𝑠,𝑏)   + (𝑖,𝑛,𝑠,𝑏)   × (𝑠,𝑏)   1 (𝑛,𝑠,𝑏)   𝐺(𝑛,𝑠,𝑏)   𝐻(𝑖,𝑛,𝑠,𝑏)   𝐾(𝑖,𝑛,𝑠,𝑏)   (𝑠,𝑏)   0 (𝑖,𝑠,𝑏)

Proof of Theorem cpmidgsum2
StepHypRef Expression
1 cpmadugsum.a . . 3 𝐴 = (𝑁 Mat 𝑅)
2 cpmadugsum.b . . 3 𝐵 = (Base‘𝐴)
3 cpmadugsum.p . . 3 𝑃 = (Poly1𝑅)
4 cpmadugsum.y . . 3 𝑌 = (𝑁 Mat 𝑃)
5 cpmadugsum.t . . 3 𝑇 = (𝑁 matToPolyMat 𝑅)
6 cpmadugsum.x . . 3 𝑋 = (var1𝑅)
7 cpmadugsum.e . . 3 = (.g‘(mulGrp‘𝑃))
8 cpmadugsum.m . . 3 · = ( ·𝑠𝑌)
9 cpmadugsum.r . . 3 × = (.r𝑌)
10 cpmadugsum.1 . . 3 1 = (1r𝑌)
11 cpmadugsum.g . . 3 + = (+g𝑌)
12 cpmadugsum.s . . 3 = (-g𝑌)
13 cpmadugsum.i . . 3 𝐼 = ((𝑋 · 1 ) (𝑇𝑀))
15 cpmadugsum.0 . . 3 0 = (0g𝑌)
16 cpmadugsum.g2 . . 3 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))))
171, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16cpmadugsum 21493 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (0...𝑠))(𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))
18 crngring 19306 . . . . . . . . . . . . 13 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
1918anim2i 619 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
20193adant3 1129 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
213, 4pmatring 21307 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
22 ringgrp 19299 . . . . . . . . . . 11 (𝑌 ∈ Ring → 𝑌 ∈ Grp)
2320, 21, 223syl 18 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Grp)
243, 4pmatlmod 21308 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ LMod)
2518, 24sylan2 595 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ LMod)
2618adantl 485 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring)
27 eqid 2798 . . . . . . . . . . . . . . 15 (Base‘𝑃) = (Base‘𝑃)
286, 3, 27vr1cl 20856 . . . . . . . . . . . . . 14 (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
2926, 28syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑋 ∈ (Base‘𝑃))
303ply1crng 20837 . . . . . . . . . . . . . . 15 (𝑅 ∈ CRing → 𝑃 ∈ CRing)
314matsca2 21035 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝑌))
3230, 31sylan2 595 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 = (Scalar‘𝑌))
3332fveq2d 6650 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (Base‘𝑃) = (Base‘(Scalar‘𝑌)))
3429, 33eleqtrd 2892 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑋 ∈ (Base‘(Scalar‘𝑌)))
35 eqid 2798 . . . . . . . . . . . . . 14 (Base‘𝑌) = (Base‘𝑌)
3635, 10ringidcl 19318 . . . . . . . . . . . . 13 (𝑌 ∈ Ring → 1 ∈ (Base‘𝑌))
3719, 21, 363syl 18 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 1 ∈ (Base‘𝑌))
38 eqid 2798 . . . . . . . . . . . . 13 (Scalar‘𝑌) = (Scalar‘𝑌)
39 eqid 2798 . . . . . . . . . . . . 13 (Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌))
4035, 38, 8, 39lmodvscl 19648 . . . . . . . . . . . 12 ((𝑌 ∈ LMod ∧ 𝑋 ∈ (Base‘(Scalar‘𝑌)) ∧ 1 ∈ (Base‘𝑌)) → (𝑋 · 1 ) ∈ (Base‘𝑌))
4125, 34, 37, 40syl3anc 1368 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑋 · 1 ) ∈ (Base‘𝑌))
42413adant3 1129 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑋 · 1 ) ∈ (Base‘𝑌))
435, 1, 2, 3, 4mat2pmatbas 21341 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
4418, 43syl3an2 1161 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
4535, 12grpsubcl 18175 . . . . . . . . . 10 ((𝑌 ∈ Grp ∧ (𝑋 · 1 ) ∈ (Base‘𝑌) ∧ (𝑇𝑀) ∈ (Base‘𝑌)) → ((𝑋 · 1 ) (𝑇𝑀)) ∈ (Base‘𝑌))
4623, 42, 44, 45syl3anc 1368 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ((𝑋 · 1 ) (𝑇𝑀)) ∈ (Base‘𝑌))
47303ad2ant2 1131 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑃 ∈ CRing)
48 eqid 2798 . . . . . . . . . 10 (𝑁 maDet 𝑃) = (𝑁 maDet 𝑃)
494, 35, 14, 48, 10, 9, 8madurid 21259 . . . . . . . . 9 ((((𝑋 · 1 ) (𝑇𝑀)) ∈ (Base‘𝑌) ∧ 𝑃 ∈ CRing) → (((𝑋 · 1 ) (𝑇𝑀)) × (𝐽‘((𝑋 · 1 ) (𝑇𝑀)))) = (((𝑁 maDet 𝑃)‘((𝑋 · 1 ) (𝑇𝑀))) · 1 ))
5046, 47, 49syl2anc 587 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (((𝑋 · 1 ) (𝑇𝑀)) × (𝐽‘((𝑋 · 1 ) (𝑇𝑀)))) = (((𝑁 maDet 𝑃)‘((𝑋 · 1 ) (𝑇𝑀))) · 1 ))
51 id 22 . . . . . . . . . 10 (𝐼 = ((𝑋 · 1 ) (𝑇𝑀)) → 𝐼 = ((𝑋 · 1 ) (𝑇𝑀)))
52 fveq2 6646 . . . . . . . . . 10 (𝐼 = ((𝑋 · 1 ) (𝑇𝑀)) → (𝐽𝐼) = (𝐽‘((𝑋 · 1 ) (𝑇𝑀))))
5351, 52oveq12d 7154 . . . . . . . . 9 (𝐼 = ((𝑋 · 1 ) (𝑇𝑀)) → (𝐼 × (𝐽𝐼)) = (((𝑋 · 1 ) (𝑇𝑀)) × (𝐽‘((𝑋 · 1 ) (𝑇𝑀)))))
5413, 53mp1i 13 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝐼 × (𝐽𝐼)) = (((𝑋 · 1 ) (𝑇𝑀)) × (𝐽‘((𝑋 · 1 ) (𝑇𝑀)))))
55 cpmidgsum2.h . . . . . . . . 9 𝐻 = (𝐾 · 1 )
56 cpmidgsum2.k . . . . . . . . . . 11 𝐾 = (𝐶𝑀)
57 cpmidgsum2.c . . . . . . . . . . . 12 𝐶 = (𝑁 CharPlyMat 𝑅)
5857, 1, 2, 3, 4, 48, 12, 6, 8, 5, 10chpmatval 21446 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝐶𝑀) = ((𝑁 maDet 𝑃)‘((𝑋 · 1 ) (𝑇𝑀))))
5956, 58syl5eq 2845 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝐾 = ((𝑁 maDet 𝑃)‘((𝑋 · 1 ) (𝑇𝑀))))
6059oveq1d 7151 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝐾 · 1 ) = (((𝑁 maDet 𝑃)‘((𝑋 · 1 ) (𝑇𝑀))) · 1 ))
6155, 60syl5eq 2845 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝐻 = (((𝑁 maDet 𝑃)‘((𝑋 · 1 ) (𝑇𝑀))) · 1 ))
6250, 54, 613eqtr4rd 2844 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝐻 = (𝐼 × (𝐽𝐼)))
6362adantr 484 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))) → 𝐻 = (𝐼 × (𝐽𝐼)))
64 simpr 488 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))) → (𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))
6563, 64eqtrd 2833 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))) → 𝐻 = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))
6665ex 416 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ((𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))) → 𝐻 = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))))
6766reximdv 3232 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (∃𝑏 ∈ (𝐵m (0...𝑠))(𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))) → ∃𝑏 ∈ (𝐵m (0...𝑠))𝐻 = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))))
6867reximdv 3232 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (0...𝑠))(𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (0...𝑠))𝐻 = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))))
6917, 68mpd 15 1 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (0...𝑠))𝐻 = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))