# Metamath Proof Explorer

## Theorem chp0mat

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

Ref Expression
Hypotheses chp0mat.c ${⊢}{C}={N}\mathrm{CharPlyMat}{R}$
chp0mat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
chp0mat.a ${⊢}{A}={N}\mathrm{Mat}{R}$
chp0mat.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
chp0mat.g ${⊢}{G}={\mathrm{mulGrp}}_{{P}}$
chp0mat.m
chp0mat.0
Assertion chp0mat

### Proof

Step Hyp Ref Expression
1 chp0mat.c ${⊢}{C}={N}\mathrm{CharPlyMat}{R}$
2 chp0mat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
3 chp0mat.a ${⊢}{A}={N}\mathrm{Mat}{R}$
4 chp0mat.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
5 chp0mat.g ${⊢}{G}={\mathrm{mulGrp}}_{{P}}$
6 chp0mat.m
7 chp0mat.0
8 simpl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {N}\in \mathrm{Fin}$
9 simpr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {R}\in \mathrm{CRing}$
10 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
11 3 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
12 10 11 sylan2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {A}\in \mathrm{Ring}$
13 ringgrp ${⊢}{A}\in \mathrm{Ring}\to {A}\in \mathrm{Grp}$
14 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
15 14 7 grpidcl
16 12 13 15 3syl
17 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
18 3 17 mat0op ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {0}_{{A}}=\left({x}\in {N},{y}\in {N}⟼{0}_{{R}}\right)$
19 7 18 syl5eq
20 10 19 sylan2
22 eqidd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({x}={i}\wedge {y}={j}\right)\right)\to {0}_{{R}}={0}_{{R}}$
23 simpl ${⊢}\left({i}\in {N}\wedge {j}\in {N}\right)\to {i}\in {N}$
24 23 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}\in {N}$
25 simpr ${⊢}\left({i}\in {N}\wedge {j}\in {N}\right)\to {j}\in {N}$
26 25 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {j}\in {N}$
27 fvexd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {0}_{{R}}\in \mathrm{V}$
28 21 22 24 26 27 ovmpod
29 28 a1d
30 29 ralrimivva
31 eqid ${⊢}\mathrm{algSc}\left({P}\right)=\mathrm{algSc}\left({P}\right)$
32 eqid ${⊢}{-}_{{P}}={-}_{{P}}$
33 1 2 3 31 14 4 17 5 32 chpdmat
34 8 9 16 30 33 syl31anc
36 eqidd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {k}\in {N}\right)\wedge \left({x}={k}\wedge {y}={k}\right)\right)\to {0}_{{R}}={0}_{{R}}$
37 simpr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {k}\in {N}\right)\to {k}\in {N}$
38 fvexd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {k}\in {N}\right)\to {0}_{{R}}\in \mathrm{V}$
39 35 36 37 37 38 ovmpod
40 39 fveq2d
41 10 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {R}\in \mathrm{Ring}$
42 eqid ${⊢}{0}_{{P}}={0}_{{P}}$
43 2 31 17 42 ply1scl0 ${⊢}{R}\in \mathrm{Ring}\to \mathrm{algSc}\left({P}\right)\left({0}_{{R}}\right)={0}_{{P}}$
44 41 43 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \mathrm{algSc}\left({P}\right)\left({0}_{{R}}\right)={0}_{{P}}$
45 44 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {k}\in {N}\right)\to \mathrm{algSc}\left({P}\right)\left({0}_{{R}}\right)={0}_{{P}}$
46 40 45 eqtrd
47 46 oveq2d
48 2 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
49 ringgrp ${⊢}{P}\in \mathrm{Ring}\to {P}\in \mathrm{Grp}$
50 10 48 49 3syl ${⊢}{R}\in \mathrm{CRing}\to {P}\in \mathrm{Grp}$
51 50 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {P}\in \mathrm{Grp}$
52 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
53 4 2 52 vr1cl ${⊢}{R}\in \mathrm{Ring}\to {X}\in {\mathrm{Base}}_{{P}}$
54 41 53 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {X}\in {\mathrm{Base}}_{{P}}$
55 51 54 jca ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \left({P}\in \mathrm{Grp}\wedge {X}\in {\mathrm{Base}}_{{P}}\right)$
56 55 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {k}\in {N}\right)\to \left({P}\in \mathrm{Grp}\wedge {X}\in {\mathrm{Base}}_{{P}}\right)$
57 52 42 32 grpsubid1 ${⊢}\left({P}\in \mathrm{Grp}\wedge {X}\in {\mathrm{Base}}_{{P}}\right)\to {X}{-}_{{P}}{0}_{{P}}={X}$
58 56 57 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {k}\in {N}\right)\to {X}{-}_{{P}}{0}_{{P}}={X}$
59 47 58 eqtrd
60 59 mpteq2dva
61 60 oveq2d
62 2 ply1crng ${⊢}{R}\in \mathrm{CRing}\to {P}\in \mathrm{CRing}$
63 5 crngmgp ${⊢}{P}\in \mathrm{CRing}\to {G}\in \mathrm{CMnd}$
64 cmnmnd ${⊢}{G}\in \mathrm{CMnd}\to {G}\in \mathrm{Mnd}$
65 62 63 64 3syl ${⊢}{R}\in \mathrm{CRing}\to {G}\in \mathrm{Mnd}$
66 65 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {G}\in \mathrm{Mnd}$
67 10 53 syl ${⊢}{R}\in \mathrm{CRing}\to {X}\in {\mathrm{Base}}_{{P}}$
68 67 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {X}\in {\mathrm{Base}}_{{P}}$
69 5 52 mgpbas ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{G}}$
70 68 69 eleqtrdi ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {X}\in {\mathrm{Base}}_{{G}}$
71 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
72 71 6 gsumconst
73 66 8 70 72 syl3anc
74 34 61 73 3eqtrd