Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cpmadugsumlemF Structured version   Visualization version   GIF version

 Description: Lemma F for cpmadugsum 21579. (Contributed by AV, 7-Nov-2019.)
Hypotheses
Ref Expression
cpmadugsum.a 𝐴 = (𝑁 Mat 𝑅)
cpmadugsum.y 𝑌 = (𝑁 Mat 𝑃)
cpmadugsum.t 𝑇 = (𝑁 matToPolyMat 𝑅)
Assertion
Ref Expression
cpmadugsumlemF (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
Distinct variable groups:   𝐵,𝑖   𝑖,𝑀   𝑖,𝑁   𝑅,𝑖   𝑖,𝑋   𝑖,𝑌   × ,𝑖   · ,𝑖   1 ,𝑖   𝑖,𝑏   𝑖,𝑠   𝑇,𝑖   ,𝑖   ,𝑖
Allowed substitution hints:   𝐴(𝑖,𝑠,𝑏)   𝐵(𝑠,𝑏)   𝑃(𝑖,𝑠,𝑏)   + (𝑖,𝑠,𝑏)   𝑅(𝑠,𝑏)   𝑇(𝑠,𝑏)   · (𝑠,𝑏)   × (𝑠,𝑏)   1 (𝑠,𝑏)   (𝑠,𝑏)   𝑀(𝑠,𝑏)   (𝑠,𝑏)   𝑁(𝑠,𝑏)   𝑋(𝑠,𝑏)   𝑌(𝑠,𝑏)

Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 nnnn0 11942 . . . 4 (𝑠 ∈ ℕ → 𝑠 ∈ ℕ0)
2 cpmadugsum.a . . . . 5 𝐴 = (𝑁 Mat 𝑅)
3 cpmadugsum.b . . . . 5 𝐵 = (Base‘𝐴)
4 cpmadugsum.p . . . . 5 𝑃 = (Poly1𝑅)
5 cpmadugsum.y . . . . 5 𝑌 = (𝑁 Mat 𝑃)
6 cpmadugsum.t . . . . 5 𝑇 = (𝑁 matToPolyMat 𝑅)
7 cpmadugsum.x . . . . 5 𝑋 = (var1𝑅)
8 cpmadugsum.e . . . . 5 = (.g‘(mulGrp‘𝑃))
9 cpmadugsum.m . . . . 5 · = ( ·𝑠𝑌)
10 cpmadugsum.r . . . . 5 × = (.r𝑌)
11 cpmadugsum.1 . . . . 5 1 = (1r𝑌)
122, 3, 4, 5, 6, 7, 8, 9, 10, 11cpmadugsumlemB 21575 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ0𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))))
131, 12sylanr1 682 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))))
142, 3, 4, 5, 6, 7, 8, 9, 10, 11cpmadugsumlemC 21576 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ0𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))
151, 14sylanr1 682 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))
1613, 15oveq12d 7169 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
17 nncn 11683 . . . . . . . . 9 (𝑠 ∈ ℕ → 𝑠 ∈ ℂ)
18 npcan1 11104 . . . . . . . . . 10 (𝑠 ∈ ℂ → ((𝑠 − 1) + 1) = 𝑠)
1918eqcomd 2765 . . . . . . . . 9 (𝑠 ∈ ℂ → 𝑠 = ((𝑠 − 1) + 1))
2017, 19syl 17 . . . . . . . 8 (𝑠 ∈ ℕ → 𝑠 = ((𝑠 − 1) + 1))
2120oveq2d 7167 . . . . . . 7 (𝑠 ∈ ℕ → (0...𝑠) = (0...((𝑠 − 1) + 1)))
2221mpteq1d 5122 . . . . . 6 (𝑠 ∈ ℕ → (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))) = (𝑖 ∈ (0...((𝑠 − 1) + 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))
2322oveq2d 7167 . . . . 5 (𝑠 ∈ ℕ → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = (𝑌 Σg (𝑖 ∈ (0...((𝑠 − 1) + 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))))
2423ad2antrl 728 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = (𝑌 Σg (𝑖 ∈ (0...((𝑠 − 1) + 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))))
25 eqid 2759 . . . . 5 (Base‘𝑌) = (Base‘𝑌)
26 cpmadugsum.g . . . . 5 + = (+g𝑌)
27 crngring 19378 . . . . . . . . . 10 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
2827anim2i 620 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
29283adant3 1130 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
304, 5pmatring 21393 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
3129, 30syl 17 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Ring)
32 ringcmn 19403 . . . . . . 7 (𝑌 ∈ Ring → 𝑌 ∈ CMnd)
3331, 32syl 17 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ CMnd)
3433adantr 485 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ CMnd)
35 nnm1nn0 11976 . . . . . 6 (𝑠 ∈ ℕ → (𝑠 − 1) ∈ ℕ0)
3635ad2antrl 728 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑠 − 1) ∈ ℕ0)
37 simpll1 1210 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → 𝑁 ∈ Fin)
38273ad2ant2 1132 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑅 ∈ Ring)
3938adantr 485 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑅 ∈ Ring)
4039adantr 485 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → 𝑅 ∈ Ring)
41 elmapi 8439 . . . . . . . . . 10 (𝑏 ∈ (𝐵m (0...𝑠)) → 𝑏:(0...𝑠)⟶𝐵)
4221feq2d 6485 . . . . . . . . . 10 (𝑠 ∈ ℕ → (𝑏:(0...𝑠)⟶𝐵𝑏:(0...((𝑠 − 1) + 1))⟶𝐵))
4341, 42syl5ibcom 248 . . . . . . . . 9 (𝑏 ∈ (𝐵m (0...𝑠)) → (𝑠 ∈ ℕ → 𝑏:(0...((𝑠 − 1) + 1))⟶𝐵))
4443impcom 412 . . . . . . . 8 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑏:(0...((𝑠 − 1) + 1))⟶𝐵)
4544adantl 486 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑏:(0...((𝑠 − 1) + 1))⟶𝐵)
4645ffvelrnda 6843 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → (𝑏𝑖) ∈ 𝐵)
47 elfznn0 13050 . . . . . . . 8 (𝑖 ∈ (0...((𝑠 − 1) + 1)) → 𝑖 ∈ ℕ0)
4847adantl 486 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → 𝑖 ∈ ℕ0)
49 1nn0 11951 . . . . . . . 8 1 ∈ ℕ0
5049a1i 11 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → 1 ∈ ℕ0)
5148, 50nn0addcld 11999 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → (𝑖 + 1) ∈ ℕ0)
522, 3, 6, 4, 5, 25, 9, 8, 7mat2pmatscmxcl 21441 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑏𝑖) ∈ 𝐵 ∧ (𝑖 + 1) ∈ ℕ0)) → (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
5337, 40, 46, 51, 52syl22anc 838 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
5425, 26, 34, 36, 53gsummptfzsplit 19121 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...((𝑠 − 1) + 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (𝑌 Σg (𝑖 ∈ {((𝑠 − 1) + 1)} ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))))
55 ringmnd 19376 . . . . . . . 8 (𝑌 ∈ Ring → 𝑌 ∈ Mnd)
5631, 55syl 17 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Mnd)
5756adantr 485 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ Mnd)
58 ovexd 7186 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑠 − 1) + 1) ∈ V)
59 simpl1 1189 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑁 ∈ Fin)
60 nn0fz0 13055 . . . . . . . . . . 11 (𝑠 ∈ ℕ0𝑠 ∈ (0...𝑠))
611, 60sylib 221 . . . . . . . . . 10 (𝑠 ∈ ℕ → 𝑠 ∈ (0...𝑠))
62 ffvelrn 6841 . . . . . . . . . 10 ((𝑏:(0...𝑠)⟶𝐵𝑠 ∈ (0...𝑠)) → (𝑏𝑠) ∈ 𝐵)
6341, 61, 62syl2anr 600 . . . . . . . . 9 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑏𝑠) ∈ 𝐵)
641adantr 485 . . . . . . . . . 10 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑠 ∈ ℕ0)
6549a1i 11 . . . . . . . . . 10 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 1 ∈ ℕ0)
6664, 65nn0addcld 11999 . . . . . . . . 9 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑠 + 1) ∈ ℕ0)
6763, 66jca 516 . . . . . . . 8 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → ((𝑏𝑠) ∈ 𝐵 ∧ (𝑠 + 1) ∈ ℕ0))
6867adantl 486 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑏𝑠) ∈ 𝐵 ∧ (𝑠 + 1) ∈ ℕ0))
692, 3, 6, 4, 5, 25, 9, 8, 7mat2pmatscmxcl 21441 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑏𝑠) ∈ 𝐵 ∧ (𝑠 + 1) ∈ ℕ0)) → (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌))
7059, 39, 68, 69syl21anc 837 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌))
71 oveq1 7158 . . . . . . . . 9 (𝑖 = ((𝑠 − 1) + 1) → (𝑖 + 1) = (((𝑠 − 1) + 1) + 1))
7271oveq1d 7166 . . . . . . . 8 (𝑖 = ((𝑠 − 1) + 1) → ((𝑖 + 1) 𝑋) = ((((𝑠 − 1) + 1) + 1) 𝑋))
73 2fveq3 6664 . . . . . . . 8 (𝑖 = ((𝑠 − 1) + 1) → (𝑇‘(𝑏𝑖)) = (𝑇‘(𝑏‘((𝑠 − 1) + 1))))
7472, 73oveq12d 7169 . . . . . . 7 (𝑖 = ((𝑠 − 1) + 1) → (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) = (((((𝑠 − 1) + 1) + 1) 𝑋) · (𝑇‘(𝑏‘((𝑠 − 1) + 1)))))
7517, 18syl 17 . . . . . . . . . . 11 (𝑠 ∈ ℕ → ((𝑠 − 1) + 1) = 𝑠)
7675oveq1d 7166 . . . . . . . . . 10 (𝑠 ∈ ℕ → (((𝑠 − 1) + 1) + 1) = (𝑠 + 1))
7776oveq1d 7166 . . . . . . . . 9 (𝑠 ∈ ℕ → ((((𝑠 − 1) + 1) + 1) 𝑋) = ((𝑠 + 1) 𝑋))
7875fveq2d 6663 . . . . . . . . . 10 (𝑠 ∈ ℕ → (𝑏‘((𝑠 − 1) + 1)) = (𝑏𝑠))
7978fveq2d 6663 . . . . . . . . 9 (𝑠 ∈ ℕ → (𝑇‘(𝑏‘((𝑠 − 1) + 1))) = (𝑇‘(𝑏𝑠)))
8077, 79oveq12d 7169 . . . . . . . 8 (𝑠 ∈ ℕ → (((((𝑠 − 1) + 1) + 1) 𝑋) · (𝑇‘(𝑏‘((𝑠 − 1) + 1)))) = (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))))
8180ad2antrl 728 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((((𝑠 − 1) + 1) + 1) 𝑋) · (𝑇‘(𝑏‘((𝑠 − 1) + 1)))) = (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))))
8274, 81sylan9eqr 2816 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 = ((𝑠 − 1) + 1)) → (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) = (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))))
8325, 57, 58, 70, 82gsumsnd 19141 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {((𝑠 − 1) + 1)} ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))))
8483oveq2d 7167 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (𝑌 Σg (𝑖 ∈ {((𝑠 − 1) + 1)} ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))))
8524, 54, 843eqtrd 2798 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))))
861ad2antrl 728 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑠 ∈ ℕ0)
874, 5pmatlmod 21394 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ LMod)
8828, 87syl 17 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ LMod)
89883adant3 1130 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ LMod)
9089adantr 485 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ LMod)
9190adantr 485 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑌 ∈ LMod)
924ply1ring 20973 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
9327, 92syl 17 . . . . . . . . . . . 12 (𝑅 ∈ CRing → 𝑃 ∈ Ring)
94933ad2ant2 1132 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑃 ∈ Ring)
95 eqid 2759 . . . . . . . . . . . 12 (mulGrp‘𝑃) = (mulGrp‘𝑃)
9695ringmgp 19372 . . . . . . . . . . 11 (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
9794, 96syl 17 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (mulGrp‘𝑃) ∈ Mnd)
9897adantr 485 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (mulGrp‘𝑃) ∈ Mnd)
9998adantr 485 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (mulGrp‘𝑃) ∈ Mnd)
100 elfznn0 13050 . . . . . . . . 9 (𝑖 ∈ (0...𝑠) → 𝑖 ∈ ℕ0)
101100adantl 486 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑖 ∈ ℕ0)
102 eqid 2759 . . . . . . . . . . . . 13 (Base‘𝑃) = (Base‘𝑃)
1037, 4, 102vr1cl 20942 . . . . . . . . . . . 12 (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
10427, 103syl 17 . . . . . . . . . . 11 (𝑅 ∈ CRing → 𝑋 ∈ (Base‘𝑃))
1051043ad2ant2 1132 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑋 ∈ (Base‘𝑃))
106105adantr 485 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑋 ∈ (Base‘𝑃))
107106adantr 485 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑋 ∈ (Base‘𝑃))
10895, 102mgpbas 19314 . . . . . . . . 9 (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
109108, 8mulgnn0cl 18312 . . . . . . . 8 (((mulGrp‘𝑃) ∈ Mnd ∧ 𝑖 ∈ ℕ0𝑋 ∈ (Base‘𝑃)) → (𝑖 𝑋) ∈ (Base‘𝑃))
11099, 101, 107, 109syl3anc 1369 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑖 𝑋) ∈ (Base‘𝑃))
1114ply1crng 20923 . . . . . . . . . . . . . . 15 (𝑅 ∈ CRing → 𝑃 ∈ CRing)
112111anim2i 620 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing))
1131123adant3 1130 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing))
1145matsca2 21121 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝑌))
115113, 114syl 17 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑃 = (Scalar‘𝑌))
116115eqcomd 2765 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (Scalar‘𝑌) = 𝑃)
117116fveq2d 6663 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (Base‘(Scalar‘𝑌)) = (Base‘𝑃))
118117eleq2d 2838 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ((𝑖 𝑋) ∈ (Base‘(Scalar‘𝑌)) ↔ (𝑖 𝑋) ∈ (Base‘𝑃)))
119118adantr 485 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑖 𝑋) ∈ (Base‘(Scalar‘𝑌)) ↔ (𝑖 𝑋) ∈ (Base‘𝑃)))
120119adantr 485 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑖 𝑋) ∈ (Base‘(Scalar‘𝑌)) ↔ (𝑖 𝑋) ∈ (Base‘𝑃)))
121110, 120mpbird 260 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑖 𝑋) ∈ (Base‘(Scalar‘𝑌)))
12231adantr 485 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ Ring)
123122adantr 485 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑌 ∈ Ring)
124 simpll1 1210 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑁 ∈ Fin)
12539adantr 485 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑅 ∈ Ring)
126 simpll3 1212 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑀𝐵)
1276, 2, 3, 4, 5mat2pmatbas 21427 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
128124, 125, 126, 127syl3anc 1369 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑇𝑀) ∈ (Base‘𝑌))
12986adantr 485 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑠 ∈ ℕ0)
130 simprr 773 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑏 ∈ (𝐵m (0...𝑠)))
131130anim1i 618 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑏 ∈ (𝐵m (0...𝑠)) ∧ 𝑖 ∈ (0...𝑠)))
1322, 3, 4, 5, 6m2pmfzmap 21448 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0) ∧ (𝑏 ∈ (𝐵m (0...𝑠)) ∧ 𝑖 ∈ (0...𝑠))) → (𝑇‘(𝑏𝑖)) ∈ (Base‘𝑌))
133124, 125, 129, 131, 132syl31anc 1371 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑇‘(𝑏𝑖)) ∈ (Base‘𝑌))
13425, 10ringcl 19383 . . . . . . 7 ((𝑌 ∈ Ring ∧ (𝑇𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏𝑖)) ∈ (Base‘𝑌)) → ((𝑇𝑀) × (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
135123, 128, 133, 134syl3anc 1369 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑇𝑀) × (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
136 eqid 2759 . . . . . . 7 (Scalar‘𝑌) = (Scalar‘𝑌)
137 eqid 2759 . . . . . . 7 (Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌))
13825, 136, 9, 137lmodvscl 19720 . . . . . 6 ((𝑌 ∈ LMod ∧ (𝑖 𝑋) ∈ (Base‘(Scalar‘𝑌)) ∧ ((𝑇𝑀) × (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌)) → ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) ∈ (Base‘𝑌))
13991, 121, 135, 138syl3anc 1369 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) ∈ (Base‘𝑌))
14025, 26, 34, 86, 139gsummptfzsplitl 19122 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
141 0nn0 11950 . . . . . . . 8 0 ∈ ℕ0
142141a1i 11 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 0 ∈ ℕ0)
143 eqid 2759 . . . . . . . . . . . . 13 (0g‘(mulGrp‘𝑃)) = (0g‘(mulGrp‘𝑃))
144108, 143, 8mulg0 18299 . . . . . . . . . . . 12 (𝑋 ∈ (Base‘𝑃) → (0 𝑋) = (0g‘(mulGrp‘𝑃)))
145105, 144syl 17 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (0 𝑋) = (0g‘(mulGrp‘𝑃)))
146145adantr 485 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (0 𝑋) = (0g‘(mulGrp‘𝑃)))
147146oveq1d 7166 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((0g‘(mulGrp‘𝑃)) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
148 eqid 2759 . . . . . . . . . . . . 13 (1r𝑃) = (1r𝑃)
14995, 148ringidval 19322 . . . . . . . . . . . 12 (1r𝑃) = (0g‘(mulGrp‘𝑃))
150149a1i 11 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (1r𝑃) = (0g‘(mulGrp‘𝑃)))
151150eqcomd 2765 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (0g‘(mulGrp‘𝑃)) = (1r𝑃))
152151oveq1d 7166 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0g‘(mulGrp‘𝑃)) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((1r𝑃) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
153115adantr 485 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑃 = (Scalar‘𝑌))
154153fveq2d 6663 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (1r𝑃) = (1r‘(Scalar‘𝑌)))
155154oveq1d 7166 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((1r𝑃) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((1r‘(Scalar‘𝑌)) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
15627, 127syl3an2 1162 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
157156adantr 485 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑇𝑀) ∈ (Base‘𝑌))
158 simpl 487 . . . . . . . . . . . . . . . . . 18 ((𝑏:(0...𝑠)⟶𝐵𝑠 ∈ ℕ) → 𝑏:(0...𝑠)⟶𝐵)
159 elnn0uz 12324 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ℕ0𝑠 ∈ (ℤ‘0))
1601, 159sylib 221 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ℕ → 𝑠 ∈ (ℤ‘0))
161 eluzfz1 12964 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (ℤ‘0) → 0 ∈ (0...𝑠))
162160, 161syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ℕ → 0 ∈ (0...𝑠))
163162adantl 486 . . . . . . . . . . . . . . . . . 18 ((𝑏:(0...𝑠)⟶𝐵𝑠 ∈ ℕ) → 0 ∈ (0...𝑠))
164158, 163ffvelrnd 6844 . . . . . . . . . . . . . . . . 17 ((𝑏:(0...𝑠)⟶𝐵𝑠 ∈ ℕ) → (𝑏‘0) ∈ 𝐵)
165164ex 417 . . . . . . . . . . . . . . . 16 (𝑏:(0...𝑠)⟶𝐵 → (𝑠 ∈ ℕ → (𝑏‘0) ∈ 𝐵))
16641, 165syl 17 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝐵m (0...𝑠)) → (𝑠 ∈ ℕ → (𝑏‘0) ∈ 𝐵))
167166impcom 412 . . . . . . . . . . . . . 14 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑏‘0) ∈ 𝐵)
168167adantl 486 . . . . . . . . . . . . 13 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑏‘0) ∈ 𝐵)
1696, 2, 3, 4, 5mat2pmatbas 21427 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌))
17059, 39, 168, 169syl3anc 1369 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌))
17125, 10ringcl 19383 . . . . . . . . . . . 12 ((𝑌 ∈ Ring ∧ (𝑇𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) → ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))
172122, 157, 170, 171syl3anc 1369 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))
173 eqid 2759 . . . . . . . . . . . 12 (1r‘(Scalar‘𝑌)) = (1r‘(Scalar‘𝑌))
17425, 136, 9, 173lmodvs1 19731 . . . . . . . . . . 11 ((𝑌 ∈ LMod ∧ ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) → ((1r‘(Scalar‘𝑌)) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑇𝑀) × (𝑇‘(𝑏‘0))))
17590, 172, 174syl2anc 588 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((1r‘(Scalar‘𝑌)) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑇𝑀) × (𝑇‘(𝑏‘0))))
176155, 175eqtrd 2794 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((1r𝑃) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑇𝑀) × (𝑇‘(𝑏‘0))))
177147, 152, 1763eqtrd 2798 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑇𝑀) × (𝑇‘(𝑏‘0))))
178177, 172eqeltrd 2853 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) ∈ (Base‘𝑌))
179 oveq1 7158 . . . . . . . . 9 (𝑖 = 0 → (𝑖 𝑋) = (0 𝑋))
180 2fveq3 6664 . . . . . . . . . 10 (𝑖 = 0 → (𝑇‘(𝑏𝑖)) = (𝑇‘(𝑏‘0)))
181180oveq2d 7167 . . . . . . . . 9 (𝑖 = 0 → ((𝑇𝑀) × (𝑇‘(𝑏𝑖))) = ((𝑇𝑀) × (𝑇‘(𝑏‘0))))
182179, 181oveq12d 7169 . . . . . . . 8 (𝑖 = 0 → ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) = ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
183182adantl 486 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 = 0) → ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) = ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
18425, 57, 142, 178, 183gsumsnd 19141 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) = ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
185108, 149, 8mulg0 18299 . . . . . . . . 9 (𝑋 ∈ (Base‘𝑃) → (0 𝑋) = (1r𝑃))
186105, 185syl 17 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (0 𝑋) = (1r𝑃))
187186adantr 485 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (0 𝑋) = (1r𝑃))
188187oveq1d 7166 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((1r𝑃) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
189184, 188, 1763eqtrd 2798 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) = ((𝑇𝑀) × (𝑇‘(𝑏‘0))))
190189oveq2d 7167 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
191140, 190eqtrd 2794 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
19285, 191oveq12d 7169 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = (((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
193 fzfid 13391 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (0...(𝑠 − 1)) ∈ Fin)
194 simpll1 1210 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → 𝑁 ∈ Fin)
19539adantr 485 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → 𝑅 ∈ Ring)
19641adantl 486 . . . . . . . . . . 11 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑏:(0...𝑠)⟶𝐵)
197196adantr 485 . . . . . . . . . 10 (((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → 𝑏:(0...𝑠)⟶𝐵)
198 nnz 12044 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ℕ → 𝑠 ∈ ℤ)
199 fzoval 13089 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ℤ → (0..^𝑠) = (0...(𝑠 − 1)))
200198, 199syl 17 . . . . . . . . . . . . . . 15 (𝑠 ∈ ℕ → (0..^𝑠) = (0...(𝑠 − 1)))
201200eqcomd 2765 . . . . . . . . . . . . . 14 (𝑠 ∈ ℕ → (0...(𝑠 − 1)) = (0..^𝑠))
202201eleq2d 2838 . . . . . . . . . . . . 13 (𝑠 ∈ ℕ → (𝑖 ∈ (0...(𝑠 − 1)) ↔ 𝑖 ∈ (0..^𝑠)))
203 elfzofz 13103 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑠) → 𝑖 ∈ (0...𝑠))
204202, 203syl6bi 256 . . . . . . . . . . . 12 (𝑠 ∈ ℕ → (𝑖 ∈ (0...(𝑠 − 1)) → 𝑖 ∈ (0...𝑠)))
205204adantr 485 . . . . . . . . . . 11 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑖 ∈ (0...(𝑠 − 1)) → 𝑖 ∈ (0...𝑠)))
206205imp 411 . . . . . . . . . 10 (((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → 𝑖 ∈ (0...𝑠))
207197, 206ffvelrnd 6844 . . . . . . . . 9 (((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → (𝑏𝑖) ∈ 𝐵)
208207adantll 714 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → (𝑏𝑖) ∈ 𝐵)
209 elfznn0 13050 . . . . . . . . . 10 (𝑖 ∈ (0...(𝑠 − 1)) → 𝑖 ∈ ℕ0)
210209adantl 486 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → 𝑖 ∈ ℕ0)
21149a1i 11 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → 1 ∈ ℕ0)
212210, 211nn0addcld 11999 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → (𝑖 + 1) ∈ ℕ0)
213194, 195, 208, 212, 52syl22anc 838 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
214213ralrimiva 3114 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ∀𝑖 ∈ (0...(𝑠 − 1))(((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
21525, 34, 193, 214gsummptcl 19156 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌))
21625, 26cmncom 18991 . . . . 5 ((𝑌 ∈ CMnd ∧ (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌) ∧ (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌)) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) = ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))))
21734, 215, 70, 216syl3anc 1369 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) = ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))))
218217oveq1d 7166 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) = (((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
219 ringgrp 19371 . . . . . . . . 9 (𝑌 ∈ Ring → 𝑌 ∈ Grp)
22031, 219syl 17 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Grp)
221220adantr 485 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ Grp)
222 fzfid 13391 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (1...𝑠) ∈ Fin)
22390adantr 485 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑌 ∈ LMod)
22498adantr 485 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (mulGrp‘𝑃) ∈ Mnd)
225 elfznn 12986 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℕ)
226225nnnn0d 11995 . . . . . . . . . . . . 13 (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℕ0)
227226adantl 486 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 ∈ ℕ0)
228106adantr 485 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑋 ∈ (Base‘𝑃))
229224, 227, 228, 109syl3anc 1369 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑖 𝑋) ∈ (Base‘𝑃))
230115fveq2d 6663 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (Base‘𝑃) = (Base‘(Scalar‘𝑌)))
231230adantr 485 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (Base‘𝑃) = (Base‘(Scalar‘𝑌)))
232231adantr 485 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (Base‘𝑃) = (Base‘(Scalar‘𝑌)))
233229, 232eleqtrd 2855 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑖 𝑋) ∈ (Base‘(Scalar‘𝑌)))
234122adantr 485 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑌 ∈ Ring)
235157adantr 485 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑇𝑀) ∈ (Base‘𝑌))
236 simpll1 1210 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑁 ∈ Fin)
23739adantr 485 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑅 ∈ Ring)
238196adantl 486 . . . . . . . . . . . . . 14 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑏:(0...𝑠)⟶𝐵)
239238adantr 485 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑏:(0...𝑠)⟶𝐵)
240 1eluzge0 12333 . . . . . . . . . . . . . . . . 17 1 ∈ (ℤ‘0)
241 fzss1 12996 . . . . . . . . . . . . . . . . 17 (1 ∈ (ℤ‘0) → (1...𝑠) ⊆ (0...𝑠))
242240, 241mp1i 13 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ℕ → (1...𝑠) ⊆ (0...𝑠))
243242sseld 3892 . . . . . . . . . . . . . . 15 (𝑠 ∈ ℕ → (𝑖 ∈ (1...𝑠) → 𝑖 ∈ (0...𝑠)))
244243ad2antrl 728 . . . . . . . . . . . . . 14 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑖 ∈ (1...𝑠) → 𝑖 ∈ (0...𝑠)))
245244imp 411 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 ∈ (0...𝑠))
246239, 245ffvelrnd 6844 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑏𝑖) ∈ 𝐵)
2476, 2, 3, 4, 5mat2pmatbas 21427 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏𝑖) ∈ 𝐵) → (𝑇‘(𝑏𝑖)) ∈ (Base‘𝑌))
248236, 237, 246, 247syl3anc 1369 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑇‘(𝑏𝑖)) ∈ (Base‘𝑌))
249234, 235, 248, 134syl3anc 1369 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑇𝑀) × (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
250223, 233, 249, 138syl3anc 1369 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) ∈ (Base‘𝑌))
251250ralrimiva 3114 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ∀𝑖 ∈ (1...𝑠)((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) ∈ (Base‘𝑌))
25225, 34, 222, 251gsummptcl 19156 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) ∈ (Base‘𝑌))
253 cpmadugsum.s . . . . . . . 8 = (-g𝑌)
25425, 26, 253grpaddsubass 18257 . . . . . . 7 ((𝑌 ∈ Grp ∧ ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌) ∧ (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌) ∧ (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) ∈ (Base‘𝑌))) → (((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))))
255221, 70, 215, 252, 254syl13anc 1370 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))))
256 oveq1 7158 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑖 → (𝑥 − 1) = (𝑖 − 1))
257256oveq1d 7166 . . . . . . . . . . . . . . 15 (𝑥 = 𝑖 → ((𝑥 − 1) + 1) = ((𝑖 − 1) + 1))
258257oveq1d 7166 . . . . . . . . . . . . . 14 (𝑥 = 𝑖 → (((𝑥 − 1) + 1) 𝑋) = (((𝑖 − 1) + 1) 𝑋))
259256fveq2d 6663 . . . . . . . . . . . . . . 15 (𝑥 = 𝑖 → (𝑏‘(𝑥 − 1)) = (𝑏‘(𝑖 − 1)))
260259fveq2d 6663 . . . . . . . . . . . . . 14 (𝑥 = 𝑖 → (𝑇‘(𝑏‘(𝑥 − 1))) = (𝑇‘(𝑏‘(𝑖 − 1))))
261258, 260oveq12d 7169 . . . . . . . . . . . . 13 (𝑥 = 𝑖 → ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))) = ((((𝑖 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))
262261cbvmptv 5136 . . . . . . . . . . . 12 (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1))))) = (𝑖 ∈ (1...𝑠) ↦ ((((𝑖 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))
263225nncnd 11691 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℂ)
264263adantl 486 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 ∈ ℂ)
265 npcan1 11104 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℂ → ((𝑖 − 1) + 1) = 𝑖)
266264, 265syl 17 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 − 1) + 1) = 𝑖)
267266oveq1d 7166 . . . . . . . . . . . . . 14 ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → (((𝑖 − 1) + 1) 𝑋) = (𝑖 𝑋))
268267oveq1d 7166 . . . . . . . . . . . . 13 ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → ((((𝑖 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) = ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))
269268mpteq2dva 5128 . . . . . . . . . . . 12 (𝑠 ∈ ℕ → (𝑖 ∈ (1...𝑠) ↦ ((((𝑖 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1))))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1))))))
270262, 269syl5eq 2806 . . . . . . . . . . 11 (𝑠 ∈ ℕ → (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1))))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1))))))
271270oveq2d 7167 . . . . . . . . . 10 (𝑠 ∈ ℕ → (𝑌 Σg (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))))
272271ad2antrl 728 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))))
273272oveq1d 7166 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
274 eqid 2759 . . . . . . . . . . 11 (0g𝑌) = (0g𝑌)
275 1zzd 12053 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 1 ∈ ℤ)
276 0zd 12033 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 0 ∈ ℤ)
27736nn0zd 12125 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑠 − 1) ∈ ℤ)
278 oveq1 7158 . . . . . . . . . . . . 13 (𝑖 = (𝑥 − 1) → (𝑖 + 1) = ((𝑥 − 1) + 1))
279278oveq1d 7166 . . . . . . . . . . . 12 (𝑖 = (𝑥 − 1) → ((𝑖 + 1) 𝑋) = (((𝑥 − 1) + 1) 𝑋))
280 2fveq3 6664 . . . . . . . . . . . 12 (𝑖 = (𝑥 − 1) → (𝑇‘(𝑏𝑖)) = (𝑇‘(𝑏‘(𝑥 − 1))))
281279, 280oveq12d 7169 . . . . . . . . . . 11 (𝑖 = (𝑥 − 1) → (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) = ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))
28225, 274, 34, 275, 276, 277, 213, 281gsummptshft 19125 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = (𝑌 Σg (𝑥 ∈ ((0 + 1)...((𝑠 − 1) + 1)) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))))
283 0p1e1 11797 . . . . . . . . . . . . . 14 (0 + 1) = 1
284283a1i 11 . . . . . . . . . . . . 13 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (0 + 1) = 1)
28575ad2antrl 728 . . . . . . . . . . . . 13 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑠 − 1) + 1) = 𝑠)
286284, 285oveq12d 7169 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0 + 1)...((𝑠 − 1) + 1)) = (1...𝑠))
287286mpteq1d 5122 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑥 ∈ ((0 + 1)...((𝑠 − 1) + 1)) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1))))) = (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1))))))
288287oveq2d 7167 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑥 ∈ ((0 + 1)...((𝑠 − 1) + 1)) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))) = (𝑌 Σg (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))))
289282, 288eqtrd 2794 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = (𝑌 Σg (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))))
290289oveq1d 7166 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
291 ringabl 19402 . . . . . . . . . . 11 (𝑌 ∈ Ring → 𝑌 ∈ Abel)
29231, 291syl 17 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Abel)
293292adantr 485 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ Abel)
294225adantl 486 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 ∈ ℕ)
295 nnz 12044 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
296 elfzm1b 13035 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑖 ∈ (1...𝑠) ↔ (𝑖 − 1) ∈ (0...(𝑠 − 1))))
297295, 198, 296syl2an 599 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑖 ∈ (1...𝑠) ↔ (𝑖 − 1) ∈ (0...(𝑠 − 1))))
298200adantl 486 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (0..^𝑠) = (0...(𝑠 − 1)))
299298eqcomd 2765 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (0...(𝑠 − 1)) = (0..^𝑠))
300299eleq2d 2838 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ) → ((𝑖 − 1) ∈ (0...(𝑠 − 1)) ↔ (𝑖 − 1) ∈ (0..^𝑠)))
301 elfzofz 13103 . . . . . . . . . . . . . . . . . 18 ((𝑖 − 1) ∈ (0..^𝑠) → (𝑖 − 1) ∈ (0...𝑠))
302300, 301syl6bi 256 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ) → ((𝑖 − 1) ∈ (0...(𝑠 − 1)) → (𝑖 − 1) ∈ (0...𝑠)))
303297, 302sylbid 243 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑖 ∈ (1...𝑠) → (𝑖 − 1) ∈ (0...𝑠)))
304303expimpd 458 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → (𝑖 − 1) ∈ (0...𝑠)))
305294, 304mpcom 38 . . . . . . . . . . . . . 14 ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → (𝑖 − 1) ∈ (0...𝑠))
306305ex 417 . . . . . . . . . . . . 13 (𝑠 ∈ ℕ → (𝑖 ∈ (1...𝑠) → (𝑖 − 1) ∈ (0...𝑠)))
307306ad2antrl 728 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑖 ∈ (1...𝑠) → (𝑖 − 1) ∈ (0...𝑠)))
308307imp 411 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑖 − 1) ∈ (0...𝑠))
309239, 308ffvelrnd 6844 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑏‘(𝑖 − 1)) ∈ 𝐵)
3102, 3, 6, 4, 5, 25, 9, 8, 7mat2pmatscmxcl 21441 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑏‘(𝑖 − 1)) ∈ 𝐵𝑖 ∈ ℕ0)) → ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ∈ (Base‘𝑌))
311236, 237, 309, 227, 310syl22anc 838 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ∈ (Base‘𝑌))
312 eqid 2759 . . . . . . . . 9 (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1))))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))
313 eqid 2759 . . . . . . . . 9 (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
31425, 253, 293, 222, 311, 250, 312, 313gsummptfidmsub 19139 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
315273, 290, 3143eqtr4d 2804 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
316315oveq2d 7167 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))) = ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))))
317221adantr 485 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑌 ∈ Grp)
31825, 253grpsubcl 18247 . . . . . . . . . 10 ((𝑌 ∈ Grp ∧ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ∈ (Base‘𝑌) ∧ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) ∈ (Base‘𝑌)) → (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌))
319317, 311, 250, 318syl3anc 1369 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌))
320319ralrimiva 3114 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ∀𝑖 ∈ (1...𝑠)(((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌))
32125, 34, 222, 320gsummptcl 19156 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) ∈ (Base‘𝑌))
32225, 26cmncom 18991 . . . . . . 7 ((𝑌 ∈ CMnd ∧ (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌) ∧ (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) ∈ (Base‘𝑌)) → ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))))
32334, 70, 321, 322syl3anc 1369 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))))
324255, 316, 3233eqtrd 2798 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))))
325324oveq1d 7166 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
32625, 26mndcl 17986 . . . . . 6 ((𝑌 ∈ Mnd ∧ (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌) ∧ (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌)) → ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) ∈ (Base‘𝑌))
32757, 70, 215, 326syl3anc 1369 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) ∈ (Base‘𝑌))
32825, 26, 253, 293, 327, 252, 172ablsubsub4 19008 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = (((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
32925, 26, 253grpaddsubass 18257 . . . . 5 ((𝑌 ∈ Grp ∧ ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) ∈ (Base‘𝑌) ∧ (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌) ∧ ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
330221, 321, 70, 172, 329syl13anc 1370 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
331325, 328, 3303eqtr3d 2802 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
3326, 2, 3, 4, 5mat2pmatbas 21427 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘(𝑖 − 1)) ∈ 𝐵) → (𝑇‘(𝑏‘(𝑖 − 1))) ∈ (Base‘𝑌))
333236, 237, 309, 332syl3anc 1369 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑇‘(𝑏‘(𝑖 − 1))) ∈ (Base‘𝑌))
33425, 9, 136, 137, 253, 223, 233, 333, 249lmodsubdi 19760 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))) = (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))
335334eqcomd 2765 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))) = ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))
336335mpteq2dva 5128 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))
337336oveq2d 7167 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
338337oveq1d 7166 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
339218, 331, 3383eqtrd 2798 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
34016, 192, 3393eqtrd 2798 1 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  Vcvv 3410   ⊆ wss 3859  {csn 4523   ↦ cmpt 5113  ⟶wf 6332  ‘cfv 6336  (class class class)co 7151   ↑m cmap 8417  Fincfn 8528  ℂcc 10574  0cc0 10576  1c1 10577   + caddc 10579   − cmin 10909  ℕcn 11675  ℕ0cn0 11935  ℤcz 12021  ℤ≥cuz 12283  ...cfz 12940  ..^cfzo 13083  Basecbs 16542  +gcplusg 16624  .rcmulr 16625  Scalarcsca 16627   ·𝑠 cvsca 16628  0gc0g 16772   Σg cgsu 16773  Mndcmnd 17978  Grpcgrp 18170  -gcsg 18172  .gcmg 18292  CMndccmn 18974  Abelcabl 18975  mulGrpcmgp 19308  1rcur 19320  Ringcrg 19366  CRingccrg 19367  LModclmod 19703  var1cv1 20901  Poly1cpl1 20902   Mat cmat 21108   matToPolyMat cmat2pmat 21405 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10632  ax-resscn 10633  ax-1cn 10634  ax-icn 10635  ax-addcl 10636  ax-addrcl 10637  ax-mulcl 10638  ax-mulrcl 10639  ax-mulcom 10640  ax-addass 10641  ax-mulass 10642  ax-distr 10643  ax-i2m1 10644  ax-1ne0 10645  ax-1rid 10646  ax-rnegex 10647  ax-rrecex 10648  ax-cnre 10649  ax-pre-lttri 10650  ax-pre-lttrn 10651  ax-pre-ltadd 10652  ax-pre-mulgt0 10653 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-ot 4532  df-uni 4800  df-int 4840  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-se 5485  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7406  df-ofr 7407  df-om 7581  df-1st 7694  df-2nd 7695  df-supp 7837  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-er 8300  df-map 8419  df-pm 8420  df-ixp 8481  df-en 8529  df-dom 8530  df-sdom 8531  df-fin 8532  df-fsupp 8868  df-sup 8940  df-oi 9008  df-card 9402  df-pnf 10716  df-mnf 10717  df-xr 10718  df-ltxr 10719  df-le 10720  df-sub 10911  df-neg 10912  df-nn 11676  df-2 11738  df-3 11739  df-4 11740  df-5 11741  df-6 11742  df-7 11743  df-8 11744  df-9 11745  df-n0 11936  df-z 12022  df-dec 12139  df-uz 12284  df-fz 12941  df-fzo 13084  df-seq 13420  df-hash 13742  df-struct 16544  df-ndx 16545  df-slot 16546  df-base 16548  df-sets 16549  df-ress 16550  df-plusg 16637  df-mulr 16638  df-sca 16640  df-vsca 16641  df-ip 16642  df-tset 16643  df-ple 16644  df-ds 16646  df-hom 16648  df-cco 16649  df-0g 16774  df-gsum 16775  df-prds 16780  df-pws 16782  df-mre 16916  df-mrc 16917  df-acs 16919  df-mgm 17919  df-sgrp 17968  df-mnd 17979  df-mhm 18023  df-submnd 18024  df-grp 18173  df-minusg 18174  df-sbg 18175  df-mulg 18293  df-subg 18344  df-ghm 18424  df-cntz 18515  df-cmn 18976  df-abl 18977  df-mgp 19309  df-ur 19321  df-ring 19368  df-cring 19369  df-subrg 19602  df-lmod 19705  df-lss 19773  df-sra 20013  df-rgmod 20014  df-dsmm 20498  df-frlm 20513  df-assa 20619  df-ascl 20621  df-psr 20672  df-mvr 20673  df-mpl 20674  df-opsr 20676  df-psr1 20905  df-vr1 20906  df-ply1 20907  df-mamu 21087  df-mat 21109  df-mat2pmat 21408 This theorem is referenced by:  cpmadugsumfi  21578
 Copyright terms: Public domain W3C validator