srgbinomlem

Description: Lemma for srgbinom . Inductive step, analogous to binomlem . (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}$
	srgbinomlem.r	$⊢ φ \to R \in SRing$
	srgbinomlem.a	$⊢ φ \to A \in S$
	srgbinomlem.b	$⊢ φ \to B \in S$
	srgbinomlem.c	$⊢ φ \to A \underset{˙}{\times} B = B \underset{˙}{\times} A$
	srgbinomlem.n	$⊢ φ \to N \in ℕ_{0}$
	srgbinomlem.i	$⊢ ψ \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)))$
Assertion	srgbinomlem	$⊢ (φ \land ψ) \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)))$

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		srgbinomlem.r	$⊢ φ \to R \in SRing$
8		srgbinomlem.a	$⊢ φ \to A \in S$
9		srgbinomlem.b	$⊢ φ \to B \in S$
10		srgbinomlem.c	$⊢ φ \to A \underset{˙}{\times} B = B \underset{˙}{\times} A$
11		srgbinomlem.n	$⊢ φ \to N \in ℕ_{0}$
12		srgbinomlem.i	$⊢ ψ \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)))$
13	1 2 3 4 5 6 7 8 9 10 11 12	srgbinomlem3	$⊢ (φ \land ψ) \to (N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} A = {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
14	1 2 3 4 5 6 7 8 9 10 11 12	srgbinomlem4	$⊢ (φ \land ψ) \to (N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} B = {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
15	13 14	oveq12d	$⊢ (φ \land ψ) \to ((N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} A) \underset{˙}{+} ((N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} B) = ({\sum_{R}}_{k = 0}^{N + 1}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} ({\sum_{R}}_{k = 0}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
16	5	srgmgp	$⊢ R \in SRing \to G \in Mnd$
17	7 16	syl	$⊢ φ \to G \in Mnd$
18		srgmnd	$⊢ R \in SRing \to R \in Mnd$
19	7 18	syl	$⊢ φ \to R \in Mnd$
20	1 4	mndcl	$⊢ (R \in Mnd \land A \in S \land B \in S) \to A \underset{˙}{+} B \in S$
21	19 8 9 20	syl3anc	$⊢ φ \to A \underset{˙}{+} B \in S$
22	17 11 21	3jca	$⊢ φ \to (G \in Mnd \land N \in ℕ_{0} \land A \underset{˙}{+} B \in S)$
23	22	adantr	$⊢ (φ \land ψ) \to (G \in Mnd \land N \in ℕ_{0} \land A \underset{˙}{+} B \in S)$
24	5 1	mgpbas	$⊢ S = {Base}_{G}$
25	5 2	mgpplusg	$⊢ \underset{˙}{\times} = +_{G}$
26	24 6 25	mulgnn0p1	$⊢ (G \in Mnd \land N \in ℕ_{0} \land A \underset{˙}{+} B \in S) \to (N + 1) \underset{˙}{\times} (A \underset{˙}{+} B) = (N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} (A \underset{˙}{+} B)$
27	23 26	syl	$⊢ (φ \land ψ) \to (N + 1) \underset{˙}{\times} (A \underset{˙}{+} B) = (N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} (A \underset{˙}{+} B)$
28	24 6	mulgnn0cl	$⊢ (G \in Mnd \land N \in ℕ_{0} \land A \underset{˙}{+} B \in S) \to N \underset{˙}{\times} (A \underset{˙}{+} B) \in S$
29	17 11 21 28	syl3anc	$⊢ φ \to N \underset{˙}{\times} (A \underset{˙}{+} B) \in S$
30	29 8 9	3jca	$⊢ φ \to (N \underset{˙}{\times} (A \underset{˙}{+} B) \in S \land A \in S \land B \in S)$
31	7 30	jca	$⊢ φ \to (R \in SRing \land (N \underset{˙}{\times} (A \underset{˙}{+} B) \in S \land A \in S \land B \in S))$
32	31	adantr	$⊢ (φ \land ψ) \to (R \in SRing \land (N \underset{˙}{\times} (A \underset{˙}{+} B) \in S \land A \in S \land B \in S))$
33	1 4 2	srgdi	$⊢ (R \in SRing \land (N \underset{˙}{\times} (A \underset{˙}{+} B) \in S \land A \in S \land B \in S)) \to (N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} (A \underset{˙}{+} B) = ((N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} A) \underset{˙}{+} ((N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} B)$
34	32 33	syl	$⊢ (φ \land ψ) \to (N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} (A \underset{˙}{+} B) = ((N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} A) \underset{˙}{+} ((N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} B)$
35	27 34	eqtrd	$⊢ (φ \land ψ) \to (N + 1) \underset{˙}{\times} (A \underset{˙}{+} B) = ((N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} A) \underset{˙}{+} ((N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} B)$
36		elfzelz	$⊢ k \in (0 \dots N + 1) \to k \in ℤ$
37		bcpasc	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) + (\binom{N}{k - 1}) = (\binom{N + 1}{k})$
38	11 36 37	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) + (\binom{N}{k - 1}) = (\binom{N + 1}{k})$
39	38	oveq1d	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((\binom{N}{k}) + (\binom{N}{k - 1})) \underset{˙}{\cdot} (((N + 1 - 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))$
40	19	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to R \in Mnd$
41		bccl	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) \in ℕ_{0}$
42	11 36 41	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) \in ℕ_{0}$
43	36	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ℤ$
44		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
45	43 44	syl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k - 1 \in ℤ$
46		bccl	$⊢ (N \in ℕ_{0} \land k - 1 \in ℤ) \to (\binom{N}{k - 1}) \in ℕ_{0}$
47	11 45 46	syl2an2r	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℕ_{0}$
48	7	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to R \in SRing$
49	17	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to G \in Mnd$
50		fznn0sub	$⊢ k \in (0 \dots N + 1) \to N + 1 - k \in ℕ_{0}$
51	50	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to N + 1 - k \in ℕ_{0}$
52	8	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to A \in S$
53	24 6	mulgnn0cl	$⊢ (G \in Mnd \land N + 1 - k \in ℕ_{0} \land A \in S) \to (N + 1 - k) \underset{˙}{\times} A \in S$
54	49 51 52 53	syl3anc	$⊢ (φ \land k \in (0 \dots N + 1)) \to (N + 1 - k) \underset{˙}{\times} A \in S$
55		elfznn0	$⊢ k \in (0 \dots N + 1) \to k \in ℕ_{0}$
56	55	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ℕ_{0}$
57	9	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to B \in S$
58	24 6	mulgnn0cl	$⊢ (G \in Mnd \land k \in ℕ_{0} \land B \in S) \to k \underset{˙}{\times} B \in S$
59	49 56 57 58	syl3anc	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \underset{˙}{\times} B \in S$
60	1 2	srgcl	$⊢ (R \in SRing \land (N + 1 - k) \underset{˙}{\times} A \in S \land k \underset{˙}{\times} B \in S) \to ((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B) \in S$
61	48 54 59 60	syl3anc	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B) \in S$
62	1 3 4	mulgnn0dir	$⊢ (R \in Mnd \land ((\binom{N}{k}) \in ℕ_{0} \land (\binom{N}{k - 1}) \in ℕ_{0} \land ((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B) \in S)) \to ((\binom{N}{k}) + (\binom{N}{k - 1})) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) = ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{+} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
63	40 42 47 61 62	syl13anc	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((\binom{N}{k}) + (\binom{N}{k - 1})) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) = ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{+} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
64	39 63	eqtr3d	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N + 1}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) = ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{+} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
65	64	mpteq2dva	$⊢ φ \to (k \in (0 \dots N + 1) ⟼ (\binom{N + 1}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = (k \in (0 \dots N + 1) ⟼ ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{+} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
66	65	oveq2d	$⊢ φ \to {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N + 1}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = {\sum_{R}}_{k = 0}^{N + 1} (((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{+} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
67		srgcmn	$⊢ R \in SRing \to R \in CMnd$
68	7 67	syl	$⊢ φ \to R \in CMnd$
69		fzfid	$⊢ φ \to (0 \dots N + 1) \in Fin$
70	1 3	mulgnn0cl	$⊢ (R \in Mnd \land (\binom{N}{k}) \in ℕ_{0} \land ((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B) \in S) \to (\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
71	40 42 61 70	syl3anc	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
72	36 44	syl	$⊢ k \in (0 \dots N + 1) \to k - 1 \in ℤ$
73	11 72 46	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℕ_{0}$
74	1 3	mulgnn0cl	$⊢ (R \in Mnd \land (\binom{N}{k - 1}) \in ℕ_{0} \land ((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B) \in S) \to (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
75	40 73 61 74	syl3anc	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
76		eqid	$⊢ (k \in (0 \dots N + 1) ⟼ (\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = (k \in (0 \dots N + 1) ⟼ (\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
77		eqid	$⊢ (k \in (0 \dots N + 1) ⟼ (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = (k \in (0 \dots N + 1) ⟼ (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
78	1 4 68 69 71 75 76 77	gsummptfidmadd	$⊢ φ \to {\sum_{R}}_{k = 0}^{N + 1} (((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{+} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) = ({\sum_{R}}_{k = 0}^{N + 1}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} ({\sum_{R}}_{k = 0}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
79	66 78	eqtrd	$⊢ φ \to {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N + 1}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = ({\sum_{R}}_{k = 0}^{N + 1}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} ({\sum_{R}}_{k = 0}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
80	79	adantr	$⊢ (φ \land ψ) \to {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N + 1}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = ({\sum_{R}}_{k = 0}^{N + 1}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} ({\sum_{R}}_{k = 0}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
81	15 35 80	3eqtr4d	$⊢ (φ \land ψ) \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)))$

Metamath Proof Explorer

Theorem srgbinomlem

Proof