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 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
chp0mat.p 𝑃 = ( Poly1𝑅 )
chp0mat.a 𝐴 = ( 𝑁 Mat 𝑅 )
chp0mat.x 𝑋 = ( var1𝑅 )
chp0mat.g 𝐺 = ( mulGrp ‘ 𝑃 )
chp0mat.m = ( .g𝐺 )
chpscmat.d 𝐷 = { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) }
chpscmat.s 𝑆 = ( algSc ‘ 𝑃 )
chpscmat.m = ( -g𝑃 )
Assertion chpscmat ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → ( 𝐶𝑀 ) = ( ( ♯ ‘ 𝑁 ) ( 𝑋 ( 𝑆𝐸 ) ) ) )

Proof

Step Hyp Ref Expression
1 chp0mat.c 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2 chp0mat.p 𝑃 = ( Poly1𝑅 )
3 chp0mat.a 𝐴 = ( 𝑁 Mat 𝑅 )
4 chp0mat.x 𝑋 = ( var1𝑅 )
5 chp0mat.g 𝐺 = ( mulGrp ‘ 𝑃 )
6 chp0mat.m = ( .g𝐺 )
7 chpscmat.d 𝐷 = { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) }
8 chpscmat.s 𝑆 = ( algSc ‘ 𝑃 )
9 chpscmat.m = ( -g𝑃 )
10 simpll ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → 𝑁 ∈ Fin )
11 simplr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → 𝑅 ∈ CRing )
12 elrabi ( 𝑀 ∈ { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) } → 𝑀 ∈ ( Base ‘ 𝐴 ) )
13 12 7 eleq2s ( 𝑀𝐷𝑀 ∈ ( Base ‘ 𝐴 ) )
14 13 3ad2ant1 ( ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
15 14 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
16 oveq ( 𝑚 = 𝑀 → ( 𝑖 𝑚 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
17 16 eqeq1d ( 𝑚 = 𝑀 → ( ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) ↔ ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) ) )
18 17 2ralbidv ( 𝑚 = 𝑀 → ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) ↔ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) ) )
19 18 rexbidv ( 𝑚 = 𝑀 → ( ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) ↔ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) ) )
20 19 elrab ( 𝑀 ∈ { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) } ↔ ( 𝑀 ∈ ( Base ‘ 𝐴 ) ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) ) )
21 ifnefalse ( 𝑖𝑗 → if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) = ( 0g𝑅 ) )
22 21 eqeq2d ( 𝑖𝑗 → ( ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) ↔ ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) )
23 22 biimpcd ( ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) → ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) )
24 23 a1i ( ( ( ( ( 𝑀 ∈ ( Base ‘ 𝐴 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝑖𝑁 ) ∧ 𝑗𝑁 ) → ( ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) → ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) ) )
25 24 ralimdva ( ( ( ( 𝑀 ∈ ( Base ‘ 𝐴 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝑖𝑁 ) → ( ∀ 𝑗𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) → ∀ 𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) ) )
26 25 ralimdva ( ( ( 𝑀 ∈ ( Base ‘ 𝐴 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) → ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) ) )
27 26 ex ( ( 𝑀 ∈ ( Base ‘ 𝐴 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) ) ) )
28 27 com23 ( ( 𝑀 ∈ ( Base ‘ 𝐴 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) ) ) )
29 28 rexlimdva ( 𝑀 ∈ ( Base ‘ 𝐴 ) → ( ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) ) ) )
30 29 imp ( ( 𝑀 ∈ ( Base ‘ 𝐴 ) ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) ) )
31 20 30 sylbi ( 𝑀 ∈ { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g𝑅 ) ) } → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) ) )
32 31 7 eleq2s ( 𝑀𝐷 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) ) )
33 32 3ad2ant1 ( ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) ) )
34 33 impcom ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) )
35 eqid ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
36 eqid ( 0g𝑅 ) = ( 0g𝑅 )
37 1 2 3 8 35 4 36 5 9 chpdmat ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) ∧ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g𝑅 ) ) ) → ( 𝐶𝑀 ) = ( 𝐺 Σg ( 𝑘𝑁 ↦ ( 𝑋 ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) ) ) )
38 10 11 15 34 37 syl31anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → ( 𝐶𝑀 ) = ( 𝐺 Σg ( 𝑘𝑁 ↦ ( 𝑋 ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) ) ) )
39 id ( 𝑛 = 𝑘𝑛 = 𝑘 )
40 39 39 oveq12d ( 𝑛 = 𝑘 → ( 𝑛 𝑀 𝑛 ) = ( 𝑘 𝑀 𝑘 ) )
41 40 eqeq1d ( 𝑛 = 𝑘 → ( ( 𝑛 𝑀 𝑛 ) = 𝐸 ↔ ( 𝑘 𝑀 𝑘 ) = 𝐸 ) )
42 41 rspccv ( ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 → ( 𝑘𝑁 → ( 𝑘 𝑀 𝑘 ) = 𝐸 ) )
43 42 3ad2ant3 ( ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) → ( 𝑘𝑁 → ( 𝑘 𝑀 𝑘 ) = 𝐸 ) )
44 43 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → ( 𝑘𝑁 → ( 𝑘 𝑀 𝑘 ) = 𝐸 ) )
45 44 imp ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) ∧ 𝑘𝑁 ) → ( 𝑘 𝑀 𝑘 ) = 𝐸 )
46 45 fveq2d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) ∧ 𝑘𝑁 ) → ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) = ( 𝑆𝐸 ) )
47 46 oveq2d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) ∧ 𝑘𝑁 ) → ( 𝑋 ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) = ( 𝑋 ( 𝑆𝐸 ) ) )
48 47 mpteq2dva ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → ( 𝑘𝑁 ↦ ( 𝑋 ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) ) = ( 𝑘𝑁 ↦ ( 𝑋 ( 𝑆𝐸 ) ) ) )
49 48 oveq2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → ( 𝐺 Σg ( 𝑘𝑁 ↦ ( 𝑋 ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) ) ) = ( 𝐺 Σg ( 𝑘𝑁 ↦ ( 𝑋 ( 𝑆𝐸 ) ) ) ) )
50 2 ply1crng ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
51 5 crngmgp ( 𝑃 ∈ CRing → 𝐺 ∈ CMnd )
52 cmnmnd ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
53 50 51 52 3syl ( 𝑅 ∈ CRing → 𝐺 ∈ Mnd )
54 53 ad2antlr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → 𝐺 ∈ Mnd )
55 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
56 2 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
57 55 56 syl ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
58 ringgrp ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
59 57 58 syl ( 𝑅 ∈ CRing → 𝑃 ∈ Grp )
60 59 ad2antlr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → 𝑃 ∈ Grp )
61 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
62 4 2 61 vr1cl ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
63 55 62 syl ( 𝑅 ∈ CRing → 𝑋 ∈ ( Base ‘ 𝑃 ) )
64 63 ad2antlr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
65 simpr ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → 𝐼𝑁 )
66 eqid ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
67 57 ad2antll ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) → 𝑃 ∈ Ring )
68 67 adantr ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → 𝑃 ∈ Ring )
69 2 ply1lmod ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
70 55 69 syl ( 𝑅 ∈ CRing → 𝑃 ∈ LMod )
71 70 ad2antll ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) → 𝑃 ∈ LMod )
72 71 adantr ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → 𝑃 ∈ LMod )
73 eqid ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
74 8 66 68 72 73 61 asclf ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → 𝑆 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ ( Base ‘ 𝑃 ) )
75 13 adantr ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
76 75 adantr ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
77 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
78 3 77 matecl ( ( 𝐼𝑁𝐼𝑁𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐼 𝑀 𝐼 ) ∈ ( Base ‘ 𝑅 ) )
79 65 65 76 78 syl3anc ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → ( 𝐼 𝑀 𝐼 ) ∈ ( Base ‘ 𝑅 ) )
80 2 ply1sca ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
81 80 ad2antll ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
82 81 adantr ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
83 82 eqcomd ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
84 83 fveq2d ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
85 79 84 eleqtrrd ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → ( 𝐼 𝑀 𝐼 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
86 74 85 ffvelrnd ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ∈ ( Base ‘ 𝑃 ) )
87 fveq2 ( 𝐸 = ( 𝐼 𝑀 𝐼 ) → ( 𝑆𝐸 ) = ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) )
88 87 eqcoms ( ( 𝐼 𝑀 𝐼 ) = 𝐸 → ( 𝑆𝐸 ) = ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) )
89 88 eleq1d ( ( 𝐼 𝑀 𝐼 ) = 𝐸 → ( ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ↔ ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ∈ ( Base ‘ 𝑃 ) ) )
90 86 89 syl5ibrcom ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → ( ( 𝐼 𝑀 𝐼 ) = 𝐸 → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) )
91 90 adantr ( ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) ∧ 𝑛 = 𝐼 ) → ( ( 𝐼 𝑀 𝐼 ) = 𝐸 → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) )
92 id ( 𝑛 = 𝐼𝑛 = 𝐼 )
93 92 92 oveq12d ( 𝑛 = 𝐼 → ( 𝑛 𝑀 𝑛 ) = ( 𝐼 𝑀 𝐼 ) )
94 93 eqeq1d ( 𝑛 = 𝐼 → ( ( 𝑛 𝑀 𝑛 ) = 𝐸 ↔ ( 𝐼 𝑀 𝐼 ) = 𝐸 ) )
95 94 imbi1d ( 𝑛 = 𝐼 → ( ( ( 𝑛 𝑀 𝑛 ) = 𝐸 → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) ↔ ( ( 𝐼 𝑀 𝐼 ) = 𝐸 → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) ) )
96 95 adantl ( ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) ∧ 𝑛 = 𝐼 ) → ( ( ( 𝑛 𝑀 𝑛 ) = 𝐸 → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) ↔ ( ( 𝐼 𝑀 𝐼 ) = 𝐸 → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) ) )
97 91 96 mpbird ( ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) ∧ 𝑛 = 𝐼 ) → ( ( 𝑛 𝑀 𝑛 ) = 𝐸 → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) )
98 65 97 rspcimdv ( ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) ∧ 𝐼𝑁 ) → ( ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) )
99 98 ex ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) → ( 𝐼𝑁 → ( ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) ) )
100 99 com23 ( ( 𝑀𝐷 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ) → ( ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 → ( 𝐼𝑁 → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) ) )
101 100 ex ( 𝑀𝐷 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 → ( 𝐼𝑁 → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) ) ) )
102 101 com24 ( 𝑀𝐷 → ( 𝐼𝑁 → ( ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) ) ) )
103 102 3imp ( ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) )
104 103 impcom ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) )
105 61 9 grpsubcl ( ( 𝑃 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑆𝐸 ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 ( 𝑆𝐸 ) ) ∈ ( Base ‘ 𝑃 ) )
106 60 64 104 105 syl3anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → ( 𝑋 ( 𝑆𝐸 ) ) ∈ ( Base ‘ 𝑃 ) )
107 5 61 mgpbas ( Base ‘ 𝑃 ) = ( Base ‘ 𝐺 )
108 106 107 eleqtrdi ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → ( 𝑋 ( 𝑆𝐸 ) ) ∈ ( Base ‘ 𝐺 ) )
109 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
110 109 6 gsumconst ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ Fin ∧ ( 𝑋 ( 𝑆𝐸 ) ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg ( 𝑘𝑁 ↦ ( 𝑋 ( 𝑆𝐸 ) ) ) ) = ( ( ♯ ‘ 𝑁 ) ( 𝑋 ( 𝑆𝐸 ) ) ) )
111 54 10 108 110 syl3anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → ( 𝐺 Σg ( 𝑘𝑁 ↦ ( 𝑋 ( 𝑆𝐸 ) ) ) ) = ( ( ♯ ‘ 𝑁 ) ( 𝑋 ( 𝑆𝐸 ) ) ) )
112 38 49 111 3eqtrd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀𝐷𝐼𝑁 ∧ ∀ 𝑛𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → ( 𝐶𝑀 ) = ( ( ♯ ‘ 𝑁 ) ( 𝑋 ( 𝑆𝐸 ) ) ) )