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 mulgnn0cl 
 |-  ( ( G e. Mnd /\ N e. NN0 /\ ( A .+ B ) e. S ) -> ( N .^ ( A .+ B ) ) e. S )
29 17 11 21 28 syl3anc 
 |-  ( ph -> ( N .^ ( A .+ B ) ) e. S )
30 29 8 9 3jca 
 |-  ( ph -> ( ( N .^ ( A .+ B ) ) e. S /\ A e. S /\ B e. S ) )
31 7 30 jca 
 |-  ( ph -> ( R e. SRing /\ ( ( N .^ ( A .+ B ) ) e. S /\ A e. S /\ B e. S ) ) )
32 31 adantr 
 |-  ( ( ph /\ ps ) -> ( R e. SRing /\ ( ( N .^ ( A .+ B ) ) e. S /\ A e. S /\ B e. S ) ) )
33 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 ) ) )
34 32 33 syl 
 |-  ( ( ph /\ ps ) -> ( ( N .^ ( A .+ B ) ) .X. ( A .+ B ) ) = ( ( ( N .^ ( A .+ B ) ) .X. A ) .+ ( ( N .^ ( A .+ B ) ) .X. B ) ) )
35 27 34 eqtrd 
 |-  ( ( ph /\ ps ) -> ( ( N + 1 ) .^ ( A .+ B ) ) = ( ( ( N .^ ( A .+ B ) ) .X. A ) .+ ( ( N .^ ( A .+ B ) ) .X. B ) ) )
36 elfzelz 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. ZZ )
37 bcpasc 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( ( N _C k ) + ( N _C ( k - 1 ) ) ) = ( ( N + 1 ) _C k ) )
38 11 36 37 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) + ( N _C ( k - 1 ) ) ) = ( ( N + 1 ) _C k ) )
39 38 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 ) ) ) )
40 19 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> R e. Mnd )
41 bccl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
42 11 36 41 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C k ) e. NN0 )
43 36 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. ZZ )
44 peano2zm 
 |-  ( k e. ZZ -> ( k - 1 ) e. ZZ )
45 43 44 syl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( k - 1 ) e. ZZ )
46 bccl 
 |-  ( ( N e. NN0 /\ ( k - 1 ) e. ZZ ) -> ( N _C ( k - 1 ) ) e. NN0 )
47 11 45 46 syl2an2r 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. NN0 )
48 7 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> R e. SRing )
49 17 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> G e. Mnd )
50 fznn0sub 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( ( N + 1 ) - k ) e. NN0 )
51 50 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N + 1 ) - k ) e. NN0 )
52 8 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> A e. S )
53 24 6 mulgnn0cl 
 |-  ( ( G e. Mnd /\ ( ( N + 1 ) - k ) e. NN0 /\ A e. S ) -> ( ( ( N + 1 ) - k ) .^ A ) e. S )
54 49 51 52 53 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N + 1 ) - k ) .^ A ) e. S )
55 elfznn0 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. NN0 )
56 55 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. NN0 )
57 9 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> B e. S )
58 24 6 mulgnn0cl 
 |-  ( ( G e. Mnd /\ k e. NN0 /\ B e. S ) -> ( k .^ B ) e. S )
59 49 56 57 58 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( k .^ B ) e. S )
60 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 )
61 48 54 59 60 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) e. S )
62 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 ) ) ) ) )
63 40 42 47 61 62 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 ) ) ) ) )
64 39 63 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 ) ) ) ) )
65 64 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 ) ) ) ) ) )
66 65 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 ) ) ) ) ) ) )
67 srgcmn 
 |-  ( R e. SRing -> R e. CMnd )
68 7 67 syl 
 |-  ( ph -> R e. CMnd )
69 fzfid 
 |-  ( ph -> ( 0 ... ( N + 1 ) ) e. Fin )
70 1 3 mulgnn0cl 
 |-  ( ( R e. Mnd /\ ( N _C k ) e. NN0 /\ ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) e. S ) -> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
71 40 42 61 70 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
72 36 44 syl 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( k - 1 ) e. ZZ )
73 11 72 46 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. NN0 )
74 1 3 mulgnn0cl 
 |-  ( ( R e. Mnd /\ ( N _C ( k - 1 ) ) e. NN0 /\ ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) e. S ) -> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
75 40 73 61 74 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
76 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 ) ) ) )
77 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 ) ) ) )
78 1 4 68 69 71 75 76 77 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 ) ) ) ) ) ) )
79 66 78 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 ) ) ) ) ) ) )
80 79 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 ) ) ) ) ) ) )
81 15 35 80 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 ) ) ) ) ) )