Metamath Proof Explorer

Theorem srgbinom

Description: The binomial theorem for commuting elements of a semiring: ( A + B ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ k ) x. ( B ^ ( N - k ) ) (generalization of binom ). (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 )
Assertion srgbinom 
|- ( ( ( R e. SRing /\ N e. NN0 ) /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - 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 oveq1 
 |-  ( x = 0 -> ( x .^ ( A .+ B ) ) = ( 0 .^ ( A .+ B ) ) )
8 oveq2 
 |-  ( x = 0 -> ( 0 ... x ) = ( 0 ... 0 ) )
9 oveq1 
 |-  ( x = 0 -> ( x _C k ) = ( 0 _C k ) )
10 oveq1 
 |-  ( x = 0 -> ( x - k ) = ( 0 - k ) )
11 10 oveq1d 
 |-  ( x = 0 -> ( ( x - k ) .^ A ) = ( ( 0 - k ) .^ A ) )
12 11 oveq1d 
 |-  ( x = 0 -> ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) = ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) )
13 9 12 oveq12d 
 |-  ( x = 0 -> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) = ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) )
14 8 13 mpteq12dv 
 |-  ( x = 0 -> ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) = ( k e. ( 0 ... 0 ) |-> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) ) )
15 14 oveq2d 
 |-  ( x = 0 -> ( R gsum ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( R gsum ( k e. ( 0 ... 0 ) |-> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
16 7 15 eqeq12d 
 |-  ( x = 0 -> ( ( x .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) <-> ( 0 .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... 0 ) |-> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
17 16 imbi2d 
 |-  ( x = 0 -> ( ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( x .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) <-> ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 0 .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... 0 ) |-> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) ) )
18 oveq1 
 |-  ( x = n -> ( x .^ ( A .+ B ) ) = ( n .^ ( A .+ B ) ) )
19 oveq2 
 |-  ( x = n -> ( 0 ... x ) = ( 0 ... n ) )
20 oveq1 
 |-  ( x = n -> ( x _C k ) = ( n _C k ) )
21 oveq1 
 |-  ( x = n -> ( x - k ) = ( n - k ) )
22 21 oveq1d 
 |-  ( x = n -> ( ( x - k ) .^ A ) = ( ( n - k ) .^ A ) )
23 22 oveq1d 
 |-  ( x = n -> ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) = ( ( ( n - k ) .^ A ) .X. ( k .^ B ) ) )
24 20 23 oveq12d 
 |-  ( x = n -> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) = ( ( n _C k ) .x. ( ( ( n - k ) .^ A ) .X. ( k .^ B ) ) ) )
25 19 24 mpteq12dv 
 |-  ( x = n -> ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) = ( k e. ( 0 ... n ) |-> ( ( n _C k ) .x. ( ( ( n - k ) .^ A ) .X. ( k .^ B ) ) ) ) )
26 25 oveq2d 
 |-  ( x = n -> ( R gsum ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( R gsum ( k e. ( 0 ... n ) |-> ( ( n _C k ) .x. ( ( ( n - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
27 18 26 eqeq12d 
 |-  ( x = n -> ( ( x .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) <-> ( n .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... n ) |-> ( ( n _C k ) .x. ( ( ( n - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
28 27 imbi2d 
 |-  ( x = n -> ( ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( x .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) <-> ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( n .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... n ) |-> ( ( n _C k ) .x. ( ( ( n - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) ) )
29 oveq1 
 |-  ( x = ( n + 1 ) -> ( x .^ ( A .+ B ) ) = ( ( n + 1 ) .^ ( A .+ B ) ) )
30 oveq2 
 |-  ( x = ( n + 1 ) -> ( 0 ... x ) = ( 0 ... ( n + 1 ) ) )
31 oveq1 
 |-  ( x = ( n + 1 ) -> ( x _C k ) = ( ( n + 1 ) _C k ) )
32 oveq1 
 |-  ( x = ( n + 1 ) -> ( x - k ) = ( ( n + 1 ) - k ) )
33 32 oveq1d 
 |-  ( x = ( n + 1 ) -> ( ( x - k ) .^ A ) = ( ( ( n + 1 ) - k ) .^ A ) )
34 33 oveq1d 
 |-  ( x = ( n + 1 ) -> ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) = ( ( ( ( n + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) )
35 31 34 oveq12d 
 |-  ( x = ( n + 1 ) -> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) = ( ( ( n + 1 ) _C k ) .x. ( ( ( ( n + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) )
36 30 35 mpteq12dv 
 |-  ( x = ( n + 1 ) -> ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) = ( k e. ( 0 ... ( n + 1 ) ) |-> ( ( ( n + 1 ) _C k ) .x. ( ( ( ( n + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) )
37 36 oveq2d 
 |-  ( x = ( n + 1 ) -> ( R gsum ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( R gsum ( k e. ( 0 ... ( n + 1 ) ) |-> ( ( ( n + 1 ) _C k ) .x. ( ( ( ( n + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
38 29 37 eqeq12d 
 |-  ( x = ( n + 1 ) -> ( ( x .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) <-> ( ( n + 1 ) .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... ( n + 1 ) ) |-> ( ( ( n + 1 ) _C k ) .x. ( ( ( ( n + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
39 38 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( x .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) <-> ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( ( n + 1 ) .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... ( n + 1 ) ) |-> ( ( ( n + 1 ) _C k ) .x. ( ( ( ( n + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) ) )
40 oveq1 
 |-  ( x = N -> ( x .^ ( A .+ B ) ) = ( N .^ ( A .+ B ) ) )
41 oveq2 
 |-  ( x = N -> ( 0 ... x ) = ( 0 ... N ) )
42 oveq1 
 |-  ( x = N -> ( x _C k ) = ( N _C k ) )
43 oveq1 
 |-  ( x = N -> ( x - k ) = ( N - k ) )
44 43 oveq1d 
 |-  ( x = N -> ( ( x - k ) .^ A ) = ( ( N - k ) .^ A ) )
45 44 oveq1d 
 |-  ( x = N -> ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) = ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) )
46 42 45 oveq12d 
 |-  ( x = N -> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) = ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) )
47 41 46 mpteq12dv 
 |-  ( x = N -> ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) = ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) )
48 47 oveq2d 
 |-  ( x = N -> ( R gsum ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
49 40 48 eqeq12d 
 |-  ( x = N -> ( ( x .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) <-> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
50 49 imbi2d 
 |-  ( x = N -> ( ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( x .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... x ) |-> ( ( x _C k ) .x. ( ( ( x - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) <-> ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) ) )
51 simpr1 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> A e. S )
52 5 1 mgpbas 
 |-  S = ( Base ` G )
53 51 52 eleqtrdi 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> A e. ( Base ` G ) )
54 eqid 
 |-  ( Base ` G ) = ( Base ` G )
55 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
56 54 55 6 mulg0 
 |-  ( A e. ( Base ` G ) -> ( 0 .^ A ) = ( 0g ` G ) )
57 53 56 syl 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 0 .^ A ) = ( 0g ` G ) )
58 simpr2 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> B e. S )
59 58 52 eleqtrdi 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> B e. ( Base ` G ) )
60 54 55 6 mulg0 
 |-  ( B e. ( Base ` G ) -> ( 0 .^ B ) = ( 0g ` G ) )
61 59 60 syl 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 0 .^ B ) = ( 0g ` G ) )
62 57 61 oveq12d 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( ( 0 .^ A ) .X. ( 0 .^ B ) ) = ( ( 0g ` G ) .X. ( 0g ` G ) ) )
63 62 oveq2d 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 1 .x. ( ( 0 .^ A ) .X. ( 0 .^ B ) ) ) = ( 1 .x. ( ( 0g ` G ) .X. ( 0g ` G ) ) ) )
64 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
65 1 64 srgidcl 
 |-  ( R e. SRing -> ( 1r ` R ) e. S )
66 65 ancli 
 |-  ( R e. SRing -> ( R e. SRing /\ ( 1r ` R ) e. S ) )
67 66 adantr 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( R e. SRing /\ ( 1r ` R ) e. S ) )
68 1 2 64 srglidm 
 |-  ( ( R e. SRing /\ ( 1r ` R ) e. S ) -> ( ( 1r ` R ) .X. ( 1r ` R ) ) = ( 1r ` R ) )
69 67 68 syl 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( ( 1r ` R ) .X. ( 1r ` R ) ) = ( 1r ` R ) )
70 69 oveq2d 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 1 .x. ( ( 1r ` R ) .X. ( 1r ` R ) ) ) = ( 1 .x. ( 1r ` R ) ) )
71 eqid 
 |-  ( Base ` R ) = ( Base ` R )
72 71 64 srgidcl 
 |-  ( R e. SRing -> ( 1r ` R ) e. ( Base ` R ) )
73 71 3 mulg1 
 |-  ( ( 1r ` R ) e. ( Base ` R ) -> ( 1 .x. ( 1r ` R ) ) = ( 1r ` R ) )
74 72 73 syl 
 |-  ( R e. SRing -> ( 1 .x. ( 1r ` R ) ) = ( 1r ` R ) )
75 74 adantr 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 1 .x. ( 1r ` R ) ) = ( 1r ` R ) )
76 70 75 eqtrd 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 1 .x. ( ( 1r ` R ) .X. ( 1r ` R ) ) ) = ( 1r ` R ) )
77 5 64 ringidval 
 |-  ( 1r ` R ) = ( 0g ` G )
78 id 
 |-  ( ( 1r ` R ) = ( 0g ` G ) -> ( 1r ` R ) = ( 0g ` G ) )
79 78 78 oveq12d 
 |-  ( ( 1r ` R ) = ( 0g ` G ) -> ( ( 1r ` R ) .X. ( 1r ` R ) ) = ( ( 0g ` G ) .X. ( 0g ` G ) ) )
80 79 oveq2d 
 |-  ( ( 1r ` R ) = ( 0g ` G ) -> ( 1 .x. ( ( 1r ` R ) .X. ( 1r ` R ) ) ) = ( 1 .x. ( ( 0g ` G ) .X. ( 0g ` G ) ) ) )
81 80 78 eqeq12d 
 |-  ( ( 1r ` R ) = ( 0g ` G ) -> ( ( 1 .x. ( ( 1r ` R ) .X. ( 1r ` R ) ) ) = ( 1r ` R ) <-> ( 1 .x. ( ( 0g ` G ) .X. ( 0g ` G ) ) ) = ( 0g ` G ) ) )
82 77 81 ax-mp 
 |-  ( ( 1 .x. ( ( 1r ` R ) .X. ( 1r ` R ) ) ) = ( 1r ` R ) <-> ( 1 .x. ( ( 0g ` G ) .X. ( 0g ` G ) ) ) = ( 0g ` G ) )
83 76 82 sylib 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 1 .x. ( ( 0g ` G ) .X. ( 0g ` G ) ) ) = ( 0g ` G ) )
84 63 83 eqtrd 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 1 .x. ( ( 0 .^ A ) .X. ( 0 .^ B ) ) ) = ( 0g ` G ) )
85 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
86 85 a1i 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 0 ... 0 ) = { 0 } )
87 86 mpteq1d 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( k e. ( 0 ... 0 ) |-> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) ) = ( k e. { 0 } |-> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) ) )
88 87 oveq2d 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( R gsum ( k e. ( 0 ... 0 ) |-> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( R gsum ( k e. { 0 } |-> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
89 srgmnd 
 |-  ( R e. SRing -> R e. Mnd )
90 89 adantr 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> R e. Mnd )
91 c0ex 
 |-  0 e. _V
92 91 a1i 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> 0 e. _V )
93 77 65 eqeltrrid 
 |-  ( R e. SRing -> ( 0g ` G ) e. S )
94 93 adantr 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 0g ` G ) e. S )
95 84 94 eqeltrd 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 1 .x. ( ( 0 .^ A ) .X. ( 0 .^ B ) ) ) e. S )
96 oveq2 
 |-  ( k = 0 -> ( 0 _C k ) = ( 0 _C 0 ) )
97 0nn0 
 |-  0 e. NN0
98 bcn0 
 |-  ( 0 e. NN0 -> ( 0 _C 0 ) = 1 )
99 97 98 ax-mp 
 |-  ( 0 _C 0 ) = 1
100 96 99 eqtrdi 
 |-  ( k = 0 -> ( 0 _C k ) = 1 )
101 oveq2 
 |-  ( k = 0 -> ( 0 - k ) = ( 0 - 0 ) )
102 0m0e0 
 |-  ( 0 - 0 ) = 0
103 101 102 eqtrdi 
 |-  ( k = 0 -> ( 0 - k ) = 0 )
104 103 oveq1d 
 |-  ( k = 0 -> ( ( 0 - k ) .^ A ) = ( 0 .^ A ) )
105 oveq1 
 |-  ( k = 0 -> ( k .^ B ) = ( 0 .^ B ) )
106 104 105 oveq12d 
 |-  ( k = 0 -> ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) = ( ( 0 .^ A ) .X. ( 0 .^ B ) ) )
107 100 106 oveq12d 
 |-  ( k = 0 -> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) = ( 1 .x. ( ( 0 .^ A ) .X. ( 0 .^ B ) ) ) )
108 1 107 gsumsn 
 |-  ( ( R e. Mnd /\ 0 e. _V /\ ( 1 .x. ( ( 0 .^ A ) .X. ( 0 .^ B ) ) ) e. S ) -> ( R gsum ( k e. { 0 } |-> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( 1 .x. ( ( 0 .^ A ) .X. ( 0 .^ B ) ) ) )
109 90 92 95 108 syl3anc 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( R gsum ( k e. { 0 } |-> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( 1 .x. ( ( 0 .^ A ) .X. ( 0 .^ B ) ) ) )
110 88 109 eqtrd 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( R gsum ( k e. ( 0 ... 0 ) |-> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( 1 .x. ( ( 0 .^ A ) .X. ( 0 .^ B ) ) ) )
111 1 4 mndcl 
 |-  ( ( R e. Mnd /\ A e. S /\ B e. S ) -> ( A .+ B ) e. S )
112 90 51 58 111 syl3anc 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( A .+ B ) e. S )
113 112 52 eleqtrdi 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( A .+ B ) e. ( Base ` G ) )
114 54 55 6 mulg0 
 |-  ( ( A .+ B ) e. ( Base ` G ) -> ( 0 .^ ( A .+ B ) ) = ( 0g ` G ) )
115 113 114 syl 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 0 .^ ( A .+ B ) ) = ( 0g ` G ) )
116 84 110 115 3eqtr4rd 
 |-  ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( 0 .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... 0 ) |-> ( ( 0 _C k ) .x. ( ( ( 0 - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
117 simprl 
 |-  ( ( n e. NN0 /\ ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) ) -> R e. SRing )
118 51 adantl 
 |-  ( ( n e. NN0 /\ ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) ) -> A e. S )
119 58 adantl 
 |-  ( ( n e. NN0 /\ ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) ) -> B e. S )
120 simprr3 
 |-  ( ( n e. NN0 /\ ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) ) -> ( A .X. B ) = ( B .X. A ) )
121 simpl 
 |-  ( ( n e. NN0 /\ ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) ) -> n e. NN0 )
122 id 
 |-  ( ( n .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... n ) |-> ( ( n _C k ) .x. ( ( ( n - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) -> ( n .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... n ) |-> ( ( n _C k ) .x. ( ( ( n - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
123 1 2 3 4 5 6 117 118 119 120 121 122 srgbinomlem 
 |-  ( ( ( n e. NN0 /\ ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) ) /\ ( n .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... n ) |-> ( ( n _C k ) .x. ( ( ( n - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) -> ( ( n + 1 ) .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... ( n + 1 ) ) |-> ( ( ( n + 1 ) _C k ) .x. ( ( ( ( n + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
124 123 exp31 
 |-  ( n e. NN0 -> ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( ( n .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... n ) |-> ( ( n _C k ) .x. ( ( ( n - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) -> ( ( n + 1 ) .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... ( n + 1 ) ) |-> ( ( ( n + 1 ) _C k ) .x. ( ( ( ( n + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) ) )
125 124 a2d 
 |-  ( n e. NN0 -> ( ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( n .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... n ) |-> ( ( n _C k ) .x. ( ( ( n - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) -> ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( ( n + 1 ) .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... ( n + 1 ) ) |-> ( ( ( n + 1 ) _C k ) .x. ( ( ( ( n + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) ) )
126 17 28 39 50 116 125 nn0ind 
 |-  ( N e. NN0 -> ( ( R e. SRing /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
127 126 expd 
 |-  ( N e. NN0 -> ( R e. SRing -> ( ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) ) )
128 127 impcom 
 |-  ( ( R e. SRing /\ N e. NN0 ) -> ( ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
129 128 imp 
 |-  ( ( ( R e. SRing /\ N e. NN0 ) /\ ( A e. S /\ B e. S /\ ( A .X. B ) = ( B .X. A ) ) ) -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )