This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsummulsubdishift2

Description: Distribute a subtraction over an indexed sum, shift one of the resulting sums, and regroup terms. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses gsummulsubdishift.b 
|- B = ( Base ` R )
gsummulsubdishift.p 
|- .+ = ( +g ` R )
gsummulsubdishift.m 
|- .- = ( -g ` R )
gsummulsubdishift.t 
|- .x. = ( .r ` R )
gsummulsubdishift.r 
|- ( ph -> R e. Ring )
gsummulsubdishift.a 
|- ( ph -> A e. B )
gsummulsubdishift.c 
|- ( ph -> C e. B )
gsummulsubdishift.n 
|- ( ph -> N e. NN0 )
gsummulsubdishift.d 
|- ( ph -> D : ( 0 ... N ) --> B )
gsummulsubdishift2.e 
|- ( ph -> E = ( ( ( D ` 0 ) .x. A ) .- ( ( D ` N ) .x. C ) ) )
gsummulsubdishift2.f 
|- ( ( ph /\ k e. ( 0 ..^ N ) ) -> F = ( ( ( D ` ( k + 1 ) ) .x. A ) .- ( ( D ` k ) .x. C ) ) )
Assertion gsummulsubdishift2 
|- ( ph -> ( ( R gsum D ) .x. ( A .- C ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) .+ E ) )

Proof

Step Hyp Ref Expression
1 gsummulsubdishift.b 
 |-  B = ( Base ` R )
2 gsummulsubdishift.p 
 |-  .+ = ( +g ` R )
3 gsummulsubdishift.m 
 |-  .- = ( -g ` R )
4 gsummulsubdishift.t 
 |-  .x. = ( .r ` R )
5 gsummulsubdishift.r 
 |-  ( ph -> R e. Ring )
6 gsummulsubdishift.a 
 |-  ( ph -> A e. B )
7 gsummulsubdishift.c 
 |-  ( ph -> C e. B )
8 gsummulsubdishift.n 
 |-  ( ph -> N e. NN0 )
9 gsummulsubdishift.d 
 |-  ( ph -> D : ( 0 ... N ) --> B )
10 gsummulsubdishift2.e 
 |-  ( ph -> E = ( ( ( D ` 0 ) .x. A ) .- ( ( D ` N ) .x. C ) ) )
11 gsummulsubdishift2.f 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> F = ( ( ( D ` ( k + 1 ) ) .x. A ) .- ( ( D ` k ) .x. C ) ) )
12 eqid 
 |-  ( invg ` R ) = ( invg ` R )
13 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
14 5 ringcmnd 
 |-  ( ph -> R e. CMnd )
15 ovexd 
 |-  ( ph -> ( 0 ... N ) e. _V )
16 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
17 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
18 9 16 17 fdmfifsupp 
 |-  ( ph -> D finSupp ( 0g ` R ) )
19 1 13 14 15 9 18 gsumcl 
 |-  ( ph -> ( R gsum D ) e. B )
20 5 ringgrpd 
 |-  ( ph -> R e. Grp )
21 1 3 20 7 6 grpsubcld 
 |-  ( ph -> ( C .- A ) e. B )
22 1 4 12 5 19 21 ringmneg2 
 |-  ( ph -> ( ( R gsum D ) .x. ( ( invg ` R ) ` ( C .- A ) ) ) = ( ( invg ` R ) ` ( ( R gsum D ) .x. ( C .- A ) ) ) )
23 1 3 12 grpinvsub 
 |-  ( ( R e. Grp /\ C e. B /\ A e. B ) -> ( ( invg ` R ) ` ( C .- A ) ) = ( A .- C ) )
24 20 7 6 23 syl3anc 
 |-  ( ph -> ( ( invg ` R ) ` ( C .- A ) ) = ( A .- C ) )
25 24 oveq2d 
 |-  ( ph -> ( ( R gsum D ) .x. ( ( invg ` R ) ` ( C .- A ) ) ) = ( ( R gsum D ) .x. ( A .- C ) ) )
26 10 fveq2d 
 |-  ( ph -> ( ( invg ` R ) ` E ) = ( ( invg ` R ) ` ( ( ( D ` 0 ) .x. A ) .- ( ( D ` N ) .x. C ) ) ) )
27 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
28 8 27 syl 
 |-  ( ph -> 0 e. ( 0 ... N ) )
29 9 28 ffvelcdmd 
 |-  ( ph -> ( D ` 0 ) e. B )
30 1 4 5 29 6 ringcld 
 |-  ( ph -> ( ( D ` 0 ) .x. A ) e. B )
31 nn0fz0 
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
32 8 31 sylib 
 |-  ( ph -> N e. ( 0 ... N ) )
33 9 32 ffvelcdmd 
 |-  ( ph -> ( D ` N ) e. B )
34 1 4 5 33 7 ringcld 
 |-  ( ph -> ( ( D ` N ) .x. C ) e. B )
35 1 3 12 grpinvsub 
 |-  ( ( R e. Grp /\ ( ( D ` 0 ) .x. A ) e. B /\ ( ( D ` N ) .x. C ) e. B ) -> ( ( invg ` R ) ` ( ( ( D ` 0 ) .x. A ) .- ( ( D ` N ) .x. C ) ) ) = ( ( ( D ` N ) .x. C ) .- ( ( D ` 0 ) .x. A ) ) )
36 20 30 34 35 syl3anc 
 |-  ( ph -> ( ( invg ` R ) ` ( ( ( D ` 0 ) .x. A ) .- ( ( D ` N ) .x. C ) ) ) = ( ( ( D ` N ) .x. C ) .- ( ( D ` 0 ) .x. A ) ) )
37 26 36 eqtrd 
 |-  ( ph -> ( ( invg ` R ) ` E ) = ( ( ( D ` N ) .x. C ) .- ( ( D ` 0 ) .x. A ) ) )
38 11 fveq2d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( invg ` R ) ` F ) = ( ( invg ` R ) ` ( ( ( D ` ( k + 1 ) ) .x. A ) .- ( ( D ` k ) .x. C ) ) ) )
39 20 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> R e. Grp )
40 5 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> R e. Ring )
41 9 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> D : ( 0 ... N ) --> B )
42 fzofzp1 
 |-  ( k e. ( 0 ..^ N ) -> ( k + 1 ) e. ( 0 ... N ) )
43 42 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k + 1 ) e. ( 0 ... N ) )
44 41 43 ffvelcdmd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( D ` ( k + 1 ) ) e. B )
45 6 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> A e. B )
46 1 4 40 44 45 ringcld 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( D ` ( k + 1 ) ) .x. A ) e. B )
47 fzossfz 
 |-  ( 0 ..^ N ) C_ ( 0 ... N )
48 simpr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. ( 0 ..^ N ) )
49 47 48 sselid 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. ( 0 ... N ) )
50 41 49 ffvelcdmd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( D ` k ) e. B )
51 7 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> C e. B )
52 1 4 40 50 51 ringcld 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( D ` k ) .x. C ) e. B )
53 1 3 12 grpinvsub 
 |-  ( ( R e. Grp /\ ( ( D ` ( k + 1 ) ) .x. A ) e. B /\ ( ( D ` k ) .x. C ) e. B ) -> ( ( invg ` R ) ` ( ( ( D ` ( k + 1 ) ) .x. A ) .- ( ( D ` k ) .x. C ) ) ) = ( ( ( D ` k ) .x. C ) .- ( ( D ` ( k + 1 ) ) .x. A ) ) )
54 39 46 52 53 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( invg ` R ) ` ( ( ( D ` ( k + 1 ) ) .x. A ) .- ( ( D ` k ) .x. C ) ) ) = ( ( ( D ` k ) .x. C ) .- ( ( D ` ( k + 1 ) ) .x. A ) ) )
55 38 54 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( invg ` R ) ` F ) = ( ( ( D ` k ) .x. C ) .- ( ( D ` ( k + 1 ) ) .x. A ) ) )
56 1 2 3 4 5 7 6 8 9 37 55 gsummulsubdishift1 
 |-  ( ph -> ( ( R gsum D ) .x. ( C .- A ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) .+ ( ( invg ` R ) ` E ) ) )
57 56 fveq2d 
 |-  ( ph -> ( ( invg ` R ) ` ( ( R gsum D ) .x. ( C .- A ) ) ) = ( ( invg ` R ) ` ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) .+ ( ( invg ` R ) ` E ) ) ) )
58 5 ringabld 
 |-  ( ph -> R e. Abel )
59 fzofi 
 |-  ( 0 ..^ N ) e. Fin
60 59 a1i 
 |-  ( ph -> ( 0 ..^ N ) e. Fin )
61 1 3 39 46 52 grpsubcld 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( ( D ` ( k + 1 ) ) .x. A ) .- ( ( D ` k ) .x. C ) ) e. B )
62 11 61 eqeltrd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> F e. B )
63 1 12 39 62 grpinvcld 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( invg ` R ) ` F ) e. B )
64 63 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ..^ N ) ( ( invg ` R ) ` F ) e. B )
65 1 14 60 64 gsummptcl 
 |-  ( ph -> ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) e. B )
66 1 3 20 30 34 grpsubcld 
 |-  ( ph -> ( ( ( D ` 0 ) .x. A ) .- ( ( D ` N ) .x. C ) ) e. B )
67 10 66 eqeltrd 
 |-  ( ph -> E e. B )
68 1 12 20 67 grpinvcld 
 |-  ( ph -> ( ( invg ` R ) ` E ) e. B )
69 1 2 12 ablinvadd 
 |-  ( ( R e. Abel /\ ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) e. B /\ ( ( invg ` R ) ` E ) e. B ) -> ( ( invg ` R ) ` ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) .+ ( ( invg ` R ) ` E ) ) ) = ( ( ( invg ` R ) ` ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) ) .+ ( ( invg ` R ) ` ( ( invg ` R ) ` E ) ) ) )
70 58 65 68 69 syl3anc 
 |-  ( ph -> ( ( invg ` R ) ` ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) .+ ( ( invg ` R ) ` E ) ) ) = ( ( ( invg ` R ) ` ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) ) .+ ( ( invg ` R ) ` ( ( invg ` R ) ` E ) ) ) )
71 63 fmpttd 
 |-  ( ph -> ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) : ( 0 ..^ N ) --> B )
72 71 60 17 fidmfisupp 
 |-  ( ph -> ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) finSupp ( 0g ` R ) )
73 1 13 12 58 60 71 72 gsuminv 
 |-  ( ph -> ( R gsum ( ( invg ` R ) o. ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) ) = ( ( invg ` R ) ` ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) ) )
74 1 12 grpinvf 
 |-  ( R e. Grp -> ( invg ` R ) : B --> B )
75 20 74 syl 
 |-  ( ph -> ( invg ` R ) : B --> B )
76 75 63 cofmpt 
 |-  ( ph -> ( ( invg ` R ) o. ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) = ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` ( ( invg ` R ) ` F ) ) ) )
77 1 12 39 62 grpinvinvd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( invg ` R ) ` ( ( invg ` R ) ` F ) ) = F )
78 77 mpteq2dva 
 |-  ( ph -> ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` ( ( invg ` R ) ` F ) ) ) = ( k e. ( 0 ..^ N ) |-> F ) )
79 76 78 eqtrd 
 |-  ( ph -> ( ( invg ` R ) o. ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) = ( k e. ( 0 ..^ N ) |-> F ) )
80 79 oveq2d 
 |-  ( ph -> ( R gsum ( ( invg ` R ) o. ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) ) = ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) )
81 73 80 eqtr3d 
 |-  ( ph -> ( ( invg ` R ) ` ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) ) = ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) )
82 1 12 20 67 grpinvinvd 
 |-  ( ph -> ( ( invg ` R ) ` ( ( invg ` R ) ` E ) ) = E )
83 81 82 oveq12d 
 |-  ( ph -> ( ( ( invg ` R ) ` ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( invg ` R ) ` F ) ) ) ) .+ ( ( invg ` R ) ` ( ( invg ` R ) ` E ) ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) .+ E ) )
84 57 70 83 3eqtrd 
 |-  ( ph -> ( ( invg ` R ) ` ( ( R gsum D ) .x. ( C .- A ) ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) .+ E ) )
85 22 25 84 3eqtr3d 
 |-  ( ph -> ( ( R gsum D ) .x. ( A .- C ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) .+ E ) )