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

Theorem cpmidgsum2 19562
 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 19561 . 2 g
18 crngring 17419 . . . . . . . . . . . . 13
1918anim2i 567 . . . . . . . . . . . 12
20193adant3 1015 . . . . . . . . . . 11
213, 4pmatring 19376 . . . . . . . . . . 11
22 ringgrp 17413 . . . . . . . . . . 11
2320, 21, 223syl 20 . . . . . . . . . 10
243, 4pmatlmod 19377 . . . . . . . . . . . . 13
2518, 24sylan2 472 . . . . . . . . . . . 12
2618adantl 464 . . . . . . . . . . . . . 14
27 eqid 2400 . . . . . . . . . . . . . . 15
286, 3, 27vr1cl 18468 . . . . . . . . . . . . . 14
2926, 28syl 17 . . . . . . . . . . . . 13
303ply1crng 18447 . . . . . . . . . . . . . . 15
314matsca2 19104 . . . . . . . . . . . . . . 15 Scalar
3230, 31sylan2 472 . . . . . . . . . . . . . 14 Scalar
3332fveq2d 5807 . . . . . . . . . . . . 13 Scalar
3429, 33eleqtrd 2490 . . . . . . . . . . . 12 Scalar
35 eqid 2400 . . . . . . . . . . . . . 14
3635, 10ringidcl 17429 . . . . . . . . . . . . 13
3719, 21, 363syl 20 . . . . . . . . . . . 12
38 eqid 2400 . . . . . . . . . . . . 13 Scalar Scalar
39 eqid 2400 . . . . . . . . . . . . 13 Scalar Scalar
4035, 38, 8, 39lmodvscl 17739 . . . . . . . . . . . 12 Scalar
4125, 34, 37, 40syl3anc 1228 . . . . . . . . . . 11
42413adant3 1015 . . . . . . . . . 10
435, 1, 2, 3, 4mat2pmatbas 19409 . . . . . . . . . . 11
4418, 43syl3an2 1262 . . . . . . . . . 10
4535, 12grpsubcl 16332 . . . . . . . . . 10
4623, 42, 44, 45syl3anc 1228 . . . . . . . . 9
47303ad2ant2 1017 . . . . . . . . 9
48 eqid 2400 . . . . . . . . . 10 maDet maDet
494, 35, 14, 48, 10, 9, 8madurid 19328 . . . . . . . . 9 maDet
5046, 47, 49syl2anc 659 . . . . . . . 8 maDet
51 id 22 . . . . . . . . . 10
52 fveq2 5803 . . . . . . . . . 10
5351, 52oveq12d 6250 . . . . . . . . 9
5413, 53mp1i 13 . . . . . . . 8
55 cpmidgsum2.h . . . . . . . . 9
56 cpmidgsum2.k . . . . . . . . . . 11
57 cpmidgsum2.c . . . . . . . . . . . 12 CharPlyMat
5857, 1, 2, 3, 4, 48, 12, 6, 8, 5, 10chpmatval 19514 . . . . . . . . . . 11 maDet
5956, 58syl5eq 2453 . . . . . . . . . 10 maDet
6059oveq1d 6247 . . . . . . . . 9 maDet
6155, 60syl5eq 2453 . . . . . . . 8 maDet
6250, 54, 613eqtr4rd 2452 . . . . . . 7
6362adantr 463 . . . . . 6 g
64 simpr 459 . . . . . 6 g g
6563, 64eqtrd 2441 . . . . 5 g g
6665ex 432 . . . 4 g g
6766reximdv 2875 . . 3 g g
6867reximdv 2875 . 2 g g
6917, 68mpd 15 1 g