Metamath Proof Explorer


Theorem cpmadugsumlemB

Description: Lemma B for cpmadugsum . (Contributed by AV, 2-Nov-2019)

Ref Expression
Hypotheses cpmadugsum.a 𝐴 = ( 𝑁 Mat 𝑅 )
cpmadugsum.b 𝐵 = ( Base ‘ 𝐴 )
cpmadugsum.p 𝑃 = ( Poly1𝑅 )
cpmadugsum.y 𝑌 = ( 𝑁 Mat 𝑃 )
cpmadugsum.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
cpmadugsum.x 𝑋 = ( var1𝑅 )
cpmadugsum.e = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
cpmadugsum.m · = ( ·𝑠𝑌 )
cpmadugsum.r × = ( .r𝑌 )
cpmadugsum.1 1 = ( 1r𝑌 )
Assertion cpmadugsumlemB ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmadugsum.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 cpmadugsum.b 𝐵 = ( Base ‘ 𝐴 )
3 cpmadugsum.p 𝑃 = ( Poly1𝑅 )
4 cpmadugsum.y 𝑌 = ( 𝑁 Mat 𝑃 )
5 cpmadugsum.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
6 cpmadugsum.x 𝑋 = ( var1𝑅 )
7 cpmadugsum.e = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
8 cpmadugsum.m · = ( ·𝑠𝑌 )
9 cpmadugsum.r × = ( .r𝑌 )
10 cpmadugsum.1 1 = ( 1r𝑌 )
11 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
12 3 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
13 11 12 syl ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
14 13 3ad2ant2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑃 ∈ Ring )
15 eqid ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
16 15 ringmgp ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
17 14 16 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
18 17 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
19 elfznn0 ( 𝑖 ∈ ( 0 ... 𝑠 ) → 𝑖 ∈ ℕ0 )
20 19 adantl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑖 ∈ ℕ0 )
21 1nn0 1 ∈ ℕ0
22 21 a1i ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 1 ∈ ℕ0 )
23 11 3ad2ant2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑅 ∈ Ring )
24 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
25 6 3 24 vr1cl ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
26 23 25 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
27 26 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
28 15 24 mgpbas ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
29 eqid ( .r𝑃 ) = ( .r𝑃 )
30 15 29 mgpplusg ( .r𝑃 ) = ( +g ‘ ( mulGrp ‘ 𝑃 ) )
31 28 7 30 mulgnn0dir ( ( ( mulGrp ‘ 𝑃 ) ∈ Mnd ∧ ( 𝑖 ∈ ℕ0 ∧ 1 ∈ ℕ0𝑋 ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝑖 + 1 ) 𝑋 ) = ( ( 𝑖 𝑋 ) ( .r𝑃 ) ( 1 𝑋 ) ) )
32 18 20 22 27 31 syl13anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 + 1 ) 𝑋 ) = ( ( 𝑖 𝑋 ) ( .r𝑃 ) ( 1 𝑋 ) ) )
33 3 ply1crng ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
34 33 anim2i ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
35 34 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
36 4 matsca2 ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
37 35 36 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
38 37 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
39 38 fveq2d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( .r𝑃 ) = ( .r ‘ ( Scalar ‘ 𝑌 ) ) )
40 eqidd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 𝑋 ) = ( 𝑖 𝑋 ) )
41 28 7 mulg1 ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 1 𝑋 ) = 𝑋 )
42 26 41 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( 1 𝑋 ) = 𝑋 )
43 42 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 1 𝑋 ) = 𝑋 )
44 39 40 43 oveq123d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 𝑋 ) ( .r𝑃 ) ( 1 𝑋 ) ) = ( ( 𝑖 𝑋 ) ( .r ‘ ( Scalar ‘ 𝑌 ) ) 𝑋 ) )
45 32 44 eqtrd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 + 1 ) 𝑋 ) = ( ( 𝑖 𝑋 ) ( .r ‘ ( Scalar ‘ 𝑌 ) ) 𝑋 ) )
46 13 anim2i ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
47 46 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
48 4 matring ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝑌 ∈ Ring )
49 47 48 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑌 ∈ Ring )
50 49 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑌 ∈ Ring )
51 simpll1 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑁 ∈ Fin )
52 23 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑅 ∈ Ring )
53 simplrl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑠 ∈ ℕ0 )
54 simprr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) )
55 54 anim1i ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) )
56 1 2 3 4 5 m2pmfzmap ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) ) → ( 𝑇 ‘ ( 𝑏𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
57 51 52 53 55 56 syl31anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
58 eqid ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
59 58 9 10 ringlidm ( ( 𝑌 ∈ Ring ∧ ( 𝑇 ‘ ( 𝑏𝑖 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( 1 × ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) = ( 𝑇 ‘ ( 𝑏𝑖 ) ) )
60 50 57 59 syl2anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 1 × ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) = ( 𝑇 ‘ ( 𝑏𝑖 ) ) )
61 60 eqcomd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏𝑖 ) ) = ( 1 × ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) )
62 45 61 oveq12d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( ( 𝑖 + 1 ) 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) = ( ( ( 𝑖 𝑋 ) ( .r ‘ ( Scalar ‘ 𝑌 ) ) 𝑋 ) · ( 1 × ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) )
63 4 matassa ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑌 ∈ AssAlg )
64 34 63 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ AssAlg )
65 64 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑌 ∈ AssAlg )
66 65 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑌 ∈ AssAlg )
67 37 eqcomd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( Scalar ‘ 𝑌 ) = 𝑃 )
68 67 fveq2d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
69 26 68 eleqtrrd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
70 69 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
71 28 7 18 20 27 mulgnn0cld ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
72 68 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
73 71 72 eleqtrrd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
74 46 48 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ Ring )
75 74 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑌 ∈ Ring )
76 58 10 ringidcl ( 𝑌 ∈ Ring → 1 ∈ ( Base ‘ 𝑌 ) )
77 75 76 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 1 ∈ ( Base ‘ 𝑌 ) )
78 77 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 1 ∈ ( Base ‘ 𝑌 ) )
79 eqid ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
80 eqid ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
81 eqid ( .r ‘ ( Scalar ‘ 𝑌 ) ) = ( .r ‘ ( Scalar ‘ 𝑌 ) )
82 58 79 80 81 8 9 assa2ass ( ( 𝑌 ∈ AssAlg ∧ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ ( 𝑖 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ) ∧ ( 1 ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏𝑖 ) ) ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑋 · 1 ) × ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) = ( ( ( 𝑖 𝑋 ) ( .r ‘ ( Scalar ‘ 𝑌 ) ) 𝑋 ) · ( 1 × ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) )
83 66 70 73 78 57 82 syl122anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑋 · 1 ) × ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) = ( ( ( 𝑖 𝑋 ) ( .r ‘ ( Scalar ‘ 𝑌 ) ) 𝑋 ) · ( 1 × ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) )
84 83 eqcomd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( ( 𝑖 𝑋 ) ( .r ‘ ( Scalar ‘ 𝑌 ) ) 𝑋 ) · ( 1 × ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) = ( ( 𝑋 · 1 ) × ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) )
85 62 84 eqtrd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( ( 𝑖 + 1 ) 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) = ( ( 𝑋 · 1 ) × ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) )
86 85 mpteq2dva ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) = ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑋 · 1 ) × ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) ) )
87 86 oveq2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑋 · 1 ) × ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) ) ) )
88 eqid ( 0g𝑌 ) = ( 0g𝑌 )
89 75 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Ring )
90 ovexd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 0 ... 𝑠 ) ∈ V )
91 4 matlmod ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝑌 ∈ LMod )
92 46 91 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ LMod )
93 92 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑌 ∈ LMod )
94 11 adantl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
95 94 25 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
96 34 36 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
97 96 eqcomd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Scalar ‘ 𝑌 ) = 𝑃 )
98 97 fveq2d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
99 95 98 eleqtrrd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
100 99 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
101 49 76 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 1 ∈ ( Base ‘ 𝑌 ) )
102 58 79 8 80 lmodvscl ( ( 𝑌 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 1 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
103 93 100 101 102 syl3anc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
104 103 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
105 93 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑌 ∈ LMod )
106 36 eqcomd ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → ( Scalar ‘ 𝑌 ) = 𝑃 )
107 106 fveq2d ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
108 35 107 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
109 108 eleq2d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( ( 𝑖 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝑖 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
110 109 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝑖 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
111 71 110 mpbird ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
112 58 79 8 80 lmodvscl ( ( 𝑌 ∈ LMod ∧ ( 𝑖 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ ( 𝑇 ‘ ( 𝑏𝑖 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
113 105 111 57 112 syl3anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
114 simpl1 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝑁 ∈ Fin )
115 23 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝑅 ∈ Ring )
116 simprl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝑠 ∈ ℕ0 )
117 eqid ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) = ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) )
118 fzfid ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 0 ... 𝑠 ) ∈ Fin )
119 ovexd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ∈ V )
120 fvexd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 0g𝑌 ) ∈ V )
121 117 118 119 120 fsuppmptdm ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) finSupp ( 0g𝑌 ) )
122 114 115 116 54 121 syl31anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) finSupp ( 0g𝑌 ) )
123 58 88 9 89 90 104 113 122 gsummulc2 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑋 · 1 ) × ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) ) ) = ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) ) ) )
124 87 123 eqtr2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) ) )