Metamath Proof Explorer

Theorem pm2mp

Description: The transformation of a sum of matrices having scaled monomials with the same power as entries into a sum of scaled monomials as a polynomial over matrices. (Contributed by AV, 12-Nov-2019) (Revised by AV, 7-Dec-2019)

Ref Expression
Hypotheses monmat2matmon.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
monmat2matmon.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
monmat2matmon.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
monmat2matmon.m1 ⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
monmat2matmon.e1 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
monmat2matmon.x ⊢ 𝑋 = ( var1 ‘ 𝐴 )
monmat2matmon.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
monmat2matmon.k ⊢ 𝐾 = ( Base ‘ 𝐴 )
monmat2matmon.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
monmat2matmon.i ⊢ 𝐼 = ( 𝑁 pMatToMatPoly 𝑅 )
monmat2matmon.e2 ⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
monmat2matmon.y ⊢ 𝑌 = ( var1 ‘ 𝑅 )
monmat2matmon.m2 ⊢ · = ( ·𝑠 ‘ 𝐶 )
monmat2matmon.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion pm2mp ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝐼 ‘ ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑀 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 monmat2matmon.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 monmat2matmon.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 monmat2matmon.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 monmat2matmon.m1 ⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
5 monmat2matmon.e1 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6 monmat2matmon.x ⊢ 𝑋 = ( var1 ‘ 𝐴 )
7 monmat2matmon.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
8 monmat2matmon.k ⊢ 𝐾 = ( Base ‘ 𝐴 )
9 monmat2matmon.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
10 monmat2matmon.i ⊢ 𝐼 = ( 𝑁 pMatToMatPoly 𝑅 )
11 monmat2matmon.e2 ⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
12 monmat2matmon.y ⊢ 𝑌 = ( var1 ‘ 𝑅 )
13 monmat2matmon.m2 ⊢ · = ( ·𝑠 ‘ 𝐶 )
14 monmat2matmon.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
15 eqid ⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
16 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
17 16 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
18 1 2 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
19 ringcmn ⊢ ( 𝐶 ∈ Ring → 𝐶 ∈ CMnd )
20 17 18 19 3syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐶 ∈ CMnd )
21 20 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → 𝐶 ∈ CMnd )
22 7 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
23 16 22 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
24 9 ply1ring ⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ Ring )
25 ringmnd ⊢ ( 𝑄 ∈ Ring → 𝑄 ∈ Mnd )
26 23 24 25 3syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑄 ∈ Mnd )
27 26 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → 𝑄 ∈ Mnd )
28 nn0ex ⊢ ℕ0 ∈ V
29 28 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ℕ0 ∈ V )
30 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
31 1 2 3 4 5 6 7 9 30 10 pm2mpghm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 ∈ ( 𝐶 GrpHom 𝑄 ) )
32 16 31 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐼 ∈ ( 𝐶 GrpHom 𝑄 ) )
33 32 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → 𝐼 ∈ ( 𝐶 GrpHom 𝑄 ) )
34 ghmmhm ⊢ ( 𝐼 ∈ ( 𝐶 GrpHom 𝑄 ) → 𝐼 ∈ ( 𝐶 MndHom 𝑄 ) )
35 33 34 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → 𝐼 ∈ ( 𝐶 MndHom 𝑄 ) )
36 17 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
37 36 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
38 elmapi ⊢ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) → 𝑀 : ℕ0 ⟶ 𝐾 )
39 38 adantr ⊢ ( ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) → 𝑀 : ℕ0 ⟶ 𝐾 )
40 39 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → 𝑀 : ℕ0 ⟶ 𝐾 )
41 40 ffvelcdmda ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 ‘ 𝑛 ) ∈ 𝐾 )
42 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
43 7 8 14 1 2 3 13 11 12 mat2pmatscmxcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑀 ‘ 𝑛 ) ∈ 𝐾 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ∈ 𝐵 )
44 37 41 42 43 syl12anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ∈ 𝐵 )
45 fvexd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 0g ‘ 𝐶 ) ∈ V )
46 ovexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ∈ V )
47 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) → 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) )
48 fvex ⊢ ( 0g ‘ 𝐴 ) ∈ V
49 fsuppmapnn0ub ⊢ ( ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ ( 0g ‘ 𝐴 ) ∈ V ) → ( 𝑀 finSupp ( 0g ‘ 𝐴 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) )
50 47 48 49 sylancl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) → ( 𝑀 finSupp ( 0g ‘ 𝐴 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) )
51 csbov12g ⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝑛 𝐸 𝑌 ) · ⦋ 𝑥 / 𝑛 ⦌ ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) )
52 csbov1g ⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( 𝑛 𝐸 𝑌 ) = ( ⦋ 𝑥 / 𝑛 ⦌ 𝑛 𝐸 𝑌 ) )
53 csbvarg ⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ 𝑛 = 𝑥 )
54 53 oveq1d ⊢ ( 𝑥 ∈ ℕ0 → ( ⦋ 𝑥 / 𝑛 ⦌ 𝑛 𝐸 𝑌 ) = ( 𝑥 𝐸 𝑌 ) )
55 52 54 eqtrd ⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( 𝑛 𝐸 𝑌 ) = ( 𝑥 𝐸 𝑌 ) )
56 csbfv2g ⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) = ( 𝑇 ‘ ⦋ 𝑥 / 𝑛 ⦌ ( 𝑀 ‘ 𝑛 ) ) )
57 csbfv2g ⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( 𝑀 ‘ 𝑛 ) = ( 𝑀 ‘ ⦋ 𝑥 / 𝑛 ⦌ 𝑛 ) )
58 53 fveq2d ⊢ ( 𝑥 ∈ ℕ0 → ( 𝑀 ‘ ⦋ 𝑥 / 𝑛 ⦌ 𝑛 ) = ( 𝑀 ‘ 𝑥 ) )
59 57 58 eqtrd ⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( 𝑀 ‘ 𝑛 ) = ( 𝑀 ‘ 𝑥 ) )
60 59 fveq2d ⊢ ( 𝑥 ∈ ℕ0 → ( 𝑇 ‘ ⦋ 𝑥 / 𝑛 ⦌ ( 𝑀 ‘ 𝑛 ) ) = ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) )
61 56 60 eqtrd ⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) = ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) )
62 55 61 oveq12d ⊢ ( 𝑥 ∈ ℕ0 → ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝑛 𝐸 𝑌 ) · ⦋ 𝑥 / 𝑛 ⦌ ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
63 51 62 eqtrd ⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
64 63 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
65 64 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
66 fveq2 ⊢ ( ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) → ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) = ( 𝑇 ‘ ( 0g ‘ 𝐴 ) ) )
67 66 oveq2d ⊢ ( ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) → ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) ) = ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 0g ‘ 𝐴 ) ) ) )
68 14 7 8 1 2 3 mat2pmatghm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )
69 16 68 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )
70 69 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )
71 ghmmhm ⊢ ( 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) → 𝑇 ∈ ( 𝐴 MndHom 𝐶 ) )
72 eqid ⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
73 72 15 mhm0 ⊢ ( 𝑇 ∈ ( 𝐴 MndHom 𝐶 ) → ( 𝑇 ‘ ( 0g ‘ 𝐴 ) ) = ( 0g ‘ 𝐶 ) )
74 70 71 73 3syl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑇 ‘ ( 0g ‘ 𝐴 ) ) = ( 0g ‘ 𝐶 ) )
75 74 oveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 0g ‘ 𝐴 ) ) ) = ( ( 𝑥 𝐸 𝑌 ) · ( 0g ‘ 𝐶 ) ) )
76 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
77 16 76 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
78 2 matlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝐶 ∈ LMod )
79 77 78 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐶 ∈ LMod )
80 79 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝐶 ∈ LMod )
81 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
82 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
83 81 82 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
84 77 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ Ring )
85 81 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
86 84 85 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
87 86 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
88 simpr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
89 16 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
90 12 1 82 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ ( Base ‘ 𝑃 ) )
91 89 90 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ ( Base ‘ 𝑃 ) )
92 91 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑌 ∈ ( Base ‘ 𝑃 ) )
93 83 11 87 88 92 mulgnn0cld ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 𝐸 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
94 1 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
95 2 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝐶 ) )
96 94 95 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝐶 ) )
97 96 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Scalar ‘ 𝐶 ) = 𝑃 )
98 97 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( Scalar ‘ 𝐶 ) = 𝑃 )
99 98 fveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ 𝑃 ) )
100 93 99 eleqtrrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 𝐸 𝑌 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
101 eqid ⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
102 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
103 101 13 102 15 lmodvs0 ⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑥 𝐸 𝑌 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ) → ( ( 𝑥 𝐸 𝑌 ) · ( 0g ‘ 𝐶 ) ) = ( 0g ‘ 𝐶 ) )
104 80 100 103 syl2anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 𝐸 𝑌 ) · ( 0g ‘ 𝐶 ) ) = ( 0g ‘ 𝐶 ) )
105 75 104 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 0g ‘ 𝐴 ) ) ) = ( 0g ‘ 𝐶 ) )
106 67 105 sylan9eqr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) ) = ( 0g ‘ 𝐶 ) )
107 65 106 eqtrd ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) )
108 107 ex ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) )
109 108 imim2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑦 < 𝑥 → ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑦 < 𝑥 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) ) )
110 109 ralimdva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) ) )
111 110 reximdva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) → ( ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) ) )
112 50 111 syld ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) → ( 𝑀 finSupp ( 0g ‘ 𝐴 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) ) )
113 112 impr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) )
114 45 46 113 mptnn0fsupp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) finSupp ( 0g ‘ 𝐶 ) )
115 3 15 21 27 29 35 44 114 gsummptmhm ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( 𝐼 ‘ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) ) ) = ( 𝐼 ‘ ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) ) ) )
116 simpll ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
117 1 2 3 4 5 6 7 8 9 10 11 12 13 14 monmat2matmon ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( ( 𝑀 ‘ 𝑛 ) ∈ 𝐾 ∧ 𝑛 ∈ ℕ0 ) ) → ( 𝐼 ‘ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) = ( ( 𝑀 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) )
118 116 41 42 117 syl12anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐼 ‘ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) = ( ( 𝑀 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) )
119 118 mpteq2dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝐼 ‘ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑀 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) )
120 119 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( 𝐼 ‘ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑀 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )
121 115 120 eqtr3d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝐼 ‘ ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑀 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )