Metamath Proof Explorer

Theorem srgbinomlem

Description: Lemma for srgbinom . Inductive step, analogous to binomlem . (Contributed by AV, 24-Aug-2019)

Ref Expression
Hypotheses srgbinom.s 
|- S = ( Base ` R )
srgbinom.m 
|- .X. = ( .r ` R )
srgbinom.t 
|- .x. = ( .g ` R )
srgbinom.a 
|- .+ = ( +g ` R )
srgbinom.g 
|- G = ( mulGrp ` R )
srgbinom.e 
|- .^ = ( .g ` G )
srgbinomlem.r 
|- ( ph -> R e. SRing )
srgbinomlem.a 
|- ( ph -> A e. S )
srgbinomlem.b 
|- ( ph -> B e. S )
srgbinomlem.c 
|- ( ph -> ( A .X. B ) = ( B .X. A ) )
srgbinomlem.n 
|- ( ph -> N e. NN0 )
srgbinomlem.i 
|- ( ps -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
Assertion srgbinomlem 
|- ( ( ph /\ ps ) -> ( ( N + 1 ) .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( ( N + 1 ) _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 srgbinom.s 
 |-  S = ( Base ` R )
2 srgbinom.m 
 |-  .X. = ( .r ` R )
3 srgbinom.t 
 |-  .x. = ( .g ` R )
4 srgbinom.a 
 |-  .+ = ( +g ` R )
5 srgbinom.g 
 |-  G = ( mulGrp ` R )
6 srgbinom.e 
 |-  .^ = ( .g ` G )
7 srgbinomlem.r 
 |-  ( ph -> R e. SRing )
8 srgbinomlem.a 
 |-  ( ph -> A e. S )
9 srgbinomlem.b 
 |-  ( ph -> B e. S )
10 srgbinomlem.c 
 |-  ( ph -> ( A .X. B ) = ( B .X. A ) )
11 srgbinomlem.n 
 |-  ( ph -> N e. NN0 )
12 srgbinomlem.i 
 |-  ( ps -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 srgbinomlem3 
 |-  ( ( ph /\ ps ) -> ( ( N .^ ( A .+ B ) ) .X. A ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
14 1 2 3 4 5 6 7 8 9 10 11 12 srgbinomlem4 
 |-  ( ( ph /\ ps ) -> ( ( N .^ ( A .+ B ) ) .X. B ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
15 13 14 oveq12d 
 |-  ( ( ph /\ ps ) -> ( ( ( N .^ ( A .+ B ) ) .X. A ) .+ ( ( N .^ ( A .+ B ) ) .X. B ) ) = ( ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
16 5 srgmgp 
 |-  ( R e. SRing -> G e. Mnd )
17 7 16 syl 
 |-  ( ph -> G e. Mnd )
18 srgmnd 
 |-  ( R e. SRing -> R e. Mnd )
19 7 18 syl 
 |-  ( ph -> R e. Mnd )
20 1 4 mndcl 
 |-  ( ( R e. Mnd /\ A e. S /\ B e. S ) -> ( A .+ B ) e. S )
21 19 8 9 20 syl3anc 
 |-  ( ph -> ( A .+ B ) e. S )
22 17 11 21 3jca 
 |-  ( ph -> ( G e. Mnd /\ N e. NN0 /\ ( A .+ B ) e. S ) )
23 22 adantr 
 |-  ( ( ph /\ ps ) -> ( G e. Mnd /\ N e. NN0 /\ ( A .+ B ) e. S ) )
24 5 1 mgpbas 
 |-  S = ( Base ` G )
25 5 2 mgpplusg 
 |-  .X. = ( +g ` G )
26 24 6 25 mulgnn0p1 
 |-  ( ( G e. Mnd /\ N e. NN0 /\ ( A .+ B ) e. S ) -> ( ( N + 1 ) .^ ( A .+ B ) ) = ( ( N .^ ( A .+ B ) ) .X. ( A .+ B ) ) )
27 23 26 syl 
 |-  ( ( ph /\ ps ) -> ( ( N + 1 ) .^ ( A .+ B ) ) = ( ( N .^ ( A .+ B ) ) .X. ( A .+ B ) ) )
28 24 6 17 11 21 mulgnn0cld 
 |-  ( ph -> ( N .^ ( A .+ B ) ) e. S )
29 28 8 9 3jca 
 |-  ( ph -> ( ( N .^ ( A .+ B ) ) e. S /\ A e. S /\ B e. S ) )
30 7 29 jca 
 |-  ( ph -> ( R e. SRing /\ ( ( N .^ ( A .+ B ) ) e. S /\ A e. S /\ B e. S ) ) )
31 30 adantr 
 |-  ( ( ph /\ ps ) -> ( R e. SRing /\ ( ( N .^ ( A .+ B ) ) e. S /\ A e. S /\ B e. S ) ) )
32 1 4 2 srgdi 
 |-  ( ( R e. SRing /\ ( ( N .^ ( A .+ B ) ) e. S /\ A e. S /\ B e. S ) ) -> ( ( N .^ ( A .+ B ) ) .X. ( A .+ B ) ) = ( ( ( N .^ ( A .+ B ) ) .X. A ) .+ ( ( N .^ ( A .+ B ) ) .X. B ) ) )
33 31 32 syl 
 |-  ( ( ph /\ ps ) -> ( ( N .^ ( A .+ B ) ) .X. ( A .+ B ) ) = ( ( ( N .^ ( A .+ B ) ) .X. A ) .+ ( ( N .^ ( A .+ B ) ) .X. B ) ) )
34 27 33 eqtrd 
 |-  ( ( ph /\ ps ) -> ( ( N + 1 ) .^ ( A .+ B ) ) = ( ( ( N .^ ( A .+ B ) ) .X. A ) .+ ( ( N .^ ( A .+ B ) ) .X. B ) ) )
35 elfzelz 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. ZZ )
36 bcpasc 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( ( N _C k ) + ( N _C ( k - 1 ) ) ) = ( ( N + 1 ) _C k ) )
37 11 35 36 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) + ( N _C ( k - 1 ) ) ) = ( ( N + 1 ) _C k ) )
38 37 oveq1d 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C k ) + ( N _C ( k - 1 ) ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) = ( ( ( N + 1 ) _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) )
39 19 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> R e. Mnd )
40 bccl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
41 11 35 40 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C k ) e. NN0 )
42 35 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. ZZ )
43 peano2zm 
 |-  ( k e. ZZ -> ( k - 1 ) e. ZZ )
44 42 43 syl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( k - 1 ) e. ZZ )
45 bccl 
 |-  ( ( N e. NN0 /\ ( k - 1 ) e. ZZ ) -> ( N _C ( k - 1 ) ) e. NN0 )
46 11 44 45 syl2an2r 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. NN0 )
47 7 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> R e. SRing )
48 17 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> G e. Mnd )
49 fznn0sub 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( ( N + 1 ) - k ) e. NN0 )
50 49 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N + 1 ) - k ) e. NN0 )
51 8 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> A e. S )
52 24 6 48 50 51 mulgnn0cld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N + 1 ) - k ) .^ A ) e. S )
53 elfznn0 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. NN0 )
54 53 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. NN0 )
55 9 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> B e. S )
56 24 6 48 54 55 mulgnn0cld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( k .^ B ) e. S )
57 1 2 srgcl 
 |-  ( ( R e. SRing /\ ( ( ( N + 1 ) - k ) .^ A ) e. S /\ ( k .^ B ) e. S ) -> ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) e. S )
58 47 52 56 57 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) e. S )
59 1 3 4 mulgnn0dir 
 |-  ( ( R e. Mnd /\ ( ( N _C k ) e. NN0 /\ ( N _C ( k - 1 ) ) e. NN0 /\ ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) e. S ) ) -> ( ( ( N _C k ) + ( N _C ( k - 1 ) ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) = ( ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) .+ ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) )
60 39 41 46 58 59 syl13anc 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C k ) + ( N _C ( k - 1 ) ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) = ( ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) .+ ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) )
61 38 60 eqtr3d 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N + 1 ) _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) = ( ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) .+ ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) )
62 61 mpteq2dva 
 |-  ( ph -> ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( ( N + 1 ) _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) = ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) .+ ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
63 62 oveq2d 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( ( N + 1 ) _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) .+ ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
64 srgcmn 
 |-  ( R e. SRing -> R e. CMnd )
65 7 64 syl 
 |-  ( ph -> R e. CMnd )
66 fzfid 
 |-  ( ph -> ( 0 ... ( N + 1 ) ) e. Fin )
67 1 3 39 41 58 mulgnn0cld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
68 35 43 syl 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( k - 1 ) e. ZZ )
69 11 68 45 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. NN0 )
70 1 3 39 69 58 mulgnn0cld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
71 eqid 
 |-  ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) = ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) )
72 eqid 
 |-  ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) = ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) )
73 1 4 65 66 67 70 71 72 gsummptfidmadd 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) .+ ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) = ( ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
74 63 73 eqtrd 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( ( N + 1 ) _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
75 74 adantr 
 |-  ( ( ph /\ ps ) -> ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( ( N + 1 ) _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
76 15 34 75 3eqtr4d 
 |-  ( ( ph /\ ps ) -> ( ( N + 1 ) .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( ( N + 1 ) _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )