Theorem crngbinom

Description: The binomial theorem for commutative rings (special case of csrgbinom ): ( A + B ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ k ) x. ( B ^ ( N - k ) ) . (Contributed by AV, 24-Aug-2019)

	Ref	Expression
Hypotheses	crngbinom.s	$$⊢S={\mathrm{Base}}_R$$
	crngbinom.m	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	crngbinom.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	crngbinom.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	crngbinom.g	$$⊢G={\mathrm{mulGrp}}_R$$
	crngbinom.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
Assertion	crngbinom	$$⊢\left(\left(R\in \mathrm{CRing}\wedge N\in {\mathbb{N}}_0\right)\wedge \left(A\in S\wedge B\in S\right)\right)\to N\underset{\dot{}}{\times }\left(A\underset{\dot{}}{+}B\right)=\underset{k=0}{\overset{N}{{\sum }_R}}\left(\left(\genfrac{}{}{0ex}{}{N}{k}\right)\underset{\dot{}}{·}\left(\left(\left(N-k\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(k\underset{\dot{}}{\times }B\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		crngbinom.s	$$⊢S={\mathrm{Base}}_R$$
2		crngbinom.m	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
3		crngbinom.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		crngbinom.a	$$⊢\underset{\dot{}}{+}={+}_R$$
5		crngbinom.g	$$⊢G={\mathrm{mulGrp}}_R$$
6		crngbinom.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
7		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
8		ringsrg	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{SRing}$$
9	7 8	syl	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{SRing}$$
10	9	adantr	$$⊢\left(R\in \mathrm{CRing}\wedge N\in {\mathbb{N}}_0\right)\to R\in \mathrm{SRing}$$
11	5	crngmgp	$$⊢R\in \mathrm{CRing}\to G\in \mathrm{CMnd}$$
12	11	adantr	$$⊢\left(R\in \mathrm{CRing}\wedge N\in {\mathbb{N}}_0\right)\to G\in \mathrm{CMnd}$$
13		simpr	$$⊢\left(R\in \mathrm{CRing}\wedge N\in {\mathbb{N}}_0\right)\to N\in {\mathbb{N}}_0$$
14	10 12 13	3jca	$$⊢\left(R\in \mathrm{CRing}\wedge N\in {\mathbb{N}}_0\right)\to \left(R\in \mathrm{SRing}\wedge G\in \mathrm{CMnd}\wedge N\in {\mathbb{N}}_0\right)$$
15	1 2 3 4 5 6	csrgbinom	$$⊢\left(\left(R\in \mathrm{SRing}\wedge G\in \mathrm{CMnd}\wedge N\in {\mathbb{N}}_0\right)\wedge \left(A\in S\wedge B\in S\right)\right)\to N\underset{\dot{}}{\times }\left(A\underset{\dot{}}{+}B\right)=\underset{k=0}{\overset{N}{{\sum }_R}}\left(\left(\genfrac{}{}{0ex}{}{N}{k}\right)\underset{\dot{}}{·}\left(\left(\left(N-k\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(k\underset{\dot{}}{\times }B\right)\right)\right)$$
16	14 15	sylan	$$⊢\left(\left(R\in \mathrm{CRing}\wedge N\in {\mathbb{N}}_0\right)\wedge \left(A\in S\wedge B\in S\right)\right)\to N\underset{\dot{}}{\times }\left(A\underset{\dot{}}{+}B\right)=\underset{k=0}{\overset{N}{{\sum }_R}}\left(\left(\genfrac{}{}{0ex}{}{N}{k}\right)\underset{\dot{}}{·}\left(\left(\left(N-k\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(k\underset{\dot{}}{\times }B\right)\right)\right)$$