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 20885. (Contributed by AV, 7-Nov-2019.)
Hypotheses
Ref Expression
cpmadugsum.a 𝐴 = (𝑁 Mat 𝑅)
cpmadugsum.y 𝑌 = (𝑁 Mat 𝑃)
cpmadugsum.t 𝑇 = (𝑁 matToPolyMat 𝑅)
Assertion
Ref Expression
cpmadugsumlemF (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (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 11491 . . . 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 20881 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ0𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))))
131, 12sylanr1 687 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))))
142, 3, 4, 5, 6, 7, 8, 9, 10, 11cpmadugsumlemC 20882 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ0𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))
151, 14sylanr1 687 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))
1613, 15oveq12d 6831 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
17 nncn 11220 . . . . . . . . 9 (𝑠 ∈ ℕ → 𝑠 ∈ ℂ)
18 npcan1 10647 . . . . . . . . . 10 (𝑠 ∈ ℂ → ((𝑠 − 1) + 1) = 𝑠)
1918eqcomd 2766 . . . . . . . . 9 (𝑠 ∈ ℂ → 𝑠 = ((𝑠 − 1) + 1))
2017, 19syl 17 . . . . . . . 8 (𝑠 ∈ ℕ → 𝑠 = ((𝑠 − 1) + 1))
2120oveq2d 6829 . . . . . . 7 (𝑠 ∈ ℕ → (0...𝑠) = (0...((𝑠 − 1) + 1)))
2221mpteq1d 4890 . . . . . 6 (𝑠 ∈ ℕ → (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))) = (𝑖 ∈ (0...((𝑠 − 1) + 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))
2322oveq2d 6829 . . . . 5 (𝑠 ∈ ℕ → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = (𝑌 Σg (𝑖 ∈ (0...((𝑠 − 1) + 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))))
2423ad2antrl 766 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = (𝑌 Σg (𝑖 ∈ (0...((𝑠 − 1) + 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))))
25 eqid 2760 . . . . 5 (Base‘𝑌) = (Base‘𝑌)
26 cpmadugsum.g . . . . 5 + = (+g𝑌)
27 crngring 18758 . . . . . . . . . 10 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
2827anim2i 594 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
29283adant3 1127 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
304, 5pmatring 20700 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
3129, 30syl 17 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Ring)
32 ringcmn 18781 . . . . . . 7 (𝑌 ∈ Ring → 𝑌 ∈ CMnd)
3331, 32syl 17 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ CMnd)
3433adantr 472 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑌 ∈ CMnd)
35 nnm1nn0 11526 . . . . . 6 (𝑠 ∈ ℕ → (𝑠 − 1) ∈ ℕ0)
3635ad2antrl 766 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑠 − 1) ∈ ℕ0)
37 simpll1 1255 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → 𝑁 ∈ Fin)
38273ad2ant2 1129 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑅 ∈ Ring)
3938adantr 472 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑅 ∈ Ring)
4039adantr 472 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → 𝑅 ∈ Ring)
41 elmapi 8045 . . . . . . . . . 10 (𝑏 ∈ (𝐵𝑚 (0...𝑠)) → 𝑏:(0...𝑠)⟶𝐵)
4221feq2d 6192 . . . . . . . . . 10 (𝑠 ∈ ℕ → (𝑏:(0...𝑠)⟶𝐵𝑏:(0...((𝑠 − 1) + 1))⟶𝐵))
4341, 42syl5ibcom 235 . . . . . . . . 9 (𝑏 ∈ (𝐵𝑚 (0...𝑠)) → (𝑠 ∈ ℕ → 𝑏:(0...((𝑠 − 1) + 1))⟶𝐵))
4443impcom 445 . . . . . . . 8 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑏:(0...((𝑠 − 1) + 1))⟶𝐵)
4544adantl 473 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑏:(0...((𝑠 − 1) + 1))⟶𝐵)
4645ffvelrnda 6522 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → (𝑏𝑖) ∈ 𝐵)
47 elfznn0 12626 . . . . . . . 8 (𝑖 ∈ (0...((𝑠 − 1) + 1)) → 𝑖 ∈ ℕ0)
4847adantl 473 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → 𝑖 ∈ ℕ0)
49 1nn0 11500 . . . . . . . 8 1 ∈ ℕ0
5049a1i 11 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → 1 ∈ ℕ0)
5148, 50nn0addcld 11547 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → (𝑖 + 1) ∈ ℕ0)
522, 3, 6, 4, 5, 25, 9, 8, 7mat2pmatscmxcl 20747 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑏𝑖) ∈ 𝐵 ∧ (𝑖 + 1) ∈ ℕ0)) → (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
5337, 40, 46, 51, 52syl22anc 1478 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...((𝑠 − 1) + 1))) → (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
5425, 26, 34, 36, 53gsummptfzsplit 18532 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...((𝑠 − 1) + 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (𝑌 Σg (𝑖 ∈ {((𝑠 − 1) + 1)} ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))))
55 ringmnd 18756 . . . . . . . 8 (𝑌 ∈ Ring → 𝑌 ∈ Mnd)
5631, 55syl 17 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Mnd)
5756adantr 472 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑌 ∈ Mnd)
58 ovexd 6843 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑠 − 1) + 1) ∈ V)
59 simpl1 1228 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑁 ∈ Fin)
60 nn0fz0 12631 . . . . . . . . . . 11 (𝑠 ∈ ℕ0𝑠 ∈ (0...𝑠))
611, 60sylib 208 . . . . . . . . . 10 (𝑠 ∈ ℕ → 𝑠 ∈ (0...𝑠))
62 ffvelrn 6520 . . . . . . . . . 10 ((𝑏:(0...𝑠)⟶𝐵𝑠 ∈ (0...𝑠)) → (𝑏𝑠) ∈ 𝐵)
6341, 61, 62syl2anr 496 . . . . . . . . 9 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑏𝑠) ∈ 𝐵)
641adantr 472 . . . . . . . . . 10 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑠 ∈ ℕ0)
6549a1i 11 . . . . . . . . . 10 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 1 ∈ ℕ0)
6664, 65nn0addcld 11547 . . . . . . . . 9 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑠 + 1) ∈ ℕ0)
6763, 66jca 555 . . . . . . . 8 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → ((𝑏𝑠) ∈ 𝐵 ∧ (𝑠 + 1) ∈ ℕ0))
6867adantl 473 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑏𝑠) ∈ 𝐵 ∧ (𝑠 + 1) ∈ ℕ0))
692, 3, 6, 4, 5, 25, 9, 8, 7mat2pmatscmxcl 20747 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑏𝑠) ∈ 𝐵 ∧ (𝑠 + 1) ∈ ℕ0)) → (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌))
7059, 39, 68, 69syl21anc 1476 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌))
71 oveq1 6820 . . . . . . . . 9 (𝑖 = ((𝑠 − 1) + 1) → (𝑖 + 1) = (((𝑠 − 1) + 1) + 1))
7271oveq1d 6828 . . . . . . . 8 (𝑖 = ((𝑠 − 1) + 1) → ((𝑖 + 1) 𝑋) = ((((𝑠 − 1) + 1) + 1) 𝑋))
73 fveq2 6352 . . . . . . . . 9 (𝑖 = ((𝑠 − 1) + 1) → (𝑏𝑖) = (𝑏‘((𝑠 − 1) + 1)))
7473fveq2d 6356 . . . . . . . 8 (𝑖 = ((𝑠 − 1) + 1) → (𝑇‘(𝑏𝑖)) = (𝑇‘(𝑏‘((𝑠 − 1) + 1))))
7572, 74oveq12d 6831 . . . . . . 7 (𝑖 = ((𝑠 − 1) + 1) → (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) = (((((𝑠 − 1) + 1) + 1) 𝑋) · (𝑇‘(𝑏‘((𝑠 − 1) + 1)))))
7617, 18syl 17 . . . . . . . . . . 11 (𝑠 ∈ ℕ → ((𝑠 − 1) + 1) = 𝑠)
7776oveq1d 6828 . . . . . . . . . 10 (𝑠 ∈ ℕ → (((𝑠 − 1) + 1) + 1) = (𝑠 + 1))
7877oveq1d 6828 . . . . . . . . 9 (𝑠 ∈ ℕ → ((((𝑠 − 1) + 1) + 1) 𝑋) = ((𝑠 + 1) 𝑋))
7976fveq2d 6356 . . . . . . . . . 10 (𝑠 ∈ ℕ → (𝑏‘((𝑠 − 1) + 1)) = (𝑏𝑠))
8079fveq2d 6356 . . . . . . . . 9 (𝑠 ∈ ℕ → (𝑇‘(𝑏‘((𝑠 − 1) + 1))) = (𝑇‘(𝑏𝑠)))
8178, 80oveq12d 6831 . . . . . . . 8 (𝑠 ∈ ℕ → (((((𝑠 − 1) + 1) + 1) 𝑋) · (𝑇‘(𝑏‘((𝑠 − 1) + 1)))) = (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))))
8281ad2antrl 766 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (((((𝑠 − 1) + 1) + 1) 𝑋) · (𝑇‘(𝑏‘((𝑠 − 1) + 1)))) = (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))))
8375, 82sylan9eqr 2816 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 = ((𝑠 − 1) + 1)) → (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) = (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))))
8425, 57, 58, 70, 83gsumsnd 18552 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {((𝑠 − 1) + 1)} ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))))
8584oveq2d 6829 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (𝑌 Σg (𝑖 ∈ {((𝑠 − 1) + 1)} ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))))
8624, 54, 853eqtrd 2798 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))))
871ad2antrl 766 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑠 ∈ ℕ0)
884, 5pmatlmod 20701 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ LMod)
8928, 88syl 17 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ LMod)
90893adant3 1127 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ LMod)
9190adantr 472 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑌 ∈ LMod)
9291adantr 472 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑌 ∈ LMod)
934ply1ring 19820 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
9427, 93syl 17 . . . . . . . . . . . 12 (𝑅 ∈ CRing → 𝑃 ∈ Ring)
95943ad2ant2 1129 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑃 ∈ Ring)
96 eqid 2760 . . . . . . . . . . . 12 (mulGrp‘𝑃) = (mulGrp‘𝑃)
9796ringmgp 18753 . . . . . . . . . . 11 (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
9895, 97syl 17 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (mulGrp‘𝑃) ∈ Mnd)
9998adantr 472 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (mulGrp‘𝑃) ∈ Mnd)
10099adantr 472 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (mulGrp‘𝑃) ∈ Mnd)
101 elfznn0 12626 . . . . . . . . 9 (𝑖 ∈ (0...𝑠) → 𝑖 ∈ ℕ0)
102101adantl 473 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑖 ∈ ℕ0)
103 eqid 2760 . . . . . . . . . . . . 13 (Base‘𝑃) = (Base‘𝑃)
1047, 4, 103vr1cl 19789 . . . . . . . . . . . 12 (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
10527, 104syl 17 . . . . . . . . . . 11 (𝑅 ∈ CRing → 𝑋 ∈ (Base‘𝑃))
1061053ad2ant2 1129 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑋 ∈ (Base‘𝑃))
107106adantr 472 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑋 ∈ (Base‘𝑃))
108107adantr 472 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑋 ∈ (Base‘𝑃))
10996, 103mgpbas 18695 . . . . . . . . 9 (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
110109, 8mulgnn0cl 17759 . . . . . . . 8 (((mulGrp‘𝑃) ∈ Mnd ∧ 𝑖 ∈ ℕ0𝑋 ∈ (Base‘𝑃)) → (𝑖 𝑋) ∈ (Base‘𝑃))
111100, 102, 108, 110syl3anc 1477 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑖 𝑋) ∈ (Base‘𝑃))
1124ply1crng 19770 . . . . . . . . . . . . . . 15 (𝑅 ∈ CRing → 𝑃 ∈ CRing)
113112anim2i 594 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing))
1141133adant3 1127 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing))
1155matsca2 20428 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝑌))
116114, 115syl 17 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑃 = (Scalar‘𝑌))
117116eqcomd 2766 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (Scalar‘𝑌) = 𝑃)
118117fveq2d 6356 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (Base‘(Scalar‘𝑌)) = (Base‘𝑃))
119118eleq2d 2825 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ((𝑖 𝑋) ∈ (Base‘(Scalar‘𝑌)) ↔ (𝑖 𝑋) ∈ (Base‘𝑃)))
120119adantr 472 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑖 𝑋) ∈ (Base‘(Scalar‘𝑌)) ↔ (𝑖 𝑋) ∈ (Base‘𝑃)))
121120adantr 472 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑖 𝑋) ∈ (Base‘(Scalar‘𝑌)) ↔ (𝑖 𝑋) ∈ (Base‘𝑃)))
122111, 121mpbird 247 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑖 𝑋) ∈ (Base‘(Scalar‘𝑌)))
12331adantr 472 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑌 ∈ Ring)
124123adantr 472 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑌 ∈ Ring)
125 simpll1 1255 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑁 ∈ Fin)
12639adantr 472 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑅 ∈ Ring)
127 simpll3 1259 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑀𝐵)
1286, 2, 3, 4, 5mat2pmatbas 20733 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
129125, 126, 127, 128syl3anc 1477 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑇𝑀) ∈ (Base‘𝑌))
13087adantr 472 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑠 ∈ ℕ0)
131 simprr 813 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑏 ∈ (𝐵𝑚 (0...𝑠)))
132131anim1i 593 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑏 ∈ (𝐵𝑚 (0...𝑠)) ∧ 𝑖 ∈ (0...𝑠)))
1332, 3, 4, 5, 6m2pmfzmap 20754 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0) ∧ (𝑏 ∈ (𝐵𝑚 (0...𝑠)) ∧ 𝑖 ∈ (0...𝑠))) → (𝑇‘(𝑏𝑖)) ∈ (Base‘𝑌))
134125, 126, 130, 132, 133syl31anc 1480 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑇‘(𝑏𝑖)) ∈ (Base‘𝑌))
13525, 10ringcl 18761 . . . . . . 7 ((𝑌 ∈ Ring ∧ (𝑇𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏𝑖)) ∈ (Base‘𝑌)) → ((𝑇𝑀) × (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
136124, 129, 134, 135syl3anc 1477 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑇𝑀) × (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
137 eqid 2760 . . . . . . 7 (Scalar‘𝑌) = (Scalar‘𝑌)
138 eqid 2760 . . . . . . 7 (Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌))
13925, 137, 9, 138lmodvscl 19082 . . . . . 6 ((𝑌 ∈ LMod ∧ (𝑖 𝑋) ∈ (Base‘(Scalar‘𝑌)) ∧ ((𝑇𝑀) × (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌)) → ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) ∈ (Base‘𝑌))
14092, 122, 136, 139syl3anc 1477 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) ∈ (Base‘𝑌))
14125, 26, 34, 87, 140gsummptfzsplitl 18533 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
142 0nn0 11499 . . . . . . . 8 0 ∈ ℕ0
143142a1i 11 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 0 ∈ ℕ0)
144 eqid 2760 . . . . . . . . . . . . 13 (0g‘(mulGrp‘𝑃)) = (0g‘(mulGrp‘𝑃))
145109, 144, 8mulg0 17747 . . . . . . . . . . . 12 (𝑋 ∈ (Base‘𝑃) → (0 𝑋) = (0g‘(mulGrp‘𝑃)))
146106, 145syl 17 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (0 𝑋) = (0g‘(mulGrp‘𝑃)))
147146adantr 472 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (0 𝑋) = (0g‘(mulGrp‘𝑃)))
148147oveq1d 6828 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((0g‘(mulGrp‘𝑃)) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
149 eqid 2760 . . . . . . . . . . . . 13 (1r𝑃) = (1r𝑃)
15096, 149ringidval 18703 . . . . . . . . . . . 12 (1r𝑃) = (0g‘(mulGrp‘𝑃))
151150a1i 11 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (1r𝑃) = (0g‘(mulGrp‘𝑃)))
152151eqcomd 2766 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (0g‘(mulGrp‘𝑃)) = (1r𝑃))
153152oveq1d 6828 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((0g‘(mulGrp‘𝑃)) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((1r𝑃) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
154116adantr 472 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑃 = (Scalar‘𝑌))
155154fveq2d 6356 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (1r𝑃) = (1r‘(Scalar‘𝑌)))
156155oveq1d 6828 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((1r𝑃) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((1r‘(Scalar‘𝑌)) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
15727, 128syl3an2 1168 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
158157adantr 472 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑇𝑀) ∈ (Base‘𝑌))
159 simpl 474 . . . . . . . . . . . . . . . . . 18 ((𝑏:(0...𝑠)⟶𝐵𝑠 ∈ ℕ) → 𝑏:(0...𝑠)⟶𝐵)
160 elnn0uz 11918 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ℕ0𝑠 ∈ (ℤ‘0))
1611, 160sylib 208 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ℕ → 𝑠 ∈ (ℤ‘0))
162 eluzfz1 12541 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (ℤ‘0) → 0 ∈ (0...𝑠))
163161, 162syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ℕ → 0 ∈ (0...𝑠))
164163adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝑏:(0...𝑠)⟶𝐵𝑠 ∈ ℕ) → 0 ∈ (0...𝑠))
165159, 164ffvelrnd 6523 . . . . . . . . . . . . . . . . 17 ((𝑏:(0...𝑠)⟶𝐵𝑠 ∈ ℕ) → (𝑏‘0) ∈ 𝐵)
166165ex 449 . . . . . . . . . . . . . . . 16 (𝑏:(0...𝑠)⟶𝐵 → (𝑠 ∈ ℕ → (𝑏‘0) ∈ 𝐵))
16741, 166syl 17 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝐵𝑚 (0...𝑠)) → (𝑠 ∈ ℕ → (𝑏‘0) ∈ 𝐵))
168167impcom 445 . . . . . . . . . . . . . 14 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑏‘0) ∈ 𝐵)
169168adantl 473 . . . . . . . . . . . . 13 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑏‘0) ∈ 𝐵)
1706, 2, 3, 4, 5mat2pmatbas 20733 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌))
17159, 39, 169, 170syl3anc 1477 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌))
17225, 10ringcl 18761 . . . . . . . . . . . 12 ((𝑌 ∈ Ring ∧ (𝑇𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) → ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))
173123, 158, 171, 172syl3anc 1477 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))
174 eqid 2760 . . . . . . . . . . . 12 (1r‘(Scalar‘𝑌)) = (1r‘(Scalar‘𝑌))
17525, 137, 9, 174lmodvs1 19093 . . . . . . . . . . 11 ((𝑌 ∈ LMod ∧ ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) → ((1r‘(Scalar‘𝑌)) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑇𝑀) × (𝑇‘(𝑏‘0))))
17691, 173, 175syl2anc 696 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((1r‘(Scalar‘𝑌)) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑇𝑀) × (𝑇‘(𝑏‘0))))
177156, 176eqtrd 2794 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((1r𝑃) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑇𝑀) × (𝑇‘(𝑏‘0))))
178148, 153, 1773eqtrd 2798 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑇𝑀) × (𝑇‘(𝑏‘0))))
179178, 173eqeltrd 2839 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) ∈ (Base‘𝑌))
180 oveq1 6820 . . . . . . . . 9 (𝑖 = 0 → (𝑖 𝑋) = (0 𝑋))
181 fveq2 6352 . . . . . . . . . . 11 (𝑖 = 0 → (𝑏𝑖) = (𝑏‘0))
182181fveq2d 6356 . . . . . . . . . 10 (𝑖 = 0 → (𝑇‘(𝑏𝑖)) = (𝑇‘(𝑏‘0)))
183182oveq2d 6829 . . . . . . . . 9 (𝑖 = 0 → ((𝑇𝑀) × (𝑇‘(𝑏𝑖))) = ((𝑇𝑀) × (𝑇‘(𝑏‘0))))
184180, 183oveq12d 6831 . . . . . . . 8 (𝑖 = 0 → ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) = ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
185184adantl 473 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 = 0) → ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) = ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
18625, 57, 143, 179, 185gsumsnd 18552 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) = ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
187109, 150, 8mulg0 17747 . . . . . . . . 9 (𝑋 ∈ (Base‘𝑃) → (0 𝑋) = (1r𝑃))
188106, 187syl 17 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (0 𝑋) = (1r𝑃))
189188adantr 472 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (0 𝑋) = (1r𝑃))
190189oveq1d 6828 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((0 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((1r𝑃) · ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
191186, 190, 1773eqtrd 2798 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) = ((𝑇𝑀) × (𝑇‘(𝑏‘0))))
192191oveq2d 6829 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
193141, 192eqtrd 2794 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
19486, 193oveq12d 6831 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = (((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
195 fzfid 12966 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (0...(𝑠 − 1)) ∈ Fin)
196 simpll1 1255 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → 𝑁 ∈ Fin)
19739adantr 472 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → 𝑅 ∈ Ring)
19841adantl 473 . . . . . . . . . . 11 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑏:(0...𝑠)⟶𝐵)
199198adantr 472 . . . . . . . . . 10 (((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → 𝑏:(0...𝑠)⟶𝐵)
200 nnz 11591 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ℕ → 𝑠 ∈ ℤ)
201 fzoval 12665 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ℤ → (0..^𝑠) = (0...(𝑠 − 1)))
202200, 201syl 17 . . . . . . . . . . . . . . 15 (𝑠 ∈ ℕ → (0..^𝑠) = (0...(𝑠 − 1)))
203202eqcomd 2766 . . . . . . . . . . . . . 14 (𝑠 ∈ ℕ → (0...(𝑠 − 1)) = (0..^𝑠))
204203eleq2d 2825 . . . . . . . . . . . . 13 (𝑠 ∈ ℕ → (𝑖 ∈ (0...(𝑠 − 1)) ↔ 𝑖 ∈ (0..^𝑠)))
205 elfzofz 12679 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑠) → 𝑖 ∈ (0...𝑠))
206204, 205syl6bi 243 . . . . . . . . . . . 12 (𝑠 ∈ ℕ → (𝑖 ∈ (0...(𝑠 − 1)) → 𝑖 ∈ (0...𝑠)))
207206adantr 472 . . . . . . . . . . 11 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑖 ∈ (0...(𝑠 − 1)) → 𝑖 ∈ (0...𝑠)))
208207imp 444 . . . . . . . . . 10 (((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → 𝑖 ∈ (0...𝑠))
209199, 208ffvelrnd 6523 . . . . . . . . 9 (((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → (𝑏𝑖) ∈ 𝐵)
210209adantll 752 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → (𝑏𝑖) ∈ 𝐵)
211 elfznn0 12626 . . . . . . . . . 10 (𝑖 ∈ (0...(𝑠 − 1)) → 𝑖 ∈ ℕ0)
212211adantl 473 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → 𝑖 ∈ ℕ0)
21349a1i 11 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → 1 ∈ ℕ0)
214212, 213nn0addcld 11547 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → (𝑖 + 1) ∈ ℕ0)
215196, 197, 210, 214, 52syl22anc 1478 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 − 1))) → (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
216215ralrimiva 3104 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ∀𝑖 ∈ (0...(𝑠 − 1))(((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
21725, 34, 195, 216gsummptcl 18566 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌))
21825, 26cmncom 18409 . . . . 5 ((𝑌 ∈ CMnd ∧ (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌) ∧ (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌)) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) = ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))))
21934, 217, 70, 218syl3anc 1477 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) = ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))))
220219oveq1d 6828 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) = (((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
221 ringgrp 18752 . . . . . . . . 9 (𝑌 ∈ Ring → 𝑌 ∈ Grp)
22231, 221syl 17 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Grp)
223222adantr 472 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑌 ∈ Grp)
224 fzfid 12966 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (1...𝑠) ∈ Fin)
22591adantr 472 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑌 ∈ LMod)
22699adantr 472 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (mulGrp‘𝑃) ∈ Mnd)
227 elfznn 12563 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℕ)
228227nnnn0d 11543 . . . . . . . . . . . . 13 (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℕ0)
229228adantl 473 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 ∈ ℕ0)
230107adantr 472 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑋 ∈ (Base‘𝑃))
231226, 229, 230, 110syl3anc 1477 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑖 𝑋) ∈ (Base‘𝑃))
232116fveq2d 6356 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (Base‘𝑃) = (Base‘(Scalar‘𝑌)))
233232adantr 472 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (Base‘𝑃) = (Base‘(Scalar‘𝑌)))
234233adantr 472 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (Base‘𝑃) = (Base‘(Scalar‘𝑌)))
235231, 234eleqtrd 2841 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑖 𝑋) ∈ (Base‘(Scalar‘𝑌)))
236123adantr 472 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑌 ∈ Ring)
237158adantr 472 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑇𝑀) ∈ (Base‘𝑌))
238 simpll1 1255 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑁 ∈ Fin)
23939adantr 472 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑅 ∈ Ring)
240198adantl 473 . . . . . . . . . . . . . 14 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑏:(0...𝑠)⟶𝐵)
241240adantr 472 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑏:(0...𝑠)⟶𝐵)
242 1eluzge0 11925 . . . . . . . . . . . . . . . . 17 1 ∈ (ℤ‘0)
243 fzss1 12573 . . . . . . . . . . . . . . . . 17 (1 ∈ (ℤ‘0) → (1...𝑠) ⊆ (0...𝑠))
244242, 243mp1i 13 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ℕ → (1...𝑠) ⊆ (0...𝑠))
245244sseld 3743 . . . . . . . . . . . . . . 15 (𝑠 ∈ ℕ → (𝑖 ∈ (1...𝑠) → 𝑖 ∈ (0...𝑠)))
246245ad2antrl 766 . . . . . . . . . . . . . 14 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑖 ∈ (1...𝑠) → 𝑖 ∈ (0...𝑠)))
247246imp 444 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 ∈ (0...𝑠))
248241, 247ffvelrnd 6523 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑏𝑖) ∈ 𝐵)
2496, 2, 3, 4, 5mat2pmatbas 20733 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏𝑖) ∈ 𝐵) → (𝑇‘(𝑏𝑖)) ∈ (Base‘𝑌))
250238, 239, 248, 249syl3anc 1477 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑇‘(𝑏𝑖)) ∈ (Base‘𝑌))
251236, 237, 250, 135syl3anc 1477 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑇𝑀) × (𝑇‘(𝑏𝑖))) ∈ (Base‘𝑌))
252225, 235, 251, 139syl3anc 1477 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) ∈ (Base‘𝑌))
253252ralrimiva 3104 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ∀𝑖 ∈ (1...𝑠)((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) ∈ (Base‘𝑌))
25425, 34, 224, 253gsummptcl 18566 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) ∈ (Base‘𝑌))
255 cpmadugsum.s . . . . . . . 8 = (-g𝑌)
25625, 26, 255grpaddsubass 17706 . . . . . . 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...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))))
257223, 70, 217, 254, 256syl13anc 1479 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))))
258 oveq1 6820 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑖 → (𝑥 − 1) = (𝑖 − 1))
259258oveq1d 6828 . . . . . . . . . . . . . . 15 (𝑥 = 𝑖 → ((𝑥 − 1) + 1) = ((𝑖 − 1) + 1))
260259oveq1d 6828 . . . . . . . . . . . . . 14 (𝑥 = 𝑖 → (((𝑥 − 1) + 1) 𝑋) = (((𝑖 − 1) + 1) 𝑋))
261258fveq2d 6356 . . . . . . . . . . . . . . 15 (𝑥 = 𝑖 → (𝑏‘(𝑥 − 1)) = (𝑏‘(𝑖 − 1)))
262261fveq2d 6356 . . . . . . . . . . . . . 14 (𝑥 = 𝑖 → (𝑇‘(𝑏‘(𝑥 − 1))) = (𝑇‘(𝑏‘(𝑖 − 1))))
263260, 262oveq12d 6831 . . . . . . . . . . . . 13 (𝑥 = 𝑖 → ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))) = ((((𝑖 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))
264263cbvmptv 4902 . . . . . . . . . . . 12 (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1))))) = (𝑖 ∈ (1...𝑠) ↦ ((((𝑖 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))
265227nncnd 11228 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℂ)
266265adantl 473 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 ∈ ℂ)
267 npcan1 10647 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℂ → ((𝑖 − 1) + 1) = 𝑖)
268266, 267syl 17 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 − 1) + 1) = 𝑖)
269268oveq1d 6828 . . . . . . . . . . . . . 14 ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → (((𝑖 − 1) + 1) 𝑋) = (𝑖 𝑋))
270269oveq1d 6828 . . . . . . . . . . . . 13 ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → ((((𝑖 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) = ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))
271270mpteq2dva 4896 . . . . . . . . . . . 12 (𝑠 ∈ ℕ → (𝑖 ∈ (1...𝑠) ↦ ((((𝑖 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1))))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1))))))
272264, 271syl5eq 2806 . . . . . . . . . . 11 (𝑠 ∈ ℕ → (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1))))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1))))))
273272oveq2d 6829 . . . . . . . . . 10 (𝑠 ∈ ℕ → (𝑌 Σg (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))))
274273ad2antrl 766 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))))
275274oveq1d 6828 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑌 Σg (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
276 eqid 2760 . . . . . . . . . . 11 (0g𝑌) = (0g𝑌)
277 1zzd 11600 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 1 ∈ ℤ)
278 0zd 11581 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 0 ∈ ℤ)
27936nn0zd 11672 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑠 − 1) ∈ ℤ)
280 oveq1 6820 . . . . . . . . . . . . 13 (𝑖 = (𝑥 − 1) → (𝑖 + 1) = ((𝑥 − 1) + 1))
281280oveq1d 6828 . . . . . . . . . . . 12 (𝑖 = (𝑥 − 1) → ((𝑖 + 1) 𝑋) = (((𝑥 − 1) + 1) 𝑋))
282 fveq2 6352 . . . . . . . . . . . . 13 (𝑖 = (𝑥 − 1) → (𝑏𝑖) = (𝑏‘(𝑥 − 1)))
283282fveq2d 6356 . . . . . . . . . . . 12 (𝑖 = (𝑥 − 1) → (𝑇‘(𝑏𝑖)) = (𝑇‘(𝑏‘(𝑥 − 1))))
284281, 283oveq12d 6831 . . . . . . . . . . 11 (𝑖 = (𝑥 − 1) → (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))) = ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))
28525, 276, 34, 277, 278, 279, 215, 284gsummptshft 18536 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = (𝑌 Σg (𝑥 ∈ ((0 + 1)...((𝑠 − 1) + 1)) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))))
286 0p1e1 11324 . . . . . . . . . . . . . 14 (0 + 1) = 1
287286a1i 11 . . . . . . . . . . . . 13 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (0 + 1) = 1)
28876ad2antrl 766 . . . . . . . . . . . . 13 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑠 − 1) + 1) = 𝑠)
289287, 288oveq12d 6831 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((0 + 1)...((𝑠 − 1) + 1)) = (1...𝑠))
290289mpteq1d 4890 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑥 ∈ ((0 + 1)...((𝑠 − 1) + 1)) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1))))) = (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1))))))
291290oveq2d 6829 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑥 ∈ ((0 + 1)...((𝑠 − 1) + 1)) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))) = (𝑌 Σg (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))))
292285, 291eqtrd 2794 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) = (𝑌 Σg (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))))
293292oveq1d 6828 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑥 ∈ (1...𝑠) ↦ ((((𝑥 − 1) + 1) 𝑋) · (𝑇‘(𝑏‘(𝑥 − 1)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
294 ringabl 18780 . . . . . . . . . . 11 (𝑌 ∈ Ring → 𝑌 ∈ Abel)
29531, 294syl 17 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Abel)
296295adantr 472 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝑌 ∈ Abel)
297227adantl 473 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 ∈ ℕ)
298 nnz 11591 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
299 elfzm1b 12611 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑖 ∈ (1...𝑠) ↔ (𝑖 − 1) ∈ (0...(𝑠 − 1))))
300298, 200, 299syl2an 495 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑖 ∈ (1...𝑠) ↔ (𝑖 − 1) ∈ (0...(𝑠 − 1))))
301202adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (0..^𝑠) = (0...(𝑠 − 1)))
302301eqcomd 2766 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (0...(𝑠 − 1)) = (0..^𝑠))
303302eleq2d 2825 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ) → ((𝑖 − 1) ∈ (0...(𝑠 − 1)) ↔ (𝑖 − 1) ∈ (0..^𝑠)))
304 elfzofz 12679 . . . . . . . . . . . . . . . . . 18 ((𝑖 − 1) ∈ (0..^𝑠) → (𝑖 − 1) ∈ (0...𝑠))
305303, 304syl6bi 243 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ) → ((𝑖 − 1) ∈ (0...(𝑠 − 1)) → (𝑖 − 1) ∈ (0...𝑠)))
306300, 305sylbid 230 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑖 ∈ (1...𝑠) → (𝑖 − 1) ∈ (0...𝑠)))
307306expimpd 630 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → (𝑖 − 1) ∈ (0...𝑠)))
308297, 307mpcom 38 . . . . . . . . . . . . . 14 ((𝑠 ∈ ℕ ∧ 𝑖 ∈ (1...𝑠)) → (𝑖 − 1) ∈ (0...𝑠))
309308ex 449 . . . . . . . . . . . . 13 (𝑠 ∈ ℕ → (𝑖 ∈ (1...𝑠) → (𝑖 − 1) ∈ (0...𝑠)))
310309ad2antrl 766 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑖 ∈ (1...𝑠) → (𝑖 − 1) ∈ (0...𝑠)))
311310imp 444 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑖 − 1) ∈ (0...𝑠))
312241, 311ffvelrnd 6523 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑏‘(𝑖 − 1)) ∈ 𝐵)
3132, 3, 6, 4, 5, 25, 9, 8, 7mat2pmatscmxcl 20747 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑏‘(𝑖 − 1)) ∈ 𝐵𝑖 ∈ ℕ0)) → ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ∈ (Base‘𝑌))
314238, 239, 312, 229, 313syl22anc 1478 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ∈ (Base‘𝑌))
315 eqid 2760 . . . . . . . . 9 (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1))))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))
316 eqid 2760 . . . . . . . . 9 (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
31725, 255, 296, 224, 314, 252, 315, 316gsummptfidmsub 18550 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
318275, 293, 3173eqtr4d 2804 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
319318oveq2d 6829 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + ((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))) = ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))))
320223adantr 472 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑌 ∈ Grp)
32125, 255grpsubcl 17696 . . . . . . . . . 10 ((𝑌 ∈ Grp ∧ ((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ∈ (Base‘𝑌) ∧ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) ∈ (Base‘𝑌)) → (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌))
322320, 314, 252, 321syl3anc 1477 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌))
323322ralrimiva 3104 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ∀𝑖 ∈ (1...𝑠)(((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌))
32425, 34, 224, 323gsummptcl 18566 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) ∈ (Base‘𝑌))
32525, 26cmncom 18409 . . . . . . 7 ((𝑌 ∈ CMnd ∧ (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌) ∧ (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) ∈ (Base‘𝑌)) → ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))))
32634, 70, 324, 325syl3anc 1477 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))))
327257, 319, 3263eqtrd 2798 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))))
328327oveq1d 6828 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
32925, 26mndcl 17502 . . . . . 6 ((𝑌 ∈ Mnd ∧ (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌) ∧ (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) ∈ (Base‘𝑌)) → ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) ∈ (Base‘𝑌))
33057, 70, 217, 329syl3anc 1477 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) ∈ (Base‘𝑌))
33125, 26, 255, 296, 330, 254, 173ablsubsub4 18424 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = (((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
33225, 26, 255grpaddsubass 17706 . . . . 5 ((𝑌 ∈ Grp ∧ ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) ∈ (Base‘𝑌) ∧ (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌) ∧ ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
333223, 324, 70, 173, 332syl13anc 1479 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
334328, 331, 3333eqtr3d 2802 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) + (𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
3356, 2, 3, 4, 5mat2pmatbas 20733 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘(𝑖 − 1)) ∈ 𝐵) → (𝑇‘(𝑏‘(𝑖 − 1))) ∈ (Base‘𝑌))
336238, 239, 312, 335syl3anc 1477 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑇‘(𝑏‘(𝑖 − 1))) ∈ (Base‘𝑌))
33725, 9, 137, 138, 255, 225, 235, 336, 251lmodsubdi 19122 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))) = (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))
338337eqcomd 2766 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))) = ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))
339338mpteq2dva 4896 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))
340339oveq2d 6829 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
341340oveq1d 6828 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 𝑋) · (𝑇‘(𝑏‘(𝑖 − 1)))) ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
342220, 334, 3413eqtrd 2798 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (0...(𝑠 − 1)) ↦ (((𝑖 + 1) 𝑋) · (𝑇‘(𝑏𝑖))))) + (((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠)))) ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))) + ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
34316, 194, 3423eqtrd 2798 1 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139  Vcvv 3340   ⊆ wss 3715  {csn 4321   ↦ cmpt 4881  ⟶wf 6045  ‘cfv 6049  (class class class)co 6813   ↑𝑚 cmap 8023  Fincfn 8121  ℂcc 10126  0cc0 10128  1c1 10129   + caddc 10131   − cmin 10458  ℕcn 11212  ℕ0cn0 11484  ℤcz 11569  ℤ≥cuz 11879  ...cfz 12519  ..^cfzo 12659  Basecbs 16059  +gcplusg 16143  .rcmulr 16144  Scalarcsca 16146   ·𝑠 cvsca 16147  0gc0g 16302   Σg cgsu 16303  Mndcmnd 17495  Grpcgrp 17623  -gcsg 17625  .gcmg 17741  CMndccmn 18393  Abelcabl 18394  mulGrpcmgp 18689  1rcur 18701  Ringcrg 18747  CRingccrg 18748  LModclmod 19065  var1cv1 19748  Poly1cpl1 19749   Mat cmat 20415   matToPolyMat cmat2pmat 20711 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-ot 4330  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-ofr 7063  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-sup 8513  df-oi 8580  df-card 8955  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-fz 12520  df-fzo 12660  df-seq 12996  df-hash 13312  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-hom 16168  df-cco 16169  df-0g 16304  df-gsum 16305  df-prds 16310  df-pws 16312  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-mhm 17536  df-submnd 17537  df-grp 17626  df-minusg 17627  df-sbg 17628  df-mulg 17742  df-subg 17792  df-ghm 17859  df-cntz 17950  df-cmn 18395  df-abl 18396  df-mgp 18690  df-ur 18702  df-ring 18749  df-cring 18750  df-subrg 18980  df-lmod 19067  df-lss 19135  df-sra 19374  df-rgmod 19375  df-assa 19514  df-ascl 19516  df-psr 19558  df-mvr 19559  df-mpl 19560  df-opsr 19562  df-psr1 19752  df-vr1 19753  df-ply1 19754  df-dsmm 20278  df-frlm 20293  df-mamu 20392  df-mat 20416  df-mat2pmat 20714 This theorem is referenced by:  cpmadugsumfi  20884
 Copyright terms: Public domain W3C validator