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

Theorem cpmidgsum2 19147
 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
cpmidgsum2.c CharPlyMat
cpmidgsum2.k
cpmidgsum2.h
Assertion
Ref Expression
cpmidgsum2 g
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,,,   ,   ,   ,,,   ,,,   ,,,,   ,,,,   ,,,   ,,,   ,,   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,   ,   ,   ,   ,
Allowed substitution hints:   ()   (,,,)   (,)   (,,,)   (,)   (,,)   (,,)   (,,,)   (,,,)   (,)   (,,)

Proof of Theorem cpmidgsum2
StepHypRef Expression
1 cpmadugsum.a . . 3 Mat
3 cpmadugsum.p . . 3 Poly1
4 cpmadugsum.y . . 3 Mat
5 cpmadugsum.t . . 3 matToPolyMat
6 cpmadugsum.x . . 3 var1
7 cpmadugsum.e . . 3 .gmulGrp
171, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16cpmadugsum 19146 . 2 g
18 crngrng 16996 . . . . . . . . . . . . 13
1918anim2i 569 . . . . . . . . . . . 12
20193adant3 1016 . . . . . . . . . . 11
213, 4pmatrng 18961 . . . . . . . . . . 11
22 rnggrp 16991 . . . . . . . . . . 11
2320, 21, 223syl 20 . . . . . . . . . 10
243, 4pmatlmod 18962 . . . . . . . . . . . . 13
2518, 24sylan2 474 . . . . . . . . . . . 12
2618adantl 466 . . . . . . . . . . . . . 14
27 eqid 2467 . . . . . . . . . . . . . . 15
286, 3, 27vr1cl 18029 . . . . . . . . . . . . . 14
2926, 28syl 16 . . . . . . . . . . . . 13
303ply1crng 18008 . . . . . . . . . . . . . . 15
314matsca2 18689 . . . . . . . . . . . . . . 15 Scalar
3230, 31sylan2 474 . . . . . . . . . . . . . 14 Scalar
3332fveq2d 5868 . . . . . . . . . . . . 13 Scalar
3429, 33eleqtrd 2557 . . . . . . . . . . . 12 Scalar
35 eqid 2467 . . . . . . . . . . . . . 14
3635, 10rngidcl 17006 . . . . . . . . . . . . 13
3719, 21, 363syl 20 . . . . . . . . . . . 12
38 eqid 2467 . . . . . . . . . . . . 13 Scalar Scalar
39 eqid 2467 . . . . . . . . . . . . 13 Scalar Scalar
4035, 38, 8, 39lmodvscl 17312 . . . . . . . . . . . 12 Scalar
4125, 34, 37, 40syl3anc 1228 . . . . . . . . . . 11
42413adant3 1016 . . . . . . . . . 10
435, 1, 2, 3, 4mat2pmatbas 18994 . . . . . . . . . . 11
4418, 43syl3an2 1262 . . . . . . . . . 10
4535, 12grpsubcl 15919 . . . . . . . . . 10
4623, 42, 44, 45syl3anc 1228 . . . . . . . . 9
47303ad2ant2 1018 . . . . . . . . 9
48 eqid 2467 . . . . . . . . . 10 maDet maDet
494, 35, 14, 48, 10, 9, 8madurid 18913 . . . . . . . . 9 maDet
5046, 47, 49syl2anc 661 . . . . . . . 8 maDet
5113a1i 11 . . . . . . . . 9
52 id 22 . . . . . . . . . 10
53 fveq2 5864 . . . . . . . . . 10
5452, 53oveq12d 6300 . . . . . . . . 9
5551, 54syl 16 . . . . . . . 8
56 cpmidgsum2.h . . . . . . . . 9
57 cpmidgsum2.k . . . . . . . . . . 11
58 cpmidgsum2.c . . . . . . . . . . . 12 CharPlyMat
5958, 1, 2, 3, 4, 48, 12, 6, 8, 5, 10chpmatval 19099 . . . . . . . . . . 11 maDet
6057, 59syl5eq 2520 . . . . . . . . . 10 maDet
6160oveq1d 6297 . . . . . . . . 9 maDet
6256, 61syl5eq 2520 . . . . . . . 8 maDet
6350, 55, 623eqtr4rd 2519 . . . . . . 7
6463adantr 465 . . . . . 6 g
65 simpr 461 . . . . . 6 g g
6664, 65eqtrd 2508 . . . . 5 g g
6766ex 434 . . . 4 g g
6867reximdv 2937 . . 3 g g
6968reximdv 2937 . 2 g g
7017, 69mpd 15 1 g