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 17 11 21	mulgnn0cld	$⊢ φ \to N \underset{˙}{\times} (A \underset{˙}{+} B) \in S$
29	28 8 9	3jca	$⊢ φ \to (N \underset{˙}{\times} (A \underset{˙}{+} B) \in S \land A \in S \land B \in S)$
30	7 29	jca	$⊢ φ \to (R \in SRing \land (N \underset{˙}{\times} (A \underset{˙}{+} B) \in S \land A \in S \land B \in S))$
31	30	adantr	$⊢ (φ \land ψ) \to (R \in SRing \land (N \underset{˙}{\times} (A \underset{˙}{+} B) \in S \land A \in S \land B \in S))$
32	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)$
33	31 32	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)$
34	27 33	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)$
35		elfzelz	$⊢ k \in (0 \dots N + 1) \to k \in ℤ$
36		bcpasc	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) + (\binom{N}{k - 1}) = (\binom{N + 1}{k})$
37	11 35 36	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) + (\binom{N}{k - 1}) = (\binom{N + 1}{k})$
38	37	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))$
39	19	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to R \in Mnd$
40		bccl	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) \in ℕ_{0}$
41	11 35 40	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) \in ℕ_{0}$
42	35	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ℤ$
43		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
44	42 43	syl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k - 1 \in ℤ$
45		bccl	$⊢ (N \in ℕ_{0} \land k - 1 \in ℤ) \to (\binom{N}{k - 1}) \in ℕ_{0}$
46	11 44 45	syl2an2r	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℕ_{0}$
47	7	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to R \in SRing$
48	17	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to G \in Mnd$
49		fznn0sub	$⊢ k \in (0 \dots N + 1) \to N + 1 - k \in ℕ_{0}$
50	49	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to N + 1 - k \in ℕ_{0}$
51	8	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to A \in S$
52	24 6 48 50 51	mulgnn0cld	$⊢ (φ \land k \in (0 \dots N + 1)) \to (N + 1 - k) \underset{˙}{\times} A \in S$
53		elfznn0	$⊢ k \in (0 \dots N + 1) \to k \in ℕ_{0}$
54	53	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ℕ_{0}$
55	9	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to B \in S$
56	24 6 48 54 55	mulgnn0cld	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \underset{˙}{\times} B \in S$
57	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$
58	47 52 56 57	syl3anc	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B) \in S$
59	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)))$
60	39 41 46 58 59	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)))$
61	38 60	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)))$
62	61	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))))$
63	62	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))))$
64		srgcmn	$⊢ R \in SRing \to R \in CMnd$
65	7 64	syl	$⊢ φ \to R \in CMnd$
66		fzfid	$⊢ φ \to (0 \dots N + 1) \in Fin$
67	1 3 39 41 58	mulgnn0cld	$⊢ (φ \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$
68	35 43	syl	$⊢ k \in (0 \dots N + 1) \to k - 1 \in ℤ$
69	11 68 45	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℕ_{0}$
70	1 3 39 69 58	mulgnn0cld	$⊢ (φ \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$
71		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)))$
72		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)))$
73	1 4 65 66 67 70 71 72	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))))$
74	63 73	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))))$
75	74	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))))$
76	15 34 75	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