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 ffvelcdmd ⊢ ( ( ( 𝑀 ∈ 𝐷 ∧ ( 𝑁 ∈ 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 ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = 𝐸 ) ) → ( 𝐶 ‘ 𝑀 ) = ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 − ( 𝑆 ‘ 𝐸 ) ) ) )