lply1binom

Description: The binomial theorem for linear polynomials (monic polynomials of degree 1) over commutative rings: ( X + A ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( X ^ k ) ) . (Contributed by AV, 25-Aug-2019)

	Ref	Expression
Hypotheses	cply1binom.p	$⊢ P = {Poly}_{1} (R)$
	cply1binom.x	$⊢ X = {var}_{1} (R)$
	cply1binom.a	$⊢ \underset{˙}{+} = +_{P}$
	cply1binom.m	$⊢ \underset{˙}{\times} = \cdot_{P}$
	cply1binom.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	cply1binom.g	$⊢ G = {mulGrp}_{P}$
	cply1binom.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
	cply1binom.b	$⊢ B = {Base}_{P}$
Assertion	lply1binom	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in B) \to N \underset{˙}{\times} (X \underset{˙}{+} A) = {\sum_{P}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} X)))$

Proof

Step	Hyp	Ref	Expression
1		cply1binom.p	$⊢ P = {Poly}_{1} (R)$
2		cply1binom.x	$⊢ X = {var}_{1} (R)$
3		cply1binom.a	$⊢ \underset{˙}{+} = +_{P}$
4		cply1binom.m	$⊢ \underset{˙}{\times} = \cdot_{P}$
5		cply1binom.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		cply1binom.g	$⊢ G = {mulGrp}_{P}$
7		cply1binom.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
8		cply1binom.b	$⊢ B = {Base}_{P}$
9		crngring	$⊢ R \in CRing \to R \in Ring$
10	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
11		ringcmn	$⊢ P \in Ring \to P \in CMnd$
12	9 10 11	3syl	$⊢ R \in CRing \to P \in CMnd$
13	12	3ad2ant1	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in B) \to P \in CMnd$
14	2 1 8	vr1cl	$⊢ R \in Ring \to X \in B$
15	9 14	syl	$⊢ R \in CRing \to X \in B$
16	15	3ad2ant1	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in B) \to X \in B$
17		simp3	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in B) \to A \in B$
18	8 3	cmncom	$⊢ (P \in CMnd \land X \in B \land A \in B) \to X \underset{˙}{+} A = A \underset{˙}{+} X$
19	13 16 17 18	syl3anc	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in B) \to X \underset{˙}{+} A = A \underset{˙}{+} X$
20	19	oveq2d	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in B) \to N \underset{˙}{\times} (X \underset{˙}{+} A) = N \underset{˙}{\times} (A \underset{˙}{+} X)$
21	1	ply1crng	$⊢ R \in CRing \to P \in CRing$
22	21	3ad2ant1	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in B) \to P \in CRing$
23		simp2	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in B) \to N \in ℕ_{0}$
24	8	eleq2i	$⊢ A \in B \leftrightarrow A \in {Base}_{P}$
25	24	biimpi	$⊢ A \in B \to A \in {Base}_{P}$
26	25	3ad2ant3	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in B) \to A \in {Base}_{P}$
27	15 8	eleqtrdi	$⊢ R \in CRing \to X \in {Base}_{P}$
28	27	3ad2ant1	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in B) \to X \in {Base}_{P}$
29		eqid	$⊢ {Base}_{P} = {Base}_{P}$
30	29 4 5 3 6 7	crngbinom	$⊢ ((P \in CRing \land N \in ℕ_{0}) \land (A \in {Base}_{P} \land X \in {Base}_{P})) \to N \underset{˙}{\times} (A \underset{˙}{+} X) = {\sum_{P}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} X)))$
31	22 23 26 28 30	syl22anc	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in B) \to N \underset{˙}{\times} (A \underset{˙}{+} X) = {\sum_{P}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} X)))$
32	20 31	eqtrd	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in B) \to N \underset{˙}{\times} (X \underset{˙}{+} A) = {\sum_{P}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} X)))$

Metamath Proof Explorer

Theorem lply1binom

Proof