Metamath Proof Explorer

Theorem cpmadugsumlemC

Description: Lemma C 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 cpmadugsumlemC ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )

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 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
12 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
13 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
14 3 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15 13 14 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
16 15 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
17 4 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝑌 ∈ Ring )
18 16 17 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ Ring )
19 18 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Ring )
20 19 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Ring )
21 ovexd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 ... 𝑠 ) ∈ V )
22 5 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
23 13 22 syl3an2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
24 23 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
25 16 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
26 4 matlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝑌 ∈ LMod )
27 25 26 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ LMod )
28 27 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑌 ∈ LMod )
29 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
30 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
31 29 30 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
32 15 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
33 29 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
34 32 33 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
35 34 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
36 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... 𝑠 ) → 𝑖 ∈ ℕ0 )
37 36 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑖 ∈ ℕ0 )
38 13 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
39 6 3 30 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
40 38 39 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
41 40 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
42 31 7 35 37 41 mulgnn0cld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
43 3 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
44 43 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
45 44 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
46 4 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
47 45 46 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
48 47 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝑌 ) = 𝑃 )
49 48 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
50 49 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
51 50 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
52 42 51 mpbird ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
53 simpll1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑁 ∈ Fin )
54 38 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑅 ∈ Ring )
55 simplrl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑠 ∈ ℕ0 )
56 simprr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) )
57 56 anim1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) )
58 1 2 3 4 5 m2pmfzmap ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
59 53 54 55 57 58 syl31anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
60 eqid ⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
61 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
62 11 60 8 61 lmodvscl ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
63 28 52 59 62 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
64 simpl1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑁 ∈ Fin )
65 38 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑅 ∈ Ring )
66 simprl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑠 ∈ ℕ0 )
67 eqid ⊢ ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) )
68 fzfid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 0 ... 𝑠 ) ∈ Fin )
69 ovexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ V )
70 fvexd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 0g ‘ 𝑌 ) ∈ V )
71 67 68 69 70 fsuppmptdm ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) finSupp ( 0g ‘ 𝑌 ) )
72 64 65 66 56 71 syl31anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) finSupp ( 0g ‘ 𝑌 ) )
73 11 12 9 20 21 24 63 72 gsummulc2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑇 ‘ 𝑀 ) × ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
74 4 matassa ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑌 ∈ AssAlg )
75 44 74 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ AssAlg )
76 75 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ AssAlg )
77 76 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑌 ∈ AssAlg )
78 15 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ Ring )
79 78 33 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
80 79 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
81 80 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
82 31 7 81 37 41 mulgnn0cld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
83 49 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
84 82 83 eleqtrrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
85 23 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
86 11 60 61 8 9 assaassr ⊢ ( ( 𝑌 ∈ AssAlg ∧ ( ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
87 77 84 85 59 86 syl13anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
88 87 mpteq2dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑇 ‘ 𝑀 ) × ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
89 88 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑇 ‘ 𝑀 ) × ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
90 73 89 eqtr3d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )