Metamath Proof Explorer


Theorem chpmatval2

Description: The characteristic polynomial of a (square) matrix (expressed with the Leibnitz formula for the determinant). (Contributed by AV, 2-Aug-2019)

Ref Expression
Hypotheses chpmatply1.c 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
chpmatply1.a 𝐴 = ( 𝑁 Mat 𝑅 )
chpmatply1.b 𝐵 = ( Base ‘ 𝐴 )
chpmatply1.p 𝑃 = ( Poly1𝑅 )
chpmatval2.y 𝑌 = ( 𝑁 Mat 𝑃 )
chpmatval2.m1 = ( -g𝑌 )
chpmatval2.x 𝑋 = ( var1𝑅 )
chpmatval2.t1 · = ( ·𝑠𝑌 )
chpmatval2.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
chpmatval2.i 1 = ( 1r𝑌 )
chpmatval2.g 𝐺 = ( SymGrp ‘ 𝑁 )
chpmatval2.h 𝐻 = ( Base ‘ 𝐺 )
chpmatval2.z 𝑍 = ( ℤRHom ‘ 𝑃 )
chpmatval2.s 𝑆 = ( pmSgn ‘ 𝑁 )
chpmatval2.u 𝑈 = ( mulGrp ‘ 𝑃 )
chpmatval2.rm × = ( .r𝑃 )
Assertion chpmatval2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝐶𝑀 ) = ( 𝑃 Σg ( 𝑝𝐻 ↦ ( ( ( 𝑍𝑆 ) ‘ 𝑝 ) × ( 𝑈 Σg ( 𝑥𝑁 ↦ ( ( 𝑝𝑥 ) ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) 𝑥 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 chpmatply1.c 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2 chpmatply1.a 𝐴 = ( 𝑁 Mat 𝑅 )
3 chpmatply1.b 𝐵 = ( Base ‘ 𝐴 )
4 chpmatply1.p 𝑃 = ( Poly1𝑅 )
5 chpmatval2.y 𝑌 = ( 𝑁 Mat 𝑃 )
6 chpmatval2.m1 = ( -g𝑌 )
7 chpmatval2.x 𝑋 = ( var1𝑅 )
8 chpmatval2.t1 · = ( ·𝑠𝑌 )
9 chpmatval2.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
10 chpmatval2.i 1 = ( 1r𝑌 )
11 chpmatval2.g 𝐺 = ( SymGrp ‘ 𝑁 )
12 chpmatval2.h 𝐻 = ( Base ‘ 𝐺 )
13 chpmatval2.z 𝑍 = ( ℤRHom ‘ 𝑃 )
14 chpmatval2.s 𝑆 = ( pmSgn ‘ 𝑁 )
15 chpmatval2.u 𝑈 = ( mulGrp ‘ 𝑃 )
16 chpmatval2.rm × = ( .r𝑃 )
17 eqid ( 𝑁 maDet 𝑃 ) = ( 𝑁 maDet 𝑃 )
18 1 2 3 4 5 17 6 7 8 9 10 chpmatval ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝐶𝑀 ) = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) ) )
19 eqid ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat 𝑃 )
20 5 fveq2i ( -g𝑌 ) = ( -g ‘ ( 𝑁 Mat 𝑃 ) )
21 6 20 eqtri = ( -g ‘ ( 𝑁 Mat 𝑃 ) )
22 5 fveq2i ( ·𝑠𝑌 ) = ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) )
23 8 22 eqtri · = ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) )
24 5 fveq2i ( 1r𝑌 ) = ( 1r ‘ ( 𝑁 Mat 𝑃 ) )
25 10 24 eqtri 1 = ( 1r ‘ ( 𝑁 Mat 𝑃 ) )
26 eqid ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) = ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) )
27 2 3 4 19 7 9 21 23 25 26 chmatcl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
28 5 eqcomi ( 𝑁 Mat 𝑃 ) = 𝑌
29 28 fveq2i ( Base ‘ ( 𝑁 Mat 𝑃 ) ) = ( Base ‘ 𝑌 )
30 11 fveq2i ( Base ‘ 𝐺 ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
31 12 30 eqtri 𝐻 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
32 17 5 29 31 13 14 16 15 mdetleib ( ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) ) = ( 𝑃 Σg ( 𝑝𝐻 ↦ ( ( ( 𝑍𝑆 ) ‘ 𝑝 ) × ( 𝑈 Σg ( 𝑥𝑁 ↦ ( ( 𝑝𝑥 ) ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) 𝑥 ) ) ) ) ) ) )
33 27 32 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) ) = ( 𝑃 Σg ( 𝑝𝐻 ↦ ( ( ( 𝑍𝑆 ) ‘ 𝑝 ) × ( 𝑈 Σg ( 𝑥𝑁 ↦ ( ( 𝑝𝑥 ) ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) 𝑥 ) ) ) ) ) ) )
34 18 33 eqtrd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝐶𝑀 ) = ( 𝑃 Σg ( 𝑝𝐻 ↦ ( ( ( 𝑍𝑆 ) ‘ 𝑝 ) × ( 𝑈 Σg ( 𝑥𝑁 ↦ ( ( 𝑝𝑥 ) ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) 𝑥 ) ) ) ) ) ) )