Metamath Proof Explorer

Theorem telgsumfzslem

Description: Lemma for telgsumfzs (induction step). (Contributed by AV, 23-Nov-2019)

Ref Expression
Hypotheses telgsumfzs.b 
|- B = ( Base ` G )
telgsumfzs.g 
|- ( ph -> G e. Abel )
telgsumfzs.m 
|- .- = ( -g ` G )
Assertion telgsumfzslem 
|- ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) -> ( G gsum ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) ) )

Proof

Step Hyp Ref Expression
1 telgsumfzs.b 
 |-  B = ( Base ` G )
2 telgsumfzs.g 
 |-  ( ph -> G e. Abel )
3 telgsumfzs.m 
 |-  .- = ( -g ` G )
4 eqid 
 |-  ( +g ` G ) = ( +g ` G )
5 2 adantr 
 |-  ( ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> G e. Abel )
6 ablcmn 
 |-  ( G e. Abel -> G e. CMnd )
7 5 6 syl 
 |-  ( ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> G e. CMnd )
8 7 adantl 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> G e. CMnd )
9 fzfid 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( M ... ( y + 1 ) ) e. Fin )
10 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
11 2 10 syl 
 |-  ( ph -> G e. Grp )
12 11 ad2antrl 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> G e. Grp )
13 12 adantr 
 |-  ( ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) /\ i e. ( M ... ( y + 1 ) ) ) -> G e. Grp )
14 fzelp1 
 |-  ( i e. ( M ... ( y + 1 ) ) -> i e. ( M ... ( ( y + 1 ) + 1 ) ) )
15 simpr 
 |-  ( ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B )
16 15 adantl 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B )
17 rspcsbela 
 |-  ( ( i e. ( M ... ( ( y + 1 ) + 1 ) ) /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> [_ i / k ]_ C e. B )
18 14 16 17 syl2anr 
 |-  ( ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) /\ i e. ( M ... ( y + 1 ) ) ) -> [_ i / k ]_ C e. B )
19 fzp1elp1 
 |-  ( i e. ( M ... ( y + 1 ) ) -> ( i + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) )
20 rspcsbela 
 |-  ( ( ( i + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> [_ ( i + 1 ) / k ]_ C e. B )
21 19 16 20 syl2anr 
 |-  ( ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) /\ i e. ( M ... ( y + 1 ) ) ) -> [_ ( i + 1 ) / k ]_ C e. B )
22 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ [_ i / k ]_ C e. B /\ [_ ( i + 1 ) / k ]_ C e. B ) -> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) e. B )
23 13 18 21 22 syl3anc 
 |-  ( ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) /\ i e. ( M ... ( y + 1 ) ) ) -> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) e. B )
24 fzp1disj 
 |-  ( ( M ... y ) i^i { ( y + 1 ) } ) = (/)
25 24 a1i 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( ( M ... y ) i^i { ( y + 1 ) } ) = (/) )
26 fzsuc 
 |-  ( y e. ( ZZ>= ` M ) -> ( M ... ( y + 1 ) ) = ( ( M ... y ) u. { ( y + 1 ) } ) )
27 26 adantr 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( M ... ( y + 1 ) ) = ( ( M ... y ) u. { ( y + 1 ) } ) )
28 1 4 8 9 23 25 27 gsummptfidmsplit 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( G gsum ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) ( +g ` G ) ( G gsum ( i e. { ( y + 1 ) } |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) ) )
29 28 adantr 
 |-  ( ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) /\ ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ) -> ( G gsum ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) ( +g ` G ) ( G gsum ( i e. { ( y + 1 ) } |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) ) )
30 simpr 
 |-  ( ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) /\ ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ) -> ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) )
31 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
32 11 31 syl 
 |-  ( ph -> G e. Mnd )
33 32 ad2antrl 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> G e. Mnd )
34 ovexd 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( y + 1 ) e. _V )
35 peano2uz 
 |-  ( y e. ( ZZ>= ` M ) -> ( y + 1 ) e. ( ZZ>= ` M ) )
36 eluzfz2 
 |-  ( ( y + 1 ) e. ( ZZ>= ` M ) -> ( y + 1 ) e. ( M ... ( y + 1 ) ) )
37 35 36 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( y + 1 ) e. ( M ... ( y + 1 ) ) )
38 fzelp1 
 |-  ( ( y + 1 ) e. ( M ... ( y + 1 ) ) -> ( y + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) )
39 37 38 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( y + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) )
40 rspcsbela 
 |-  ( ( ( y + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> [_ ( y + 1 ) / k ]_ C e. B )
41 39 15 40 syl2an 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> [_ ( y + 1 ) / k ]_ C e. B )
42 peano2uz 
 |-  ( ( y + 1 ) e. ( ZZ>= ` M ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` M ) )
43 35 42 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` M ) )
44 eluzfz2 
 |-  ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` M ) -> ( ( y + 1 ) + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) )
45 43 44 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( ( y + 1 ) + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) )
46 rspcsbela 
 |-  ( ( ( ( y + 1 ) + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> [_ ( ( y + 1 ) + 1 ) / k ]_ C e. B )
47 45 15 46 syl2an 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> [_ ( ( y + 1 ) + 1 ) / k ]_ C e. B )
48 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ [_ ( y + 1 ) / k ]_ C e. B /\ [_ ( ( y + 1 ) + 1 ) / k ]_ C e. B ) -> ( [_ ( y + 1 ) / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) e. B )
49 12 41 47 48 syl3anc 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( [_ ( y + 1 ) / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) e. B )
50 csbeq1 
 |-  ( i = ( y + 1 ) -> [_ i / k ]_ C = [_ ( y + 1 ) / k ]_ C )
51 oveq1 
 |-  ( i = ( y + 1 ) -> ( i + 1 ) = ( ( y + 1 ) + 1 ) )
52 51 csbeq1d 
 |-  ( i = ( y + 1 ) -> [_ ( i + 1 ) / k ]_ C = [_ ( ( y + 1 ) + 1 ) / k ]_ C )
53 50 52 oveq12d 
 |-  ( i = ( y + 1 ) -> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) = ( [_ ( y + 1 ) / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) )
54 53 adantl 
 |-  ( ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) /\ i = ( y + 1 ) ) -> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) = ( [_ ( y + 1 ) / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) )
55 1 33 34 49 54 gsumsnd 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( G gsum ( i e. { ( y + 1 ) } |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ ( y + 1 ) / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) )
56 55 adantr 
 |-  ( ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) /\ ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ) -> ( G gsum ( i e. { ( y + 1 ) } |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ ( y + 1 ) / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) )
57 30 56 oveq12d 
 |-  ( ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) /\ ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ) -> ( ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) ( +g ` G ) ( G gsum ( i e. { ( y + 1 ) } |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) ) = ( ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ( +g ` G ) ( [_ ( y + 1 ) / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) ) )
58 eluzfz1 
 |-  ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` M ) -> M e. ( M ... ( ( y + 1 ) + 1 ) ) )
59 43 58 syl 
 |-  ( y e. ( ZZ>= ` M ) -> M e. ( M ... ( ( y + 1 ) + 1 ) ) )
60 rspcsbela 
 |-  ( ( M e. ( M ... ( ( y + 1 ) + 1 ) ) /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> [_ M / k ]_ C e. B )
61 59 15 60 syl2an 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> [_ M / k ]_ C e. B )
62 1 4 3 grpnpncan 
 |-  ( ( G e. Grp /\ ( [_ M / k ]_ C e. B /\ [_ ( y + 1 ) / k ]_ C e. B /\ [_ ( ( y + 1 ) + 1 ) / k ]_ C e. B ) ) -> ( ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ( +g ` G ) ( [_ ( y + 1 ) / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) )
63 12 61 41 47 62 syl13anc 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ( +g ` G ) ( [_ ( y + 1 ) / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) )
64 63 adantr 
 |-  ( ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) /\ ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ) -> ( ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ( +g ` G ) ( [_ ( y + 1 ) / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) )
65 29 57 64 3eqtrd 
 |-  ( ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) /\ ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ) -> ( G gsum ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) )
66 65 ex 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) -> ( G gsum ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) ) )