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	$⊢ \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	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)))$

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

Metamath Proof Explorer

Theorem srgbinom

Proof