Metamath Proof Explorer

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	$⊢ \underset{˙}{\times} = \cdot_{R}$
		srgbinom.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		srgbinom.a	$⊢ \underset{˙}{+} = +_{R}$
		srgbinom.g	$⊢ G = {mulGrp}_{R}$
		srgbinom.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
	Assertion	csrgbinom	$⊢ ((R \in SRing \land G \in CMnd \land N \in ℕ_{0}) \land (A \in S \land B \in S)) \to N \underset{˙}{\times} (A \underset{˙}{+} B) = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$

Proof

Step	Hyp	Ref	Expression
1		srgbinom.s	$⊢ S = {Base}_{R}$
2		srgbinom.m	$⊢ \underset{˙}{\times} = \cdot_{R}$
3		srgbinom.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		srgbinom.a	$⊢ \underset{˙}{+} = +_{R}$
5		srgbinom.g	$⊢ G = {mulGrp}_{R}$
6		srgbinom.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
7		3simpb	$⊢ (R \in SRing \land G \in CMnd \land N \in ℕ_{0}) \to (R \in SRing \land N \in ℕ_{0})$
8	7	adantr	$⊢ ((R \in SRing \land G \in CMnd \land N \in ℕ_{0}) \land (A \in S \land B \in S)) \to (R \in SRing \land N \in ℕ_{0})$
9		simprl	$⊢ ((R \in SRing \land G \in CMnd \land N \in ℕ_{0}) \land (A \in S \land B \in S)) \to A \in S$
10		simprr	$⊢ ((R \in SRing \land G \in CMnd \land N \in ℕ_{0}) \land (A \in S \land B \in S)) \to B \in S$
11		simpl2	$⊢ ((R \in SRing \land G \in CMnd \land N \in ℕ_{0}) \land (A \in S \land B \in S)) \to G \in CMnd$
12	5 1	mgpbas	$⊢ S = {Base}_{G}$
13	5 2	mgpplusg	$⊢ \underset{˙}{\times} = +_{G}$
14	12 13	cmncom	$⊢ (G \in CMnd \land A \in S \land B \in S) \to A \underset{˙}{\times} B = B \underset{˙}{\times} A$
15	11 9 10 14	syl3anc	$⊢ ((R \in SRing \land G \in CMnd \land N \in ℕ_{0}) \land (A \in S \land B \in S)) \to A \underset{˙}{\times} B = B \underset{˙}{\times} A$
16	1 2 3 4 5 6	srgbinom	$⊢ ((R \in SRing \land N \in ℕ_{0}) \land (A \in S \land B \in S \land A \underset{˙}{\times} B = B \underset{˙}{\times} A)) \to N \underset{˙}{\times} (A \underset{˙}{+} B) = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
17	8 9 10 15 16	syl13anc	$⊢ ((R \in SRing \land G \in CMnd \land N \in ℕ_{0}) \land (A \in S \land B \in S)) \to N \underset{˙}{\times} (A \underset{˙}{+} B) = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$