Metamath Proof Explorer

Theorem cpmidpmat

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as polynomial over the ring of matrices. (Contributed by AV, 14-Nov-2019) (Revised by AV, 7-Dec-2019)

Ref Expression
Hypotheses cpmidgsum.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
cpmidgsum.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
cpmidgsum.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cpmidgsum.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
cpmidgsum.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
cpmidgsum.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
cpmidgsum.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
cpmidgsum.1 ⊢ 1 = ( 1r ‘ 𝑌 )
cpmidgsum.u ⊢ 𝑈 = ( algSc ‘ 𝑃 )
cpmidgsum.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
cpmidgsum.k ⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
cpmidgsum.h ⊢ 𝐻 = ( 𝐾 · 1 )
cpmidgsumm2pm.o ⊢ 𝑂 = ( 1r ‘ 𝐴 )
cpmidgsumm2pm.m ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
cpmidgsumm2pm.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
cpmidgsum.w ⊢ 𝑊 = ( Base ‘ 𝑌 )
cpmidpmat.p ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
cpmidpmat.z ⊢ 𝑍 = ( var1 ‘ 𝐴 )
cpmidpmat.m ⊢ ∙ = ( ·𝑠 ‘ 𝑄 )
cpmidpmat.e ⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
cpmidpmat.i ⊢ 𝐼 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion cpmidpmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ‘ 𝐻 ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmidgsum.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 cpmidgsum.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 cpmidgsum.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 cpmidgsum.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5 cpmidgsum.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
6 cpmidgsum.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
7 cpmidgsum.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
8 cpmidgsum.1 ⊢ 1 = ( 1r ‘ 𝑌 )
9 cpmidgsum.u ⊢ 𝑈 = ( algSc ‘ 𝑃 )
10 cpmidgsum.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
11 cpmidgsum.k ⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
12 cpmidgsum.h ⊢ 𝐻 = ( 𝐾 · 1 )
13 cpmidgsumm2pm.o ⊢ 𝑂 = ( 1r ‘ 𝐴 )
14 cpmidgsumm2pm.m ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
15 cpmidgsumm2pm.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
16 cpmidgsum.w ⊢ 𝑊 = ( Base ‘ 𝑌 )
17 cpmidpmat.p ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
18 cpmidpmat.z ⊢ 𝑍 = ( var1 ‘ 𝐴 )
19 cpmidpmat.m ⊢ ∙ = ( ·𝑠 ‘ 𝑄 )
20 cpmidpmat.e ⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
21 cpmidpmat.i ⊢ 𝐼 = ( 𝑁 pMatToMatPoly 𝑅 )
22 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 cpmidgsumm2pm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐻 = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) ) ) ) )
23 22 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ‘ 𝐻 ) = ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) ) ) ) ) )
24 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) )
25 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 24 cpmidpmatlem1 ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) )
26 25 eqcomd ⊢ ( 𝑛 ∈ ℕ0 → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) )
27 26 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) )
28 27 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) = ( 𝑇 ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) )
29 28 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) ) = ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) )
30 29 mpteq2dva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) ) )
31 30 oveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) ) ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) ) ) )
32 31 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) ) ) ) ) = ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) ) ) ) )
33 3simpa ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
34 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 24 cpmidpmatlem2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ∈ ( 𝐵 ↑m ℕ0 ) )
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 24 cpmidpmatlem3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) finSupp ( 0g ‘ 𝐴 ) )
36 fveq2 ⊢ ( 𝑘 = 𝑥 → ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) )
37 36 oveq1d ⊢ ( 𝑘 = 𝑥 → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) )
38 37 cbvmptv ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) = ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) )
39 38 eleq1i ⊢ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ∈ ( 𝐵 ↑m ℕ0 ) ↔ ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ∈ ( 𝐵 ↑m ℕ0 ) )
40 38 breq1i ⊢ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) finSupp ( 0g ‘ 𝐴 ) ↔ ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) finSupp ( 0g ‘ 𝐴 ) )
41 39 40 anbi12i ⊢ ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ∈ ( 𝐵 ↑m ℕ0 ) ∧ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) finSupp ( 0g ‘ 𝐴 ) ) ↔ ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ∈ ( 𝐵 ↑m ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) finSupp ( 0g ‘ 𝐴 ) ) )
42 3 4 16 19 20 18 1 2 17 21 6 5 7 15 pm2mp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ∈ ( 𝐵 ↑m ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) ) )
43 41 42 sylan2b ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ∈ ( 𝐵 ↑m ℕ0 ) ∧ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) ) )
44 33 34 35 43 syl12anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) ) )
45 38 fveq1i ⊢ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) = ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 )
46 45 fveq2i ⊢ ( 𝑇 ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) = ( 𝑇 ‘ ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) )
47 46 oveq2i ⊢ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) = ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) )
48 47 mpteq2i ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) )
49 48 oveq2i ⊢ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) ) )
50 49 fveq2i ⊢ ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) ) ) ) = ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) ) ) )
51 45 oveq1i ⊢ ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) = ( ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) )
52 51 mpteq2i ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) )
53 52 oveq2i ⊢ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑥 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) )
54 44 50 53 3eqtr4g ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) ) )
55 32 54 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) ) )
56 25 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) )
57 56 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) = ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ∙ ( 𝑛 𝐸 𝑍 ) ) )
58 57 mpteq2dva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) )
59 58 oveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) ‘ 𝑛 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) ) )
60 23 55 59 3eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ‘ 𝐻 ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ∙ ( 𝑛 𝐸 𝑍 ) ) ) ) )