Theorem csrgbinom

Description: The binomial theorem for commutative semirings. (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	csrgbinom	|- ( ( ( R e. SRing /\ G e. CMnd /\ N e. NN0 ) /\ ( A e. S /\ B e. S ) ) -> ( 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		3simpb	|- ( ( R e. SRing /\ G e. CMnd /\ N e. NN0 ) -> ( R e. SRing /\ N e. NN0 ) )
8	7	adantr	|- ( ( ( R e. SRing /\ G e. CMnd /\ N e. NN0 ) /\ ( A e. S /\ B e. S ) ) -> ( R e. SRing /\ N e. NN0 ) )
9		simprl	|- ( ( ( R e. SRing /\ G e. CMnd /\ N e. NN0 ) /\ ( A e. S /\ B e. S ) ) -> A e. S )
10		simprr	|- ( ( ( R e. SRing /\ G e. CMnd /\ N e. NN0 ) /\ ( A e. S /\ B e. S ) ) -> B e. S )
11		simpl2	|- ( ( ( R e. SRing /\ G e. CMnd /\ N e. NN0 ) /\ ( A e. S /\ B e. S ) ) -> G e. CMnd )
12	5 1	mgpbas	|- S = ( Base ` G )
13	5 2	mgpplusg	|- .X. = ( +g ` G )
14	12 13	cmncom	|- ( ( G e. CMnd /\ A e. S /\ B e. S ) -> ( A .X. B ) = ( B .X. A ) )
15	11 9 10 14	syl3anc	|- ( ( ( R e. SRing /\ G e. CMnd /\ N e. NN0 ) /\ ( A e. S /\ B e. S ) ) -> ( A .X. B ) = ( B .X. A ) )
16	1 2 3 4 5 6	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 ) ) ) ) ) )
17	8 9 10 15 16	syl13anc	|- ( ( ( R e. SRing /\ G e. CMnd /\ N e. NN0 ) /\ ( A e. S /\ B e. S ) ) -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )