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

Theorem chfacfpmmulgsum 22886
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 2735 . . 3 (Base‘𝑌) = (Base‘𝑌)
2 cayhamlem1.0 . . 3 0 = (0g𝑌)
3 chfacfpmmulgsum.p . . 3 + = (+g𝑌)
4 crngring 20263 . . . . . . . 8 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
54anim2i 617 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
653adant3 1131 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
7 cayhamlem1.p . . . . . . 7 𝑃 = (Poly1𝑅)
8 cayhamlem1.y . . . . . . 7 𝑌 = (𝑁 Mat 𝑃)
97, 8pmatring 22714 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
106, 9syl 17 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Ring)
11 ringcmn 20296 . . . . 5 (𝑌 ∈ Ring → 𝑌 ∈ CMnd)
1210, 11syl 17 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ CMnd)
1312adantr 480 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ CMnd)
14 nn0ex 12530 . . . 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 484 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
1916, 17, 183jca 1127 . . . 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 22883 . . . 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 22885 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))) finSupp 0 )
30 nn0disj 13681 . . . 4 ((0...(𝑠 + 1)) ∩ (ℤ‘((𝑠 + 1) + 1))) = ∅
3130a1i 11 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0...(𝑠 + 1)) ∩ (ℤ‘((𝑠 + 1) + 1))) = ∅)
32 nnnn0 12531 . . . . . 6 (𝑠 ∈ ℕ → 𝑠 ∈ ℕ0)
33 peano2nn0 12564 . . . . . 6 (𝑠 ∈ ℕ0 → (𝑠 + 1) ∈ ℕ0)
3432, 33syl 17 . . . . 5 (𝑠 ∈ ℕ → (𝑠 + 1) ∈ ℕ0)
35 nn0split 13680 . . . . 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 19962 . 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 12272 . . . . . . . . . . . . 13 (𝑠 ∈ ℕ → 𝑠 ∈ ℂ)
42 add1p1 12515 . . . . . . . . . . . . 13 (𝑠 ∈ ℂ → ((𝑠 + 1) + 1) = (𝑠 + 2))
4341, 42syl 17 . . . . . . . . . . . 12 (𝑠 ∈ ℕ → ((𝑠 + 1) + 1) = (𝑠 + 2))
4443ad2antrl 728 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑠 + 1) + 1) = (𝑠 + 2))
4544fveq2d 6911 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (ℤ‘((𝑠 + 1) + 1)) = (ℤ‘(𝑠 + 2)))
4645eleq2d 2825 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↔ 𝑖 ∈ (ℤ‘(𝑠 + 2))))
4746biimpa 476 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ‘((𝑠 + 1) + 1))) → 𝑖 ∈ (ℤ‘(𝑠 + 2)))
4820, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmul0 22884 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑖 ∈ (ℤ‘(𝑠 + 2))) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) = 0 )
4939, 40, 47, 48syl3anc 1370 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ‘((𝑠 + 1) + 1))) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) = 0 )
5049mpteq2dva 5248 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))) = (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ 0 ))
5150oveq2d 7447 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = (𝑌 Σg (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ 0 )))
524, 9sylan2 593 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ Ring)
53 ringmnd 20261 . . . . . . . . . 10 (𝑌 ∈ Ring → 𝑌 ∈ Mnd)
5452, 53syl 17 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ Mnd)
55543adant3 1131 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Mnd)
56 fvex 6920 . . . . . . . 8 (ℤ‘((𝑠 + 1) + 1)) ∈ V
5755, 56jctir 520 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑌 ∈ Mnd ∧ (ℤ‘((𝑠 + 1) + 1)) ∈ V))
5857adantr 480 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 ∈ Mnd ∧ (ℤ‘((𝑠 + 1) + 1)) ∈ V))
592gsumz 18862 . . . . . 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 2775 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = 0 )
6261oveq2d 7447 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (𝑌 Σg (𝑖 ∈ (ℤ‘((𝑠 + 1) + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + 0 ))
63 fzfid 14011 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (0...(𝑠 + 1)) ∈ Fin)
64 elfznn0 13657 . . . . . . . 8 (𝑖 ∈ (0...(𝑠 + 1)) → 𝑖 ∈ ℕ0)
6564, 19sylan2 593 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 + 1))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑖 ∈ ℕ0))
6665, 27syl 17 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 + 1))) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) ∈ (Base‘𝑌))
6766ralrimiva 3144 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ∀𝑖 ∈ (0...(𝑠 + 1))((𝑖 (𝑇𝑀)) × (𝐺𝑖)) ∈ (Base‘𝑌))
681, 13, 63, 67gsummptcl 20000 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) ∈ (Base‘𝑌))
691, 3, 2mndrid 18781 . . . 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 2775 . 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 19965 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))))))
74 elfznn0 13657 . . . . . . 7 (𝑖 ∈ (0...𝑠) → 𝑖 ∈ ℕ0)
7574, 28sylan2 593 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) ∈ (Base‘𝑌))
761, 3, 13, 72, 75gsummptfzsplitl 19966 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))))))
7755adantr 480 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ Mnd)
78 0nn0 12539 . . . . . . . 8 0 ∈ ℕ0
7978a1i 11 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 0 ∈ ℕ0)
8020, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 22883 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 0 ∈ ℕ0) → ((0 (𝑇𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌))
8179, 80mpd3an3 1461 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0 (𝑇𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌))
82 oveq1 7438 . . . . . . . . 9 (𝑖 = 0 → (𝑖 (𝑇𝑀)) = (0 (𝑇𝑀)))
83 fveq2 6907 . . . . . . . . 9 (𝑖 = 0 → (𝐺𝑖) = (𝐺‘0))
8482, 83oveq12d 7449 . . . . . . . 8 (𝑖 = 0 → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) = ((0 (𝑇𝑀)) × (𝐺‘0)))
851, 84gsumsn 19987 . . . . . . 7 ((𝑌 ∈ Mnd ∧ 0 ∈ ℕ0 ∧ ((0 (𝑇𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌)) → (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((0 (𝑇𝑀)) × (𝐺‘0)))
8677, 79, 81, 85syl3anc 1370 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((0 (𝑇𝑀)) × (𝐺‘0)))
8786oveq2d 7447 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + ((0 (𝑇𝑀)) × (𝐺‘0))))
8876, 87eqtrd 2775 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + ((0 (𝑇𝑀)) × (𝐺‘0))))
89 ovexd 7466 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑠 + 1) ∈ V)
90 1nn0 12540 . . . . . . . 8 1 ∈ ℕ0
9190a1i 11 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 1 ∈ ℕ0)
9272, 91nn0addcld 12589 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑠 + 1) ∈ ℕ0)
9320, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 22883 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ (𝑠 + 1) ∈ ℕ0) → (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌))
9492, 93mpd3an3 1461 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌))
95 oveq1 7438 . . . . . . 7 (𝑖 = (𝑠 + 1) → (𝑖 (𝑇𝑀)) = ((𝑠 + 1) (𝑇𝑀)))
96 fveq2 6907 . . . . . . 7 (𝑖 = (𝑠 + 1) → (𝐺𝑖) = (𝐺‘(𝑠 + 1)))
9795, 96oveq12d 7449 . . . . . 6 (𝑖 = (𝑠 + 1) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) = (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))))
981, 97gsumsn 19987 . . . . 5 ((𝑌 ∈ Mnd ∧ (𝑠 + 1) ∈ V ∧ (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌)) → (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))))
9977, 89, 94, 98syl3anc 1370 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))))
10088, 99oveq12d 7449 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))))) = (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + ((0 (𝑇𝑀)) × (𝐺‘0))) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))))
101 fzfid 14011 . . . . . 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 13590 . . . . . . . . . 10 (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℕ)
105104nnnn0d 12585 . . . . . . . . 9 (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℕ0)
106105adantl 481 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 ∈ ℕ0)
107102, 103, 106, 27syl3anc 1370 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) ∈ (Base‘𝑌))
108107ralrimiva 3144 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ∀𝑖 ∈ (1...𝑠)((𝑖 (𝑇𝑀)) × (𝐺𝑖)) ∈ (Base‘𝑌))
1091, 13, 101, 108gsummptcl 20000 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) ∈ (Base‘𝑌))
1101, 3mndass 18769 . . . . 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 1371 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + ((0 (𝑇𝑀)) × (𝐺‘0))) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (((0 (𝑇𝑀)) × (𝐺‘0)) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))))))
112104nnne0d 12314 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑠) → 𝑖 ≠ 0)
113112ad2antlr 727 . . . . . . . . . . . . 13 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑖 ≠ 0)
114 neeq1 3001 . . . . . . . . . . . . . 14 (𝑛 = 𝑖 → (𝑛 ≠ 0 ↔ 𝑖 ≠ 0))
115114adantl 481 . . . . . . . . . . . . 13 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑛 ≠ 0 ↔ 𝑖 ≠ 0))
116113, 115mpbird 257 . . . . . . . . . . . 12 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 ≠ 0)
117 eqneqall 2949 . . . . . . . . . . . 12 (𝑛 = 0 → (𝑛 ≠ 0 → 0 = (𝑇‘(𝑏‘(𝑖 − 1)))))
118116, 117mpan9 506 . . . . . . . . . . 11 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → 0 = (𝑇‘(𝑏‘(𝑖 − 1))))
119 simplr 769 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → 𝑛 = 𝑖)
120 eqeq1 2739 . . . . . . . . . . . . . . . . 17 (0 = 𝑛 → (0 = 𝑖𝑛 = 𝑖))
121120eqcoms 2743 . . . . . . . . . . . . . . . 16 (𝑛 = 0 → (0 = 𝑖𝑛 = 𝑖))
122121adantl 481 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → (0 = 𝑖𝑛 = 𝑖))
123119, 122mpbird 257 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → 0 = 𝑖)
124123fveq2d 6911 . . . . . . . . . . . . 13 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → (𝑏‘0) = (𝑏𝑖))
125124fveq2d 6911 . . . . . . . . . . . 12 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → (𝑇‘(𝑏‘0)) = (𝑇‘(𝑏𝑖)))
126125oveq2d 7447 . . . . . . . . . . 11 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → ((𝑇𝑀) × (𝑇‘(𝑏‘0))) = ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))
127118, 126oveq12d 7449 . . . . . . . . . 10 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
128 elfz2 13551 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑠) ↔ ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (1 ≤ 𝑖𝑖𝑠)))
129 zleltp1 12666 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑖𝑠𝑖 < (𝑠 + 1)))
130129ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖𝑠𝑖 < (𝑠 + 1)))
1311303adant1 1129 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖𝑠𝑖 < (𝑠 + 1)))
132131biimpcd 249 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖𝑠 → ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → 𝑖 < (𝑠 + 1)))
133132adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((1 ≤ 𝑖𝑖𝑠) → ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → 𝑖 < (𝑠 + 1)))
134133impcom 407 . . . . . . . . . . . . . . . . . . . 20 (((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (1 ≤ 𝑖𝑖𝑠)) → 𝑖 < (𝑠 + 1))
135134orcd 873 . . . . . . . . . . . . . . . . . . 19 (((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (1 ≤ 𝑖𝑖𝑠)) → (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖))
136 zre 12615 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ℤ → 𝑠 ∈ ℝ)
137 1red 11260 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ℤ → 1 ∈ ℝ)
138136, 137readdcld 11288 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ℤ → (𝑠 + 1) ∈ ℝ)
139 zre 12615 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ℤ → 𝑖 ∈ ℝ)
140138, 139anim12ci 614 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ ℝ ∧ (𝑠 + 1) ∈ ℝ))
1411403adant1 1129 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ ℝ ∧ (𝑠 + 1) ∈ ℝ))
142 lttri2 11341 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ ℝ ∧ (𝑠 + 1) ∈ ℝ) → (𝑖 ≠ (𝑠 + 1) ↔ (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖)))
143141, 142syl 17 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ≠ (𝑠 + 1) ↔ (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖)))
144143adantr 480 . . . . . . . . . . . . . . . . . . 19 (((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (1 ≤ 𝑖𝑖𝑠)) → (𝑖 ≠ (𝑠 + 1) ↔ (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖)))
145135, 144mpbird 257 . . . . . . . . . . . . . . . . . 18 (((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (1 ≤ 𝑖𝑖𝑠)) → 𝑖 ≠ (𝑠 + 1))
146128, 145sylbi 217 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑠) → 𝑖 ≠ (𝑠 + 1))
147146ad2antlr 727 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑖 ≠ (𝑠 + 1))
148 neeq1 3001 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → (𝑛 ≠ (𝑠 + 1) ↔ 𝑖 ≠ (𝑠 + 1)))
149148adantl 481 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑛 ≠ (𝑠 + 1) ↔ 𝑖 ≠ (𝑠 + 1)))
150147, 149mpbird 257 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 ≠ (𝑠 + 1))
151150adantr 480 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → 𝑛 ≠ (𝑠 + 1))
152151neneqd 2943 . . . . . . . . . . . . 13 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → ¬ 𝑛 = (𝑠 + 1))
153152pm2.21d 121 . . . . . . . . . . . 12 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → (𝑛 = (𝑠 + 1) → (𝑇‘(𝑏𝑠)) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))
154153imp 406 . . . . . . . . . . 11 (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ 𝑛 = (𝑠 + 1)) → (𝑇‘(𝑏𝑠)) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
155104nnred 12279 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℝ)
156 eleq1w 2822 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → (𝑛 ∈ ℝ ↔ 𝑖 ∈ ℝ))
157155, 156syl5ibrcom 247 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑠) → (𝑛 = 𝑖𝑛 ∈ ℝ))
158157adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑛 = 𝑖𝑛 ∈ ℝ))
159158imp 406 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 ∈ ℝ)
16072nn0red 12586 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑠 ∈ ℝ)
161160ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑠 ∈ ℝ)
162 1red 11260 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 1 ∈ ℝ)
163161, 162readdcld 11288 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑠 + 1) ∈ ℝ)
164128, 134sylbi 217 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑠) → 𝑖 < (𝑠 + 1))
165164ad2antlr 727 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑖 < (𝑠 + 1))
166 breq1 5151 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (𝑛 < (𝑠 + 1) ↔ 𝑖 < (𝑠 + 1)))
167166adantl 481 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑛 < (𝑠 + 1) ↔ 𝑖 < (𝑠 + 1)))
168165, 167mpbird 257 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 < (𝑠 + 1))
169159, 163, 168ltnsymd 11408 . . . . . . . . . . . . . . 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 406 . . . . . . . . . . . 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 7453 . . . . . . . . . . . . . 14 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑏‘(𝑛 − 1)) = (𝑏‘(𝑖 − 1)))
175174fveq2d 6911 . . . . . . . . . . . . 13 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑇‘(𝑏‘(𝑛 − 1))) = (𝑇‘(𝑏‘(𝑖 − 1))))
176173fveq2d 6911 . . . . . . . . . . . . . . 15 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑏𝑛) = (𝑏𝑖))
177176fveq2d 6911 . . . . . . . . . . . . . 14 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑇‘(𝑏𝑛)) = (𝑇‘(𝑏𝑖)))
178177oveq2d 7447 . . . . . . . . . . . . 13 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇𝑀) × (𝑇‘(𝑏𝑛))) = ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))
179175, 178oveq12d 7449 . . . . . . . . . . . 12 ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛)))) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
180172, 179ifeqda 4567 . . . . . . . . . . 11 (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) → if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
181154, 180ifeqda 4567 . . . . . . . . . 10 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛)))))) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
182127, 181ifeqda 4567 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
183 ovexd 7466 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))) ∈ V)
18425, 182, 106, 183fvmptd2 7024 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝐺𝑖) = ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))
185184oveq2d 7447 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 (𝑇𝑀)) × (𝐺𝑖)) = ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))
186185mpteq2dva 5248 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖)))))))
187186oveq2d 7447 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))))
188 nn0p1gt0 12553 . . . . . . . . . . . . . 14 (𝑠 ∈ ℕ0 → 0 < (𝑠 + 1))
189 0red 11262 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ℕ0 → 0 ∈ ℝ)
190 ltne 11356 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ 0 < (𝑠 + 1)) → (𝑠 + 1) ≠ 0)
191189, 190sylan 580 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℕ0 ∧ 0 < (𝑠 + 1)) → (𝑠 + 1) ≠ 0)
192 neeq1 3001 . . . . . . . . . . . . . . 15 (𝑛 = (𝑠 + 1) → (𝑛 ≠ 0 ↔ (𝑠 + 1) ≠ 0))
193191, 192syl5ibrcom 247 . . . . . . . . . . . . . 14 ((𝑠 ∈ ℕ0 ∧ 0 < (𝑠 + 1)) → (𝑛 = (𝑠 + 1) → 𝑛 ≠ 0))
19432, 188, 193syl2anc2 585 . . . . . . . . . . . . 13 (𝑠 ∈ ℕ → (𝑛 = (𝑠 + 1) → 𝑛 ≠ 0))
195194ad2antrl 728 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑛 = (𝑠 + 1) → 𝑛 ≠ 0))
196195imp 406 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) → 𝑛 ≠ 0)
197 eqneqall 2949 . . . . . . . . . . 11 (𝑛 = 0 → (𝑛 ≠ 0 → ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = (𝑇‘(𝑏𝑠))))
198196, 197mpan9 506 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) ∧ 𝑛 = 0) → ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = (𝑇‘(𝑏𝑠)))
199 iftrue 4537 . . . . . . . . . . 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 4567 . . . . . . . . 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 6922 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑇‘(𝑏𝑠)) ∈ V)
20425, 201, 202, 203fvmptd2 7024 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝐺‘(𝑠 + 1)) = (𝑇‘(𝑏𝑠)))
205204oveq2d 7447 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) = (((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))))
20624, 20, 21, 7, 8mat2pmatbas 22748 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
2074, 206syl3an2 1163 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
208 eqid 2735 . . . . . . . . . . . . . 14 (mulGrp‘𝑌) = (mulGrp‘𝑌)
209208, 1mgpbas 20158 . . . . . . . . . . . . 13 (Base‘𝑌) = (Base‘(mulGrp‘𝑌))
210 eqid 2735 . . . . . . . . . . . . 13 (0g‘(mulGrp‘𝑌)) = (0g‘(mulGrp‘𝑌))
211209, 210, 26mulg0 19105 . . . . . . . . . . . 12 ((𝑇𝑀) ∈ (Base‘𝑌) → (0 (𝑇𝑀)) = (0g‘(mulGrp‘𝑌)))
212207, 211syl 17 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (0 (𝑇𝑀)) = (0g‘(mulGrp‘𝑌)))
213 eqid 2735 . . . . . . . . . . . 12 (1r𝑌) = (1r𝑌)
214208, 213ringidval 20201 . . . . . . . . . . 11 (1r𝑌) = (0g‘(mulGrp‘𝑌))
215212, 214eqtr4di 2793 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (0 (𝑇𝑀)) = (1r𝑌))
216215adantr 480 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (0 (𝑇𝑀)) = (1r𝑌))
217216oveq1d 7446 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0 (𝑇𝑀)) × (𝐺‘0)) = ((1r𝑌) × (𝐺‘0)))
218523adant3 1131 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Ring)
21920, 21, 7, 8, 22, 23, 2, 24, 25chfacfisf 22876 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌))
2204, 219syl3anl2 1412 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌))
221220, 79ffvelcdmd 7105 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝐺‘0) ∈ (Base‘𝑌))
2221, 22, 213ringlidm 20283 . . . . . . . . 9 ((𝑌 ∈ Ring ∧ (𝐺‘0) ∈ (Base‘𝑌)) → ((1r𝑌) × (𝐺‘0)) = (𝐺‘0))
223218, 221, 222syl2an2r 685 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((1r𝑌) × (𝐺‘0)) = (𝐺‘0))
224 iftrue 4537 . . . . . . . . 9 (𝑛 = 0 → if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))) = ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
225 ovexd 7466 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) ∈ V)
22625, 224, 79, 225fvmptd3 7039 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝐺‘0) = ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
227217, 223, 2263eqtrd 2779 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((0 (𝑇𝑀)) × (𝐺‘0)) = ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
228205, 227oveq12d 7449 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) + ((0 (𝑇𝑀)) × (𝐺‘0))) = ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) + ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
2291, 3cmncom 19831 . . . . . . 7 ((𝑌 ∈ CMnd ∧ ((0 (𝑇𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌) ∧ (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌)) → (((0 (𝑇𝑀)) × (𝐺‘0)) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))) = ((((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) + ((0 (𝑇𝑀)) × (𝐺‘0))))
23013, 81, 94, 229syl3anc 1370 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((0 (𝑇𝑀)) × (𝐺‘0)) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))) = ((((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))) + ((0 (𝑇𝑀)) × (𝐺‘0))))
231 ringgrp 20256 . . . . . . . . 9 (𝑌 ∈ Ring → 𝑌 ∈ Grp)
23210, 231syl 17 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Grp)
233232adantr 480 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ Grp)
234205, 94eqeltrrd 2840 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌))
23510adantr 480 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑌 ∈ Ring)
236207adantr 480 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑇𝑀) ∈ (Base‘𝑌))
237 simpl1 1190 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑁 ∈ Fin)
23843ad2ant2 1133 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑅 ∈ Ring)
239238adantr 480 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑅 ∈ Ring)
240 elmapi 8888 . . . . . . . . . . . 12 (𝑏 ∈ (𝐵m (0...𝑠)) → 𝑏:(0...𝑠)⟶𝐵)
241240adantl 481 . . . . . . . . . . 11 ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑏:(0...𝑠)⟶𝐵)
242241adantl 481 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝑏:(0...𝑠)⟶𝐵)
243 0elfz 13661 . . . . . . . . . . . 12 (𝑠 ∈ ℕ0 → 0 ∈ (0...𝑠))
24432, 243syl 17 . . . . . . . . . . 11 (𝑠 ∈ ℕ → 0 ∈ (0...𝑠))
245244ad2antrl 728 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 0 ∈ (0...𝑠))
246242, 245ffvelcdmd 7105 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑏‘0) ∈ 𝐵)
24724, 20, 21, 7, 8mat2pmatbas 22748 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌))
248237, 239, 246, 247syl3anc 1370 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌))
2491, 22ringcl 20268 . . . . . . . 8 ((𝑌 ∈ Ring ∧ (𝑇𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) → ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))
250235, 236, 248, 249syl3anc 1370 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))
2511, 2, 23, 3grpsubadd0sub 19058 . . . . . . 7 ((𝑌 ∈ Grp ∧ (((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ∈ (Base‘𝑌) ∧ ((𝑇𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) → ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) + ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
252233, 234, 250, 251syl3anc 1370 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))) = ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) + ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
253228, 230, 2523eqtr4d 2785 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((0 (𝑇𝑀)) × (𝐺‘0)) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))) = ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))
254187, 253oveq12d 7449 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + (((0 (𝑇𝑀)) × (𝐺‘0)) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
255111, 254eqtrd 2775 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) + ((0 (𝑇𝑀)) × (𝐺‘0))) + (((𝑠 + 1) (𝑇𝑀)) × (𝐺‘(𝑠 + 1)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
25673, 100, 2553eqtrd 2779 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 (𝑇𝑀)) × (𝐺𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 (𝑇𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) (𝑇𝑀)) × (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
25738, 71, 2563eqtrd 2779 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 206  wa 395  wo 847  w3a 1086   = wceq 1537  wcel 2106  wne 2938  Vcvv 3478  cun 3961  cin 3962  c0 4339  ifcif 4531  {csn 4631   class class class wbr 5148  cmpt 5231  wf 6559  cfv 6563  (class class class)co 7431  m cmap 8865  Fincfn 8984  cc 11151  cr 11152  0cc0 11153  1c1 11154   + caddc 11156   < clt 11293  cle 11294  cmin 11490  cn 12264  2c2 12319  0cn0 12524  cz 12611  cuz 12876  ...cfz 13544  Basecbs 17245  +gcplusg 17298  .rcmulr 17299  0gc0g 17486   Σg cgsu 17487  Mndcmnd 18760  Grpcgrp 18964  -gcsg 18966  .gcmg 19098  CMndccmn 19813  mulGrpcmgp 20152  1rcur 20199  Ringcrg 20251  CRingccrg 20252  Poly1cpl1 22194   Mat cmat 22427   matToPolyMat cmat2pmat 22726
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-ot 4640  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-ofr 7698  df-om 7888  df-1st 8013  df-2nd 8014  df-supp 8185  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-er 8744  df-map 8867  df-pm 8868  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9400  df-sup 9480  df-oi 9548  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12612  df-dec 12732  df-uz 12877  df-rp 13033  df-fz 13545  df-fzo 13692  df-seq 14040  df-hash 14367  df-struct 17181  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-mulr 17312  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-hom 17322  df-cco 17323  df-0g 17488  df-gsum 17489  df-prds 17494  df-pws 17496  df-mre 17631  df-mrc 17632  df-acs 17634  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-mhm 18809  df-submnd 18810  df-grp 18967  df-minusg 18968  df-sbg 18969  df-mulg 19099  df-subg 19154  df-ghm 19244  df-cntz 19348  df-cmn 19815  df-abl 19816  df-mgp 20153  df-rng 20171  df-ur 20200  df-ring 20253  df-cring 20254  df-subrng 20563  df-subrg 20587  df-lmod 20877  df-lss 20948  df-sra 21190  df-rgmod 21191  df-dsmm 21770  df-frlm 21785  df-ascl 21893  df-psr 21947  df-mpl 21949  df-opsr 21951  df-psr1 22197  df-ply1 22199  df-mamu 22411  df-mat 22428  df-mat2pmat 22729
This theorem is referenced by:  chfacfpmmulgsum2  22887
  Copyright terms: Public domain W3C validator