# Metamath Proof Explorer

## Theorem chpscmat

Description: The characteristic polynomial of a (nonempty!) scalar matrix. (Contributed by AV, 21-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
chpscmat.d ${⊢}{D}=\left\{{m}\in {\mathrm{Base}}_{{A}}|\exists {c}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{m}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\right\}$
chpscmat.s ${⊢}{S}=\mathrm{algSc}\left({P}\right)$
chpscmat.m
Assertion chpscmat

### 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 chpscmat.d ${⊢}{D}=\left\{{m}\in {\mathrm{Base}}_{{A}}|\exists {c}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{m}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\right\}$
8 chpscmat.s ${⊢}{S}=\mathrm{algSc}\left({P}\right)$
9 chpscmat.m
10 simpll ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\right)\to {N}\in \mathrm{Fin}$
11 simplr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\right)\to {R}\in \mathrm{CRing}$
12 elrabi ${⊢}{M}\in \left\{{m}\in {\mathrm{Base}}_{{A}}|\exists {c}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{m}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\right\}\to {M}\in {\mathrm{Base}}_{{A}}$
13 12 7 eleq2s ${⊢}{M}\in {D}\to {M}\in {\mathrm{Base}}_{{A}}$
14 13 3ad2ant1 ${⊢}\left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\to {M}\in {\mathrm{Base}}_{{A}}$
15 14 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\right)\to {M}\in {\mathrm{Base}}_{{A}}$
16 oveq ${⊢}{m}={M}\to {i}{m}{j}={i}{M}{j}$
17 16 eqeq1d ${⊢}{m}={M}\to \left({i}{m}{j}=if\left({i}={j},{c},{0}_{{R}}\right)↔{i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\right)$
18 17 2ralbidv ${⊢}{m}={M}\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{m}{j}=if\left({i}={j},{c},{0}_{{R}}\right)↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\right)$
19 18 rexbidv ${⊢}{m}={M}\to \left(\exists {c}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{m}{j}=if\left({i}={j},{c},{0}_{{R}}\right)↔\exists {c}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\right)$
20 19 elrab ${⊢}{M}\in \left\{{m}\in {\mathrm{Base}}_{{A}}|\exists {c}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{m}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\right\}↔\left({M}\in {\mathrm{Base}}_{{A}}\wedge \exists {c}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\right)$
21 ifnefalse ${⊢}{i}\ne {j}\to if\left({i}={j},{c},{0}_{{R}}\right)={0}_{{R}}$
22 21 eqeq2d ${⊢}{i}\ne {j}\to \left({i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)↔{i}{M}{j}={0}_{{R}}\right)$
23 22 biimpcd ${⊢}{i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\to \left({i}\ne {j}\to {i}{M}{j}={0}_{{R}}\right)$
24 23 a1i ${⊢}\left(\left(\left(\left({M}\in {\mathrm{Base}}_{{A}}\wedge {c}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {i}\in {N}\right)\wedge {j}\in {N}\right)\to \left({i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\to \left({i}\ne {j}\to {i}{M}{j}={0}_{{R}}\right)\right)$
25 24 ralimdva ${⊢}\left(\left(\left({M}\in {\mathrm{Base}}_{{A}}\wedge {c}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {i}\in {N}\right)\to \left(\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\to \forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}\ne {j}\to {i}{M}{j}={0}_{{R}}\right)\right)$
26 25 ralimdva ${⊢}\left(\left({M}\in {\mathrm{Base}}_{{A}}\wedge {c}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}\ne {j}\to {i}{M}{j}={0}_{{R}}\right)\right)$
27 26 ex ${⊢}\left({M}\in {\mathrm{Base}}_{{A}}\wedge {c}\in {\mathrm{Base}}_{{R}}\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}\ne {j}\to {i}{M}{j}={0}_{{R}}\right)\right)\right)$
28 27 com23 ${⊢}\left({M}\in {\mathrm{Base}}_{{A}}\wedge {c}\in {\mathrm{Base}}_{{R}}\right)\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}\ne {j}\to {i}{M}{j}={0}_{{R}}\right)\right)\right)$
29 28 rexlimdva ${⊢}{M}\in {\mathrm{Base}}_{{A}}\to \left(\exists {c}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}\ne {j}\to {i}{M}{j}={0}_{{R}}\right)\right)\right)$
30 29 imp ${⊢}\left({M}\in {\mathrm{Base}}_{{A}}\wedge \exists {c}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}\ne {j}\to {i}{M}{j}={0}_{{R}}\right)\right)$
31 20 30 sylbi ${⊢}{M}\in \left\{{m}\in {\mathrm{Base}}_{{A}}|\exists {c}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{m}{j}=if\left({i}={j},{c},{0}_{{R}}\right)\right\}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}\ne {j}\to {i}{M}{j}={0}_{{R}}\right)\right)$
32 31 7 eleq2s ${⊢}{M}\in {D}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}\ne {j}\to {i}{M}{j}={0}_{{R}}\right)\right)$
33 32 3ad2ant1 ${⊢}\left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}\ne {j}\to {i}{M}{j}={0}_{{R}}\right)\right)$
34 33 impcom ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}\ne {j}\to {i}{M}{j}={0}_{{R}}\right)$
35 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
36 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
37 1 2 3 8 35 4 36 5 9 chpdmat
38 10 11 15 34 37 syl31anc
39 id ${⊢}{n}={k}\to {n}={k}$
40 39 39 oveq12d ${⊢}{n}={k}\to {n}{M}{n}={k}{M}{k}$
41 40 eqeq1d ${⊢}{n}={k}\to \left({n}{M}{n}={E}↔{k}{M}{k}={E}\right)$
42 41 rspccv ${⊢}\forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\to \left({k}\in {N}\to {k}{M}{k}={E}\right)$
43 42 3ad2ant3 ${⊢}\left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\to \left({k}\in {N}\to {k}{M}{k}={E}\right)$
44 43 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\right)\to \left({k}\in {N}\to {k}{M}{k}={E}\right)$
45 44 imp ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\right)\wedge {k}\in {N}\right)\to {k}{M}{k}={E}$
46 45 fveq2d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\right)\wedge {k}\in {N}\right)\to {S}\left({k}{M}{k}\right)={S}\left({E}\right)$
47 46 oveq2d
48 47 mpteq2dva
49 48 oveq2d
50 2 ply1crng ${⊢}{R}\in \mathrm{CRing}\to {P}\in \mathrm{CRing}$
51 5 crngmgp ${⊢}{P}\in \mathrm{CRing}\to {G}\in \mathrm{CMnd}$
52 cmnmnd ${⊢}{G}\in \mathrm{CMnd}\to {G}\in \mathrm{Mnd}$
53 50 51 52 3syl ${⊢}{R}\in \mathrm{CRing}\to {G}\in \mathrm{Mnd}$
54 53 ad2antlr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\right)\to {G}\in \mathrm{Mnd}$
55 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
56 2 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
57 55 56 syl ${⊢}{R}\in \mathrm{CRing}\to {P}\in \mathrm{Ring}$
58 ringgrp ${⊢}{P}\in \mathrm{Ring}\to {P}\in \mathrm{Grp}$
59 57 58 syl ${⊢}{R}\in \mathrm{CRing}\to {P}\in \mathrm{Grp}$
60 59 ad2antlr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\right)\to {P}\in \mathrm{Grp}$
61 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
62 4 2 61 vr1cl ${⊢}{R}\in \mathrm{Ring}\to {X}\in {\mathrm{Base}}_{{P}}$
63 55 62 syl ${⊢}{R}\in \mathrm{CRing}\to {X}\in {\mathrm{Base}}_{{P}}$
64 63 ad2antlr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\right)\to {X}\in {\mathrm{Base}}_{{P}}$
65 simpr ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to {I}\in {N}$
66 eqid ${⊢}\mathrm{Scalar}\left({P}\right)=\mathrm{Scalar}\left({P}\right)$
67 57 ad2antll ${⊢}\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\to {P}\in \mathrm{Ring}$
68 67 adantr ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to {P}\in \mathrm{Ring}$
69 2 ply1lmod ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{LMod}$
70 55 69 syl ${⊢}{R}\in \mathrm{CRing}\to {P}\in \mathrm{LMod}$
71 70 ad2antll ${⊢}\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\to {P}\in \mathrm{LMod}$
72 71 adantr ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to {P}\in \mathrm{LMod}$
73 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}$
74 8 66 68 72 73 61 asclf ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to {S}:{\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}⟶{\mathrm{Base}}_{{P}}$
75 13 adantr ${⊢}\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\to {M}\in {\mathrm{Base}}_{{A}}$
76 75 adantr ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to {M}\in {\mathrm{Base}}_{{A}}$
77 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
78 3 77 matecl ${⊢}\left({I}\in {N}\wedge {I}\in {N}\wedge {M}\in {\mathrm{Base}}_{{A}}\right)\to {I}{M}{I}\in {\mathrm{Base}}_{{R}}$
79 65 65 76 78 syl3anc ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to {I}{M}{I}\in {\mathrm{Base}}_{{R}}$
80 2 ply1sca ${⊢}{R}\in \mathrm{CRing}\to {R}=\mathrm{Scalar}\left({P}\right)$
81 80 ad2antll ${⊢}\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\to {R}=\mathrm{Scalar}\left({P}\right)$
82 81 adantr ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to {R}=\mathrm{Scalar}\left({P}\right)$
83 82 eqcomd ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to \mathrm{Scalar}\left({P}\right)={R}$
84 83 fveq2d ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{{R}}$
85 79 84 eleqtrrd ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to {I}{M}{I}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}$
86 74 85 ffvelrnd ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to {S}\left({I}{M}{I}\right)\in {\mathrm{Base}}_{{P}}$
87 fveq2 ${⊢}{E}={I}{M}{I}\to {S}\left({E}\right)={S}\left({I}{M}{I}\right)$
88 87 eqcoms ${⊢}{I}{M}{I}={E}\to {S}\left({E}\right)={S}\left({I}{M}{I}\right)$
89 88 eleq1d ${⊢}{I}{M}{I}={E}\to \left({S}\left({E}\right)\in {\mathrm{Base}}_{{P}}↔{S}\left({I}{M}{I}\right)\in {\mathrm{Base}}_{{P}}\right)$
90 86 89 syl5ibrcom ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to \left({I}{M}{I}={E}\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)$
91 90 adantr ${⊢}\left(\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\wedge {n}={I}\right)\to \left({I}{M}{I}={E}\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)$
92 id ${⊢}{n}={I}\to {n}={I}$
93 92 92 oveq12d ${⊢}{n}={I}\to {n}{M}{n}={I}{M}{I}$
94 93 eqeq1d ${⊢}{n}={I}\to \left({n}{M}{n}={E}↔{I}{M}{I}={E}\right)$
95 94 imbi1d ${⊢}{n}={I}\to \left(\left({n}{M}{n}={E}\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)↔\left({I}{M}{I}={E}\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)\right)$
96 95 adantl ${⊢}\left(\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\wedge {n}={I}\right)\to \left(\left({n}{M}{n}={E}\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)↔\left({I}{M}{I}={E}\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)\right)$
97 91 96 mpbird ${⊢}\left(\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\wedge {n}={I}\right)\to \left({n}{M}{n}={E}\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)$
98 65 97 rspcimdv ${⊢}\left(\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\wedge {I}\in {N}\right)\to \left(\forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)$
99 98 ex ${⊢}\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\to \left({I}\in {N}\to \left(\forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)\right)$
100 99 com23 ${⊢}\left({M}\in {D}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\right)\to \left(\forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\to \left({I}\in {N}\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)\right)$
101 100 ex ${⊢}{M}\in {D}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \left(\forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\to \left({I}\in {N}\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)\right)\right)$
102 101 com24 ${⊢}{M}\in {D}\to \left({I}\in {N}\to \left(\forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)\right)\right)$
103 102 3imp ${⊢}\left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}\right)$
104 103 impcom ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {D}\wedge {I}\in {N}\wedge \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{n}{M}{n}={E}\right)\right)\to {S}\left({E}\right)\in {\mathrm{Base}}_{{P}}$
105 61 9 grpsubcl
106 60 64 104 105 syl3anc
107 5 61 mgpbas ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{G}}$
108 106 107 eleqtrdi
109 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
110 109 6 gsumconst
111 54 10 108 110 syl3anc
112 38 49 111 3eqtrd