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

Theorem chfacfpmmulgsum 21615
Description: Breaking up a sum of values of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019.)
Hypotheses
Ref Expression
cayhamlem1.a 𝐴 = (𝑁 Mat 𝑅)
cayhamlem1.b 𝐵 = (Base‘𝐴)
cayhamlem1.p 𝑃 = (Poly1𝑅)
cayhamlem1.y 𝑌 = (𝑁 Mat 𝑃)
cayhamlem1.r × = (.r𝑌)
cayhamlem1.s = (-g𝑌)
cayhamlem1.0 0 = (0g𝑌)
cayhamlem1.t 𝑇 = (𝑁 matToPolyMat 𝑅)
cayhamlem1.g 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))))
cayhamlem1.e = (.g‘(mulGrp‘𝑌))
chfacfpmmulgsum.p + = (+g𝑌)
Assertion
Ref Expression
chfacfpmmulgsum (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
Distinct variable groups:   𝐵,𝑛   𝑛,𝑀   𝑛,𝑁   𝑅,𝑛   𝑛,𝑌   𝑛,𝑏   𝑛,𝑠   0 ,𝑛   𝐵,𝑖   𝑖,𝐺   𝑖,𝑀   𝑖,𝑁   𝑅,𝑖   𝑇,𝑖   × ,𝑖   ,𝑖   𝑖,𝑠   𝑖,𝑏   𝑇,𝑛,𝑖   𝑖,𝑌   × ,𝑛   ,𝑛
Allowed substitution hints:   𝐴(𝑖,𝑛,𝑠,𝑏)   𝐵(𝑠,𝑏)   𝑃(𝑖,𝑛,𝑠,𝑏)   + (𝑖,𝑛,𝑠,𝑏)   𝑅(𝑠,𝑏)   𝑇(𝑠,𝑏)   × (𝑠,𝑏)   (𝑛,𝑠,𝑏)   𝐺(𝑛,𝑠,𝑏)   𝑀(𝑠,𝑏)   (𝑖,𝑠,𝑏)   𝑁(𝑠,𝑏)   𝑌(𝑠,𝑏)   0 (𝑖,𝑠,𝑏)

Proof of Theorem chfacfpmmulgsum
StepHypRef Expression
1 eqid 2738 . . 3 (Base‘𝑌) = (Base‘𝑌)
2 cayhamlem1.0 . . 3 0 = (0g𝑌)
3 chfacfpmmulgsum.p . . 3 + = (+g𝑌)
4 crngring 19428 . . . . . . . 8 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
54anim2i 620 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
653adant3 1133 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
7 cayhamlem1.p . . . . . . 7 𝑃 = (Poly1𝑅)
8 cayhamlem1.y . . . . . . 7 𝑌 = (𝑁 Mat 𝑃)
97, 8pmatring 21443 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
106, 9syl 17 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Ring)
11 ringcmn 19453 . . . . 5 (𝑌 ∈ Ring → 𝑌 ∈ CMnd)
1210, 11syl 17 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ CMnd)
1312adantr 484 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ CMnd)
14 nn0ex 11982 . . . 4 0 ∈ V
1514a1i 11 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ℕ0 ∈ V)
16 simpll 767 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵))
17 simplr 769 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))))
18 simpr 488 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
1916, 17, 183jca 1129 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑖 ∈ ℕ0))
20 cayhamlem1.a . . . . 5 𝐴 = (𝑁 Mat 𝑅)
21 cayhamlem1.b . . . . 5 𝐵 = (Base‘𝐴)
22 cayhamlem1.r . . . . 5 × = (.r𝑌)
23 cayhamlem1.s . . . . 5 = (-g𝑌)
24 cayhamlem1.t . . . . 5 𝑇 = (𝑁 matToPolyMat 𝑅)
25 cayhamlem1.g . . . . 5 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))))
26 cayhamlem1.e . . . . 5 = (.g‘(mulGrp‘𝑌))
2720, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 21612 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) ∈ (Base‘𝑌))
2819, 27syl 17 . . 3 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) ∈ (Base‘𝑌))
2920, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulfsupp 21614 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))) finSupp 0 )
30 nn0disj 13114 . . . 4 ((0...(𝑠 + 1)) ∩ (ℤ‘((𝑠 + 1) + 1))) = ∅
3130a1i 11 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0...(𝑠 + 1)) ∩ (ℤ‘((𝑠 + 1) + 1))) = ∅)
32 nnnn0 11983 . . . . . 6 (𝑠 ∈ ℕ → 𝑠 ∈ ℕ0)
33 peano2nn0 12016 . . . . . 6 (𝑠 ∈ ℕ0 → (𝑠 + 1) ∈ ℕ0)
3432, 33syl 17 . . . . 5 (𝑠 ∈ ℕ → (𝑠 + 1) ∈ ℕ0)
35 nn0split 13113 . . . . 5 ((𝑠 + 1) ∈ ℕ0 → ℕ0 = ((0...(𝑠 + 1)) ∪ (ℤ‘((𝑠 + 1) + 1))))
3634, 35syl 17 . . . 4 (𝑠 ∈ ℕ → ℕ0 = ((0...(𝑠 + 1)) ∪ (ℤ‘((𝑠 + 1) + 1))))
3736ad2antrl 728 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ℕ0 = ((0...(𝑠 + 1)) ∪ (ℤ‘((𝑠 + 1) + 1))))
381, 2, 3, 13, 15, 28, 29, 31, 37gsumsplit2 19168 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (𝑌 Σg (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))))))
39 simpll 767 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ‘((𝑠 + 1) + 1))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵))
40 simplr 769 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ‘((𝑠 + 1) + 1))) → (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))))
41 nncn 11724 . . . . . . . . . . . . 13 (𝑠 ∈ ℕ → 𝑠 ∈ ℂ)
42 add1p1 11967 . . . . . . . . . . . . 13 (𝑠 ∈ ℂ → ((𝑠 + 1) + 1) = (𝑠 + 2))
4341, 42syl 17 . . . . . . . . . . . 12 (𝑠 ∈ ℕ → ((𝑠 + 1) + 1) = (𝑠 + 2))
4443ad2antrl 728 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑠 + 1) + 1) = (𝑠 + 2))
4544fveq2d 6678 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (ℤ‘((𝑠 + 1) + 1)) = (ℤ‘(𝑠 + 2)))
4645eleq2d 2818 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↔ 𝑖 ∈ (ℤ‘(𝑠 + 2))))
4746biimpa 480 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ‘((𝑠 + 1) + 1))) → 𝑖 ∈ (ℤ‘(𝑠 + 2)))
4820, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmul0 21613 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑖 ∈ (ℤ‘(𝑠 + 2))) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) = 0 )
4939, 40, 47, 48syl3anc 1372 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ‘((𝑠 + 1) + 1))) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) = 0 )
5049mpteq2dva 5125 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))) = (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ 0 ))
5150oveq2d 7186 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = (𝑌 Σg (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ 0 )))
524, 9sylan2 596 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ Ring)
53 ringmnd 19426 . . . . . . . . . 10 (𝑌 ∈ Ring → 𝑌 ∈ Mnd)
5452, 53syl 17 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ Mnd)
55543adant3 1133 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Mnd)
56 fvex 6687 . . . . . . . 8 (ℤ‘((𝑠 + 1) + 1)) ∈ V
5755, 56jctir 524 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑌 ∈ Mnd ∧ (ℤ‘((𝑠 + 1) + 1)) ∈ V))
5857adantr 484 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 ∈ Mnd ∧ (ℤ‘((𝑠 + 1) + 1)) ∈ V))
592gsumz 18116 . . . . . 6 ((𝑌 ∈ Mnd ∧ (ℤ‘((𝑠 + 1) + 1)) ∈ V) → (𝑌 Σg (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ 0 )) = 0 )
6058, 59syl 17 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ 0 )) = 0 )
6151, 60eqtrd 2773 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = 0 )
6261oveq2d 7186 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (𝑌 Σg (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + 0 ))
63 fzfid 13432 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (0...(𝑠 + 1)) ∈ Fin)
64 elfznn0 13091 . . . . . . . 8 (𝑖 ∈ (0...(𝑠 + 1)) → 𝑖 ∈ ℕ0)
6564, 19sylan2 596 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 + 1))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑖 ∈ ℕ0))
6665, 27syl 17 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 + 1))) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) ∈ (Base‘𝑌))
6766ralrimiva 3096 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ∀𝑖 ∈ (0...(𝑠 + 1))((𝑖 (𝑇𝑀)) × (𝐺𝑖)) ∈ (Base‘𝑌))
681, 13, 63, 67gsummptcl 19206 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) ∈ (Base‘𝑌))
691, 3, 2mndrid 18048 . . . 4 ((𝑌 ∈ Mnd ∧ (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) ∈ (Base‘𝑌)) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + 0 ) = (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))))
7055, 68, 69syl2an2r 685 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + 0 ) = (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))))
7162, 70eqtrd 2773 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (𝑌 Σg (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))))) = (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))))
7232ad2antrl 728 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑠 ∈ ℕ0)
731, 3, 13, 72, 66gsummptfzsplit 19171 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))))))
74 elfznn0 13091 . . . . . . 7 (𝑖 ∈ (0...𝑠) → 𝑖 ∈ ℕ0)
7574, 28sylan2 596 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) ∈ (Base‘𝑌))
761, 3, 13, 72, 75gsummptfzsplitl 19172 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))))))
7755adantr 484 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ Mnd)
78 0nn0 11991 . . . . . . . 8 0 ∈ ℕ0
7978a1i 11 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 0 ∈ ℕ0)
8020, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 21612 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 0 ∈ ℕ0) → ((0 (𝑇𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌))
8179, 80mpd3an3 1463 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0 (𝑇𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌))
82 oveq1 7177 . . . . . . . . 9 (𝑖 = 0 → (𝑖 (𝑇𝑀)) = (0 (𝑇𝑀)))
83 fveq2 6674 . . . . . . . . 9 (𝑖 = 0 → (𝐺𝑖) = (𝐺‘0))
8482, 83oveq12d 7188 . . . . . . . 8 (𝑖 = 0 → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) = ((0 (𝑇𝑀)) × (𝐺‘0)))
851, 84gsumsn 19193 . . . . . . 7 ((𝑌 ∈ Mnd ∧ 0 ∈ ℕ0 ∧ ((0 (𝑇𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌)) → (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((0 (𝑇𝑀)) × (𝐺‘0)))
8677, 79, 81, 85syl3anc 1372 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((0 (𝑇𝑀)) × (𝐺‘0)))
8786oveq2d 7186 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + ((0 (𝑇𝑀)) × (𝐺‘0))))
8876, 87eqtrd 2773 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + ((0 (𝑇𝑀)) × (𝐺‘0))))
89 ovexd 7205 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑠 + 1) ∈ V)
90 1nn0 11992 . . . . . . . 8 1 ∈ ℕ0
9190a1i 11 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 1 ∈ ℕ0)
9272, 91nn0addcld 12040 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑠 + 1) ∈ ℕ0)
9320, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 21612 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ (𝑠 + 1) ∈ ℕ0) → (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌))
9492, 93mpd3an3 1463 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌))
95 oveq1 7177 . . . . . . 7 (𝑖 = (𝑠 + 1) → (𝑖 (𝑇𝑀)) = ((𝑠 + 1) (𝑇𝑀)))
96 fveq2 6674 . . . . . . 7 (𝑖 = (𝑠 + 1) → (𝐺𝑖) = (𝐺‘(𝑠 + 1)))
9795, 96oveq12d 7188 . . . . . 6 (𝑖 = (𝑠 + 1) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) = (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))))
981, 97gsumsn 19193 . . . . 5 ((𝑌 ∈ Mnd ∧ (𝑠 + 1) ∈ V ∧ (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌)) → (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))))
9977, 89, 94, 98syl3anc 1372 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))))
10088, 99oveq12d 7188 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))))) = (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + ((0 (𝑇𝑀)) × (𝐺‘0))) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))))
101 fzfid 13432 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (1...𝑠) ∈ Fin)
102 simpll 767 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵))
103 simplr 769 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))))
104 elfznn 13027 . . . . . . . . . 10 (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℕ)
105104nnnn0d 12036 . . . . . . . . 9 (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℕ0)
106105adantl 485 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 ∈ ℕ0)
107102, 103, 106, 27syl3anc 1372 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) ∈ (Base‘𝑌))
108107ralrimiva 3096 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ∀𝑖 ∈ (1...𝑠)((𝑖 (𝑇𝑀)) × (𝐺𝑖)) ∈ (Base‘𝑌))
1091, 13, 101, 108gsummptcl 19206 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) ∈ (Base‘𝑌))
1101, 3mndass 18036 . . . . 5 ((𝑌 ∈ Mnd ∧ ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) ∈ (Base‘𝑌) ∧ ((0 (𝑇𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌) ∧ (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + ((0 (𝑇𝑀)) × (𝐺‘0))) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (((0 (𝑇𝑀)) × (𝐺‘0)) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))))))
11177, 109, 81, 94, 110syl13anc 1373 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + ((0 (𝑇𝑀)) × (𝐺‘0))) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (((0 (𝑇𝑀)) × (𝐺‘0)) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))))))
112104nnne0d 11766 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑠) → 𝑖 ≠ 0)
113112ad2antlr 727 . . . . . . . . . . . . 13 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑖 ≠ 0)
114 neeq1 2996 . . . . . . . . . . . . . 14 (𝑛 = 𝑖 → (𝑛 ≠ 0 ↔ 𝑖 ≠ 0))
115114adantl 485 . . . . . . . . . . . . 13 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑛 ≠ 0 ↔ 𝑖 ≠ 0))
116113, 115mpbird 260 . . . . . . . . . . . 12 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 ≠ 0)
117 eqneqall 2945 . . . . . . . . . . . 12 (𝑛 = 0 → (𝑛 ≠ 0 → 0 = (𝑇‘(𝑏‘(𝑖 − 1)))))
118116, 117mpan9 510 . . . . . . . . . . 11 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → 0 = (𝑇‘(𝑏‘(𝑖 − 1))))
119 simplr 769 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → 𝑛 = 𝑖)
120 eqeq1 2742 . . . . . . . . . . . . . . . . 17 (0 = 𝑛 → (0 = 𝑖𝑛 = 𝑖))
121120eqcoms 2746 . . . . . . . . . . . . . . . 16 (𝑛 = 0 → (0 = 𝑖𝑛 = 𝑖))
122121adantl 485 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → (0 = 𝑖𝑛 = 𝑖))
123119, 122mpbird 260 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → 0 = 𝑖)
124123fveq2d 6678 . . . . . . . . . . . . 13 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → (𝑏‘0) = (𝑏𝑖))
125124fveq2d 6678 . . . . . . . . . . . 12 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → (𝑇‘(𝑏‘0)) = (𝑇‘(𝑏𝑖)))
126125oveq2d 7186 . . . . . . . . . . 11 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → ((𝑇𝑀) × (𝑇‘(𝑏‘0))) = ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))
127118, 126oveq12d 7188 . . . . . . . . . 10 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
128 elfz2 12988 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑠) ↔ ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (1 ≤ 𝑖𝑖𝑠)))
129 zleltp1 12114 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑖𝑠𝑖 < (𝑠 + 1)))
130129ancoms 462 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖𝑠𝑖 < (𝑠 + 1)))
1311303adant1 1131 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖𝑠𝑖 < (𝑠 + 1)))
132131biimpcd 252 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖𝑠 → ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → 𝑖 < (𝑠 + 1)))
133132adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((1 ≤ 𝑖𝑖𝑠) → ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → 𝑖 < (𝑠 + 1)))
134133impcom 411 . . . . . . . . . . . . . . . . . . . 20 (((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (1 ≤ 𝑖𝑖𝑠)) → 𝑖 < (𝑠 + 1))
135134orcd 872 . . . . . . . . . . . . . . . . . . 19 (((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (1 ≤ 𝑖𝑖𝑠)) → (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖))
136 zre 12066 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ℤ → 𝑠 ∈ ℝ)
137 1red 10720 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ℤ → 1 ∈ ℝ)
138136, 137readdcld 10748 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ℤ → (𝑠 + 1) ∈ ℝ)
139 zre 12066 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ℤ → 𝑖 ∈ ℝ)
140138, 139anim12ci 617 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ ℝ ∧ (𝑠 + 1) ∈ ℝ))
1411403adant1 1131 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ ℝ ∧ (𝑠 + 1) ∈ ℝ))
142 lttri2 10801 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ ℝ ∧ (𝑠 + 1) ∈ ℝ) → (𝑖 ≠ (𝑠 + 1) ↔ (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖)))
143141, 142syl 17 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ≠ (𝑠 + 1) ↔ (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖)))
144143adantr 484 . . . . . . . . . . . . . . . . . . 19 (((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (1 ≤ 𝑖𝑖𝑠)) → (𝑖 ≠ (𝑠 + 1) ↔ (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖)))
145135, 144mpbird 260 . . . . . . . . . . . . . . . . . 18 (((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (1 ≤ 𝑖𝑖𝑠)) → 𝑖 ≠ (𝑠 + 1))
146128, 145sylbi 220 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑠) → 𝑖 ≠ (𝑠 + 1))
147146ad2antlr 727 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑖 ≠ (𝑠 + 1))
148 neeq1 2996 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → (𝑛 ≠ (𝑠 + 1) ↔ 𝑖 ≠ (𝑠 + 1)))
149148adantl 485 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑛 ≠ (𝑠 + 1) ↔ 𝑖 ≠ (𝑠 + 1)))
150147, 149mpbird 260 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 ≠ (𝑠 + 1))
151150adantr 484 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → 𝑛 ≠ (𝑠 + 1))
152151neneqd 2939 . . . . . . . . . . . . 13 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → ¬ 𝑛 = (𝑠 + 1))
153152pm2.21d 121 . . . . . . . . . . . 12 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → (𝑛 = (𝑠 + 1) → (𝑇‘(𝑏𝑠)) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))
154153imp 410 . . . . . . . . . . 11 (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ 𝑛 = (𝑠 + 1)) → (𝑇‘(𝑏𝑠)) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
155104nnred 11731 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℝ)
156 eleq1w 2815 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → (𝑛 ∈ ℝ ↔ 𝑖 ∈ ℝ))
157155, 156syl5ibrcom 250 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑠) → (𝑛 = 𝑖𝑛 ∈ ℝ))
158157adantl 485 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑛 = 𝑖𝑛 ∈ ℝ))
159158imp 410 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 ∈ ℝ)
16072nn0red 12037 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑠 ∈ ℝ)
161160ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑠 ∈ ℝ)
162 1red 10720 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 1 ∈ ℝ)
163161, 162readdcld 10748 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑠 + 1) ∈ ℝ)
164128, 134sylbi 220 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑠) → 𝑖 < (𝑠 + 1))
165164ad2antlr 727 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑖 < (𝑠 + 1))
166 breq1 5033 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (𝑛 < (𝑠 + 1) ↔ 𝑖 < (𝑠 + 1)))
167166adantl 485 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑛 < (𝑠 + 1) ↔ 𝑖 < (𝑠 + 1)))
168165, 167mpbird 260 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 < (𝑠 + 1))
169159, 163, 168ltnsymd 10867 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → ¬ (𝑠 + 1) < 𝑛)
170169pm2.21d 121 . . . . . . . . . . . . . 14 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → ((𝑠 + 1) < 𝑛0 = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))
171170ad2antrr 726 . . . . . . . . . . . . 13 (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) → ((𝑠 + 1) < 𝑛0 = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))
172171imp 410 . . . . . . . . . . . 12 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ (𝑠 + 1) < 𝑛) → 0 = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
173 simp-4r 784 . . . . . . . . . . . . . . 15 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 = 𝑖)
174173fvoveq1d 7192 . . . . . . . . . . . . . 14 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑏‘(𝑛 − 1)) = (𝑏‘(𝑖 − 1)))
175174fveq2d 6678 . . . . . . . . . . . . 13 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑇‘(𝑏‘(𝑛 − 1))) = (𝑇‘(𝑏‘(𝑖 − 1))))
176173fveq2d 6678 . . . . . . . . . . . . . . 15 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑏𝑛) = (𝑏𝑖))
177176fveq2d 6678 . . . . . . . . . . . . . 14 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑇‘(𝑏𝑛)) = (𝑇‘(𝑏𝑖)))
178177oveq2d 7186 . . . . . . . . . . . . 13 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇𝑀) × (𝑇‘(𝑏𝑛))) = ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))
179175, 178oveq12d 7188 . . . . . . . . . . . 12 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛)))) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
180172, 179ifeqda 4450 . . . . . . . . . . 11 (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) → if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
181154, 180ifeqda 4450 . . . . . . . . . 10 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛)))))) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
182127, 181ifeqda 4450 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
183 ovexd 7205 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) ∈ V)
18425, 182, 106, 183fvmptd2 6783 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝐺𝑖) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
185184oveq2d 7186 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) = ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))
186185mpteq2dva 5125 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))
187186oveq2d 7186 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
188 nn0p1gt0 12005 . . . . . . . . . . . . . 14 (𝑠 ∈ ℕ0 → 0 < (𝑠 + 1))
189 0red 10722 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ℕ0 → 0 ∈ ℝ)
190 ltne 10815 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ 0 < (𝑠 + 1)) → (𝑠 + 1) ≠ 0)
191189, 190sylan 583 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℕ0 ∧ 0 < (𝑠 + 1)) → (𝑠 + 1) ≠ 0)
192 neeq1 2996 . . . . . . . . . . . . . . 15 (𝑛 = (𝑠 + 1) → (𝑛 ≠ 0 ↔ (𝑠 + 1) ≠ 0))
193191, 192syl5ibrcom 250 . . . . . . . . . . . . . 14 ((𝑠 ∈ ℕ0 ∧ 0 < (𝑠 + 1)) → (𝑛 = (𝑠 + 1) → 𝑛 ≠ 0))
19432, 188, 193syl2anc2 588 . . . . . . . . . . . . 13 (𝑠 ∈ ℕ → (𝑛 = (𝑠 + 1) → 𝑛 ≠ 0))
195194ad2antrl 728 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑛 = (𝑠 + 1) → 𝑛 ≠ 0))
196195imp 410 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) → 𝑛 ≠ 0)
197 eqneqall 2945 . . . . . . . . . . 11 (𝑛 = 0 → (𝑛 ≠ 0 → ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = (𝑇‘(𝑏𝑠))))
198196, 197mpan9 510 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) ∧ 𝑛 = 0) → ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = (𝑇‘(𝑏𝑠)))
199 iftrue 4420 . . . . . . . . . . 11 (𝑛 = (𝑠 + 1) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛)))))) = (𝑇‘(𝑏𝑠)))
200199ad2antlr 727 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) ∧ ¬ 𝑛 = 0) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛)))))) = (𝑇‘(𝑏𝑠)))
201198, 200ifeqda 4450 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) → if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))) = (𝑇‘(𝑏𝑠)))
20272, 33syl 17 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑠 + 1) ∈ ℕ0)
203 fvexd 6689 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑇‘(𝑏𝑠)) ∈ V)
20425, 201, 202, 203fvmptd2 6783 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝐺‘(𝑠 + 1)) = (𝑇‘(𝑏𝑠)))
205204oveq2d 7186 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) = (((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))))
20624, 20, 21, 7, 8mat2pmatbas 21477 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
2074, 206syl3an2 1165 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
208 eqid 2738 . . . . . . . . . . . . . 14 (mulGrp‘𝑌) = (mulGrp‘𝑌)
209208, 1mgpbas 19364 . . . . . . . . . . . . 13 (Base‘𝑌) = (Base‘(mulGrp‘𝑌))
210 eqid 2738 . . . . . . . . . . . . 13 (0g‘(mulGrp‘𝑌)) = (0g‘(mulGrp‘𝑌))
211209, 210, 26mulg0 18349 . . . . . . . . . . . 12 ((𝑇𝑀) ∈ (Base‘𝑌) → (0 (𝑇𝑀)) = (0g‘(mulGrp‘𝑌)))
212207, 211syl 17 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (0 (𝑇𝑀)) = (0g‘(mulGrp‘𝑌)))
213 eqid 2738 . . . . . . . . . . . 12 (1r𝑌) = (1r𝑌)
214208, 213ringidval 19372 . . . . . . . . . . 11 (1r𝑌) = (0g‘(mulGrp‘𝑌))
215212, 214eqtr4di 2791 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (0 (𝑇𝑀)) = (1r𝑌))
216215adantr 484 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (0 (𝑇𝑀)) = (1r𝑌))
217216oveq1d 7185 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0 (𝑇𝑀)) × (𝐺‘0)) = ((1r𝑌) × (𝐺‘0)))
218523adant3 1133 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Ring)
21920, 21, 7, 8, 22, 23, 2, 24, 25chfacfisf 21605 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌))
2204, 219syl3anl2 1414 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌))
221220, 79ffvelrnd 6862 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝐺‘0) ∈ (Base‘𝑌))
2221, 22, 213ringlidm 19443 . . . . . . . . 9 ((𝑌 ∈ Ring ∧ (𝐺‘0) ∈ (Base‘𝑌)) → ((1r𝑌) × (𝐺‘0)) = (𝐺‘0))
223218, 221, 222syl2an2r 685 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((1r𝑌) × (𝐺‘0)) = (𝐺‘0))
224 iftrue 4420 . . . . . . . . 9 (𝑛 = 0 → if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))) = ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
225 ovexd 7205 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) ∈ V)
22625, 224, 79, 225fvmptd3 6798 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝐺‘0) = ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
227217, 223, 2263eqtrd 2777 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0 (𝑇𝑀)) × (𝐺‘0)) = ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
228205, 227oveq12d 7188 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) + ((0 (𝑇𝑀)) × (𝐺‘0))) = ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) + ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
2291, 3cmncom 19041 . . . . . . 7 ((𝑌 ∈ CMnd ∧ ((0 (𝑇𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌) ∧ (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌)) → (((0 (𝑇𝑀)) × (𝐺‘0)) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))) = ((((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) + ((0 (𝑇𝑀)) × (𝐺‘0))))
23013, 81, 94, 229syl3anc 1372 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((0 (𝑇𝑀)) × (𝐺‘0)) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))) = ((((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) + ((0 (𝑇𝑀)) × (𝐺‘0))))
231 ringgrp 19421 . . . . . . . . 9 (𝑌 ∈ Ring → 𝑌 ∈ Grp)
23210, 231syl 17 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Grp)
233232adantr 484 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ Grp)
234205, 94eqeltrrd 2834 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌))
23510adantr 484 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ Ring)
236207adantr 484 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑇𝑀) ∈ (Base‘𝑌))
237 simpl1 1192 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑁 ∈ Fin)
23843ad2ant2 1135 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑅 ∈ Ring)
239238adantr 484 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑅 ∈ Ring)
240 elmapi 8459 . . . . . . . . . . . 12 (𝑏 ∈ (𝐵m (0...𝑠)) → 𝑏:(0...𝑠)⟶𝐵)
241240adantl 485 . . . . . . . . . . 11 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑏:(0...𝑠)⟶𝐵)
242241adantl 485 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑏:(0...𝑠)⟶𝐵)
243 0elfz 13095 . . . . . . . . . . . 12 (𝑠 ∈ ℕ0 → 0 ∈ (0...𝑠))
24432, 243syl 17 . . . . . . . . . . 11 (𝑠 ∈ ℕ → 0 ∈ (0...𝑠))
245244ad2antrl 728 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 0 ∈ (0...𝑠))
246242, 245ffvelrnd 6862 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑏‘0) ∈ 𝐵)
24724, 20, 21, 7, 8mat2pmatbas 21477 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌))
248237, 239, 246, 247syl3anc 1372 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌))
2491, 22ringcl 19433 . . . . . . . 8 ((𝑌 ∈ Ring ∧ (𝑇𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) → ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))
250235, 236, 248, 249syl3anc 1372 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))
2511, 2, 23, 3grpsubadd0sub 18304 . . . . . . 7 ((𝑌 ∈ Grp ∧ (((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌) ∧ ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) → ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) + ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
252233, 234, 250, 251syl3anc 1372 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) + ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
253228, 230, 2523eqtr4d 2783 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((0 (𝑇𝑀)) × (𝐺‘0)) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))) = ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
254187, 253oveq12d 7188 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (((0 (𝑇𝑀)) × (𝐺‘0)) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
255111, 254eqtrd 2773 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + ((0 (𝑇𝑀)) × (𝐺‘0))) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
25673, 100, 2553eqtrd 2777 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
25738, 71, 2563eqtrd 2777 1 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 846  w3a 1088   = wceq 1542  wcel 2114  wne 2934  Vcvv 3398  cun 3841  cin 3842  c0 4211  ifcif 4414  {csn 4516   class class class wbr 5030  cmpt 5110  wf 6335  cfv 6339  (class class class)co 7170  m cmap 8437  Fincfn 8555  cc 10613  cr 10614  0cc0 10615  1c1 10616   + caddc 10618   < clt 10753  cle 10754  cmin 10948  cn 11716  2c2 11771  0cn0 11976  cz 12062  cuz 12324  ...cfz 12981  Basecbs 16586  +gcplusg 16668  .rcmulr 16669  0gc0g 16816   Σg cgsu 16817  Mndcmnd 18027  Grpcgrp 18219  -gcsg 18221  .gcmg 18342  CMndccmn 19024  mulGrpcmgp 19358  1rcur 19370  Ringcrg 19416  CRingccrg 19417  Poly1cpl1 20952   Mat cmat 21158   matToPolyMat cmat2pmat 21455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-cnex 10671  ax-resscn 10672  ax-1cn 10673  ax-icn 10674  ax-addcl 10675  ax-addrcl 10676  ax-mulcl 10677  ax-mulrcl 10678  ax-mulcom 10679  ax-addass 10680  ax-mulass 10681  ax-distr 10682  ax-i2m1 10683  ax-1ne0 10684  ax-1rid 10685  ax-rnegex 10686  ax-rrecex 10687  ax-cnre 10688  ax-pre-lttri 10689  ax-pre-lttrn 10690  ax-pre-ltadd 10691  ax-pre-mulgt0 10692
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-ot 4525  df-uni 4797  df-int 4837  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-se 5484  df-we 5485  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 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-of 7425  df-ofr 7426  df-om 7600  df-1st 7714  df-2nd 7715  df-supp 7857  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-1o 8131  df-er 8320  df-map 8439  df-pm 8440  df-ixp 8508  df-en 8556  df-dom 8557  df-sdom 8558  df-fin 8559  df-fsupp 8907  df-sup 8979  df-oi 9047  df-card 9441  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-sub 10950  df-neg 10951  df-nn 11717  df-2 11779  df-3 11780  df-4 11781  df-5 11782  df-6 11783  df-7 11784  df-8 11785  df-9 11786  df-n0 11977  df-z 12063  df-dec 12180  df-uz 12325  df-rp 12473  df-fz 12982  df-fzo 13125  df-seq 13461  df-hash 13783  df-struct 16588  df-ndx 16589  df-slot 16590  df-base 16592  df-sets 16593  df-ress 16594  df-plusg 16681  df-mulr 16682  df-sca 16684  df-vsca 16685  df-ip 16686  df-tset 16687  df-ple 16688  df-ds 16690  df-hom 16692  df-cco 16693  df-0g 16818  df-gsum 16819  df-prds 16824  df-pws 16826  df-mre 16960  df-mrc 16961  df-acs 16963  df-mgm 17968  df-sgrp 18017  df-mnd 18028  df-mhm 18072  df-submnd 18073  df-grp 18222  df-minusg 18223  df-sbg 18224  df-mulg 18343  df-subg 18394  df-ghm 18474  df-cntz 18565  df-cmn 19026  df-abl 19027  df-mgp 19359  df-ur 19371  df-ring 19418  df-cring 19419  df-subrg 19652  df-lmod 19755  df-lss 19823  df-sra 20063  df-rgmod 20064  df-dsmm 20548  df-frlm 20563  df-ascl 20671  df-psr 20722  df-mpl 20724  df-opsr 20726  df-psr1 20955  df-ply1 20957  df-mamu 21137  df-mat 21159  df-mat2pmat 21458
This theorem is referenced by:  chfacfpmmulgsum2  21616
  Copyright terms: Public domain W3C validator