Metamath Proof Explorer

Theorem cpmidgsum2

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as another group sum. (Contributed by AV, 10-Nov-2019)

Ref Expression
Hypotheses cpmadugsum.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
cpmadugsum.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
cpmadugsum.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cpmadugsum.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
cpmadugsum.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
cpmadugsum.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
cpmadugsum.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
cpmadugsum.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
cpmadugsum.r ⊢ × = ( .r ‘ 𝑌 )
cpmadugsum.1 ⊢ 1 = ( 1r ‘ 𝑌 )
cpmadugsum.g ⊢ + = ( +g ‘ 𝑌 )
cpmadugsum.s ⊢ − = ( -g ‘ 𝑌 )
cpmadugsum.i ⊢ 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
cpmadugsum.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑃 )
cpmadugsum.0 ⊢ 0 = ( 0g ‘ 𝑌 )
cpmadugsum.g2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
cpmidgsum2.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
cpmidgsum2.k ⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
cpmidgsum2.h ⊢ 𝐻 = ( 𝐾 · 1 )
Assertion cpmidgsum2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) 𝐻 = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmadugsum.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 cpmadugsum.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 cpmadugsum.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 cpmadugsum.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5 cpmadugsum.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
6 cpmadugsum.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
7 cpmadugsum.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
8 cpmadugsum.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
9 cpmadugsum.r ⊢ × = ( .r ‘ 𝑌 )
10 cpmadugsum.1 ⊢ 1 = ( 1r ‘ 𝑌 )
11 cpmadugsum.g ⊢ + = ( +g ‘ 𝑌 )
12 cpmadugsum.s ⊢ − = ( -g ‘ 𝑌 )
13 cpmadugsum.i ⊢ 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
14 cpmadugsum.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑃 )
15 cpmadugsum.0 ⊢ 0 = ( 0g ‘ 𝑌 )
16 cpmadugsum.g2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
17 cpmidgsum2.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
18 cpmidgsum2.k ⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
19 cpmidgsum2.h ⊢ 𝐻 = ( 𝐾 · 1 )
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 cpmadugsum ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )
21 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
22 21 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
23 22 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
24 3 4 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
25 ringgrp ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
26 23 24 25 3syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Grp )
27 3 4 pmatlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ LMod )
28 21 27 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ LMod )
29 21 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
30 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
31 6 3 30 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
32 29 31 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
33 3 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
34 4 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
35 33 34 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
36 35 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Base ‘ 𝑃 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
37 32 36 eleqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
38 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
39 38 10 ringidcl ⊢ ( 𝑌 ∈ Ring → 1 ∈ ( Base ‘ 𝑌 ) )
40 22 24 39 3syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 1 ∈ ( Base ‘ 𝑌 ) )
41 eqid ⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
42 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
43 38 41 8 42 lmodvscl ⊢ ( ( 𝑌 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 1 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
44 28 37 40 43 syl3anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
45 44 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
46 5 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
47 21 46 syl3an2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
48 38 12 grpsubcl ⊢ ( ( 𝑌 ∈ Grp ∧ ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
49 26 45 47 48 syl3anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
50 33 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ CRing )
51 eqid ⊢ ( 𝑁 maDet 𝑃 ) = ( 𝑁 maDet 𝑃 )
52 4 38 14 51 10 9 8 madurid ⊢ ( ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) ∧ 𝑃 ∈ CRing ) → ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) × ( 𝐽 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) ) = ( ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) · 1 ) )
53 49 50 52 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) × ( 𝐽 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) ) = ( ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) · 1 ) )
54 id ⊢ ( 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) → 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) )
55 fveq2 ⊢ ( 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) → ( 𝐽 ‘ 𝐼 ) = ( 𝐽 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) )
56 54 55 oveq12d ⊢ ( 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) → ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) × ( 𝐽 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) ) )
57 13 56 mp1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) × ( 𝐽 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) ) )
58 17 1 2 3 4 51 12 6 8 5 10 chpmatval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) )
59 18 58 eqtrid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐾 = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) )
60 59 oveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐾 · 1 ) = ( ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) · 1 ) )
61 19 60 eqtrid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐻 = ( ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) · 1 ) )
62 53 57 61 3eqtr4rd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐻 = ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) )
63 62 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) → 𝐻 = ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) )
64 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) → ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )
65 63 64 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) → 𝐻 = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )
66 65 ex ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) → 𝐻 = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) )
67 66 reximdv ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) → ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) 𝐻 = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) )
68 67 reximdv ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) 𝐻 = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) )
69 20 68 mpd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) 𝐻 = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )