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 11 grpmndd 
 |-  ( ph -> G e. Mnd )
32 31 ad2antrl 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> G e. Mnd )
33 ovexd 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( y + 1 ) e. _V )
34 peano2uz 
 |-  ( y e. ( ZZ>= ` M ) -> ( y + 1 ) e. ( ZZ>= ` M ) )
35 eluzfz2 
 |-  ( ( y + 1 ) e. ( ZZ>= ` M ) -> ( y + 1 ) e. ( M ... ( y + 1 ) ) )
36 34 35 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( y + 1 ) e. ( M ... ( y + 1 ) ) )
37 fzelp1 
 |-  ( ( y + 1 ) e. ( M ... ( y + 1 ) ) -> ( y + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) )
38 36 37 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( y + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) )
39 rspcsbela 
 |-  ( ( ( y + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> [_ ( y + 1 ) / k ]_ C e. B )
40 38 15 39 syl2an 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> [_ ( y + 1 ) / k ]_ C e. B )
41 peano2uz 
 |-  ( ( y + 1 ) e. ( ZZ>= ` M ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` M ) )
42 34 41 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` M ) )
43 eluzfz2 
 |-  ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` M ) -> ( ( y + 1 ) + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) )
44 42 43 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( ( y + 1 ) + 1 ) e. ( M ... ( ( y + 1 ) + 1 ) ) )
45 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 )
46 44 15 45 syl2an 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> [_ ( ( y + 1 ) + 1 ) / k ]_ C e. B )
47 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 )
48 12 40 46 47 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 )
49 csbeq1 
 |-  ( i = ( y + 1 ) -> [_ i / k ]_ C = [_ ( y + 1 ) / k ]_ C )
50 oveq1 
 |-  ( i = ( y + 1 ) -> ( i + 1 ) = ( ( y + 1 ) + 1 ) )
51 50 csbeq1d 
 |-  ( i = ( y + 1 ) -> [_ ( i + 1 ) / k ]_ C = [_ ( ( y + 1 ) + 1 ) / k ]_ C )
52 49 51 oveq12d 
 |-  ( i = ( y + 1 ) -> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) = ( [_ ( y + 1 ) / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) )
53 52 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 ) )
54 1 32 33 48 53 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 ) )
55 54 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 ) )
56 30 55 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 ) ) )
57 eluzfz1 
 |-  ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` M ) -> M e. ( M ... ( ( y + 1 ) + 1 ) ) )
58 42 57 syl 
 |-  ( y e. ( ZZ>= ` M ) -> M e. ( M ... ( ( y + 1 ) + 1 ) ) )
59 rspcsbela 
 |-  ( ( M e. ( M ... ( ( y + 1 ) + 1 ) ) /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> [_ M / k ]_ C e. B )
60 58 15 59 syl2an 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> [_ M / k ]_ C e. B )
61 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 ) )
62 12 60 40 46 61 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 ) )
63 62 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 ) )
64 29 56 63 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 ) )
65 64 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 ) ) )