Metamath Proof Explorer

Theorem chpidmat

Description: The characteristic polynomial of the identity matrix. (Contributed by AV, 19-Aug-2019)

Ref Expression
Hypotheses chp0mat.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
chp0mat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
chp0mat.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
chp0mat.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
chp0mat.g ⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
chp0mat.m ⊢ ↑ = ( .g ‘ 𝐺 )
chpidmat.i ⊢ 𝐼 = ( 1r ‘ 𝐴 )
chpidmat.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
chpidmat.1 ⊢ 1 = ( 1r ‘ 𝑅 )
chpidmat.m ⊢ − = ( -g ‘ 𝑃 )
Assertion chpidmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝐶 ‘ 𝐼 ) = ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 − ( 𝑆 ‘ 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 chp0mat.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2 chp0mat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 chp0mat.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4 chp0mat.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
5 chp0mat.g ⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
6 chp0mat.m ⊢ ↑ = ( .g ‘ 𝐺 )
7 chpidmat.i ⊢ 𝐼 = ( 1r ‘ 𝐴 )
8 chpidmat.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
9 chpidmat.1 ⊢ 1 = ( 1r ‘ 𝑅 )
10 chpidmat.m ⊢ − = ( -g ‘ 𝑃 )
11 simpl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑁 ∈ Fin )
12 simpr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing )
13 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
14 3 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
15 13 14 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
16 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
17 16 7 ringidcl ⊢ ( 𝐴 ∈ Ring → 𝐼 ∈ ( Base ‘ 𝐴 ) )
18 15 17 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐼 ∈ ( Base ‘ 𝐴 ) )
19 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
20 11 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → 𝑁 ∈ Fin )
21 13 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
22 21 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → 𝑅 ∈ Ring )
23 simplrl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → 𝑖 ∈ 𝑁 )
24 simplrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → 𝑗 ∈ 𝑁 )
25 3 9 19 20 22 23 24 7 mat1ov ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝑖 𝐼 𝑗 ) = if ( 𝑖 = 𝑗 , 1 , ( 0g ‘ 𝑅 ) ) )
26 ifnefalse ⊢ ( 𝑖 ≠ 𝑗 → if ( 𝑖 = 𝑗 , 1 , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
27 26 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → if ( 𝑖 = 𝑗 , 1 , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
28 25 27 eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝑖 𝐼 𝑗 ) = ( 0g ‘ 𝑅 ) )
29 28 ex ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ≠ 𝑗 → ( 𝑖 𝐼 𝑗 ) = ( 0g ‘ 𝑅 ) ) )
30 29 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝐼 𝑗 ) = ( 0g ‘ 𝑅 ) ) )
31 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
32 1 2 3 8 16 4 19 5 31 chpdmat ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ ( Base ‘ 𝐴 ) ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝐼 𝑗 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝐶 ‘ 𝐼 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ ( 𝑘 𝐼 𝑘 ) ) ) ) ) )
33 11 12 18 30 32 syl31anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝐶 ‘ 𝐼 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ ( 𝑘 𝐼 𝑘 ) ) ) ) ) )
34 11 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → 𝑁 ∈ Fin )
35 21 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → 𝑅 ∈ Ring )
36 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
37 3 9 19 34 35 36 36 7 mat1ov ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 𝐼 𝑘 ) = if ( 𝑘 = 𝑘 , 1 , ( 0g ‘ 𝑅 ) ) )
38 eqid ⊢ 𝑘 = 𝑘
39 38 iftruei ⊢ if ( 𝑘 = 𝑘 , 1 , ( 0g ‘ 𝑅 ) ) = 1
40 37 39 eqtrdi ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 𝐼 𝑘 ) = 1 )
41 40 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑆 ‘ ( 𝑘 𝐼 𝑘 ) ) = ( 𝑆 ‘ 1 ) )
42 41 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ ( 𝑘 𝐼 𝑘 ) ) ) = ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) )
43 42 mpteq2dva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ ( 𝑘 𝐼 𝑘 ) ) ) ) = ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) ) )
44 43 oveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ ( 𝑘 𝐼 𝑘 ) ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) ) ) )
45 2 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
46 5 crngmgp ⊢ ( 𝑃 ∈ CRing → 𝐺 ∈ CMnd )
47 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
48 45 46 47 3syl ⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ Mnd )
49 48 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐺 ∈ Mnd )
50 2 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
51 ringgrp ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
52 50 51 syl ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Grp )
53 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
54 4 2 53 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
55 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
56 2 8 9 55 ply1scl1 ⊢ ( 𝑅 ∈ Ring → ( 𝑆 ‘ 1 ) = ( 1r ‘ 𝑃 ) )
57 53 55 ringidcl ⊢ ( 𝑃 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
58 50 57 syl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
59 56 58 eqeltrd ⊢ ( 𝑅 ∈ Ring → ( 𝑆 ‘ 1 ) ∈ ( Base ‘ 𝑃 ) )
60 52 54 59 3jca ⊢ ( 𝑅 ∈ Ring → ( 𝑃 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑆 ‘ 1 ) ∈ ( Base ‘ 𝑃 ) ) )
61 13 60 syl ⊢ ( 𝑅 ∈ CRing → ( 𝑃 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑆 ‘ 1 ) ∈ ( Base ‘ 𝑃 ) ) )
62 61 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑃 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑆 ‘ 1 ) ∈ ( Base ‘ 𝑃 ) ) )
63 53 31 grpsubcl ⊢ ( ( 𝑃 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑆 ‘ 1 ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) ∈ ( Base ‘ 𝑃 ) )
64 62 63 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) ∈ ( Base ‘ 𝑃 ) )
65 5 53 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝐺 )
66 64 65 eleqtrdi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) ∈ ( Base ‘ 𝐺 ) )
67 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
68 67 6 gsumconst ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ Fin ∧ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) ) ) = ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) ) )
69 10 eqcomi ⊢ ( -g ‘ 𝑃 ) = −
70 69 oveqi ⊢ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) = ( 𝑋 − ( 𝑆 ‘ 1 ) )
71 70 oveq2i ⊢ ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) ) = ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 − ( 𝑆 ‘ 1 ) ) )
72 68 71 eqtrdi ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ Fin ∧ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) ) ) = ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 − ( 𝑆 ‘ 1 ) ) ) )
73 49 11 66 72 syl3anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ 1 ) ) ) ) = ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 − ( 𝑆 ‘ 1 ) ) ) )
74 44 73 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( 𝑆 ‘ ( 𝑘 𝐼 𝑘 ) ) ) ) ) = ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 − ( 𝑆 ‘ 1 ) ) ) )
75 33 74 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝐶 ‘ 𝐼 ) = ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 − ( 𝑆 ‘ 1 ) ) ) )