lply1binomsc

Description: The binomial theorem for linear polynomials (monic polynomials of degree 1) over commutative rings, expressed by an element of this ring: ( 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}$
	lply1binomsc.k	$⊢ K = {Base}_{R}$
	lply1binomsc.s	$⊢ S = algSc (P)$
	lply1binomsc.h	$⊢ H = {mulGrp}_{R}$
	lply1binomsc.e	$⊢ E = \cdot_{H}$
Assertion	lply1binomsc	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to N \underset{˙}{\times} (X \underset{˙}{+} S (A)) = {\sum_{P}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (S ((N - k) E 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		lply1binomsc.k	$⊢ K = {Base}_{R}$
9		lply1binomsc.s	$⊢ S = algSc (P)$
10		lply1binomsc.h	$⊢ H = {mulGrp}_{R}$
11		lply1binomsc.e	$⊢ E = \cdot_{H}$
12		eqid	$⊢ Scalar (P) = Scalar (P)$
13		crngring	$⊢ R \in CRing \to R \in Ring$
14	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
15	13 14	syl	$⊢ R \in CRing \to P \in Ring$
16	15	3ad2ant1	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to P \in Ring$
17	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
18	13 17	syl	$⊢ R \in CRing \to P \in LMod$
19	18	3ad2ant1	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to P \in LMod$
20		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
21		eqid	$⊢ {Base}_{P} = {Base}_{P}$
22	9 12 16 19 20 21	asclf	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to S : {Base}_{Scalar (P)} ⟶ {Base}_{P}$
23	1	ply1sca	$⊢ R \in CRing \to R = Scalar (P)$
24	23	3ad2ant1	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to R = Scalar (P)$
25	24	fveq2d	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to {Base}_{R} = {Base}_{Scalar (P)}$
26	8 25	syl5eq	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to K = {Base}_{Scalar (P)}$
27	26	feq2d	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to (S : K ⟶ {Base}_{P} \leftrightarrow S : {Base}_{Scalar (P)} ⟶ {Base}_{P})$
28	22 27	mpbird	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to S : K ⟶ {Base}_{P}$
29		simp3	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to A \in K$
30	28 29	ffvelrnd	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to S (A) \in {Base}_{P}$
31	1 2 3 4 5 6 7 21	lply1binom	$⊢ (R \in CRing \land N \in ℕ_{0} \land S (A) \in {Base}_{P}) \to N \underset{˙}{\times} (X \underset{˙}{+} S (A)) = {\sum_{P}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} S (A)) \underset{˙}{\times} (k \underset{˙}{\times} X)))$
32	30 31	syld3an3	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to N \underset{˙}{\times} (X \underset{˙}{+} S (A)) = {\sum_{P}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} S (A)) \underset{˙}{\times} (k \underset{˙}{\times} X)))$
33	1	ply1assa	$⊢ R \in CRing \to P \in AssAlg$
34	33	3ad2ant1	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to P \in AssAlg$
35	34	adantr	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to P \in AssAlg$
36		fznn0sub	$⊢ k \in (0 \dots N) \to N - k \in ℕ_{0}$
37	36	adantl	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to N - k \in ℕ_{0}$
38	23	fveq2d	$⊢ R \in CRing \to {Base}_{R} = {Base}_{Scalar (P)}$
39	8 38	syl5eq	$⊢ R \in CRing \to K = {Base}_{Scalar (P)}$
40	39	eleq2d	$⊢ R \in CRing \to (A \in K \leftrightarrow A \in {Base}_{Scalar (P)})$
41	40	biimpa	$⊢ (R \in CRing \land A \in K) \to A \in {Base}_{Scalar (P)}$
42	41	3adant2	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to A \in {Base}_{Scalar (P)}$
43	42	adantr	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to A \in {Base}_{Scalar (P)}$
44		eqid	$⊢ 1_{P} = 1_{P}$
45	21 44	ringidcl	$⊢ P \in Ring \to 1_{P} \in {Base}_{P}$
46	15 45	syl	$⊢ R \in CRing \to 1_{P} \in {Base}_{P}$
47	46	3ad2ant1	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to 1_{P} \in {Base}_{P}$
48	47	adantr	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to 1_{P} \in {Base}_{P}$
49		eqid	$⊢ \cdot_{P} = \cdot_{P}$
50		eqid	$⊢ {mulGrp}_{Scalar (P)} = {mulGrp}_{Scalar (P)}$
51		eqid	$⊢ \cdot_{{mulGrp}_{Scalar (P)}} = \cdot_{{mulGrp}_{Scalar (P)}}$
52	21 12 20 49 50 51 6 7	assamulgscm	$⊢ (P \in AssAlg \land (N - k \in ℕ_{0} \land A \in {Base}_{Scalar (P)} \land 1_{P} \in {Base}_{P})) \to (N - k) \underset{˙}{\times} (A \cdot_{P} 1_{P}) = ((N - k) \cdot_{{mulGrp}_{Scalar (P)}} A) \cdot_{P} ((N - k) \underset{˙}{\times} 1_{P})$
53	35 37 43 48 52	syl13anc	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to (N - k) \underset{˙}{\times} (A \cdot_{P} 1_{P}) = ((N - k) \cdot_{{mulGrp}_{Scalar (P)}} A) \cdot_{P} ((N - k) \underset{˙}{\times} 1_{P})$
54	23	fveq2d	$⊢ R \in CRing \to {mulGrp}_{R} = {mulGrp}_{Scalar (P)}$
55	10 54	syl5eq	$⊢ R \in CRing \to H = {mulGrp}_{Scalar (P)}$
56	55	fveq2d	$⊢ R \in CRing \to \cdot_{H} = \cdot_{{mulGrp}_{Scalar (P)}}$
57	11 56	syl5eq	$⊢ R \in CRing \to E = \cdot_{{mulGrp}_{Scalar (P)}}$
58	57	3ad2ant1	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to E = \cdot_{{mulGrp}_{Scalar (P)}}$
59	58	adantr	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to E = \cdot_{{mulGrp}_{Scalar (P)}}$
60	59	eqcomd	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to \cdot_{{mulGrp}_{Scalar (P)}} = E$
61	60	oveqd	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to (N - k) \cdot_{{mulGrp}_{Scalar (P)}} A = (N - k) E A$
62	6	ringmgp	$⊢ P \in Ring \to G \in Mnd$
63	15 62	syl	$⊢ R \in CRing \to G \in Mnd$
64	63	3ad2ant1	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to G \in Mnd$
65	6 21	mgpbas	$⊢ {Base}_{P} = {Base}_{G}$
66	6 44	ringidval	$⊢ 1_{P} = 0_{G}$
67	65 7 66	mulgnn0z	$⊢ (G \in Mnd \land N - k \in ℕ_{0}) \to (N - k) \underset{˙}{\times} 1_{P} = 1_{P}$
68	64 36 67	syl2an	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to (N - k) \underset{˙}{\times} 1_{P} = 1_{P}$
69	61 68	oveq12d	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to ((N - k) \cdot_{{mulGrp}_{Scalar (P)}} A) \cdot_{P} ((N - k) \underset{˙}{\times} 1_{P}) = ((N - k) E A) \cdot_{P} 1_{P}$
70	53 69	eqtrd	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to (N - k) \underset{˙}{\times} (A \cdot_{P} 1_{P}) = ((N - k) E A) \cdot_{P} 1_{P}$
71	9 12 20 49 44	asclval	$⊢ A \in {Base}_{Scalar (P)} \to S (A) = A \cdot_{P} 1_{P}$
72	43 71	syl	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to S (A) = A \cdot_{P} 1_{P}$
73	72	oveq2d	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to (N - k) \underset{˙}{\times} S (A) = (N - k) \underset{˙}{\times} (A \cdot_{P} 1_{P})$
74	10	ringmgp	$⊢ R \in Ring \to H \in Mnd$
75	13 74	syl	$⊢ R \in CRing \to H \in Mnd$
76	75	3ad2ant1	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to H \in Mnd$
77	76	adantr	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to H \in Mnd$
78		simpr	$⊢ (R \in CRing \land A \in K) \to A \in K$
79	10 8	mgpbas	$⊢ K = {Base}_{H}$
80	78 79	eleqtrdi	$⊢ (R \in CRing \land A \in K) \to A \in {Base}_{H}$
81	80	3adant2	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to A \in {Base}_{H}$
82	81	adantr	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to A \in {Base}_{H}$
83		eqid	$⊢ {Base}_{H} = {Base}_{H}$
84	83 11	mulgnn0cl	$⊢ (H \in Mnd \land N - k \in ℕ_{0} \land A \in {Base}_{H}) \to (N - k) E A \in {Base}_{H}$
85	77 37 82 84	syl3anc	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to (N - k) E A \in {Base}_{H}$
86	24	adantr	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to R = Scalar (P)$
87	86	eqcomd	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to Scalar (P) = R$
88	87	fveq2d	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to {Base}_{Scalar (P)} = {Base}_{R}$
89		eqid	$⊢ {Base}_{R} = {Base}_{R}$
90	10 89	mgpbas	$⊢ {Base}_{R} = {Base}_{H}$
91	88 90	eqtrdi	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to {Base}_{Scalar (P)} = {Base}_{H}$
92	85 91	eleqtrrd	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to (N - k) E A \in {Base}_{Scalar (P)}$
93	9 12 20 49 44	asclval	$⊢ (N - k) E A \in {Base}_{Scalar (P)} \to S ((N - k) E A) = ((N - k) E A) \cdot_{P} 1_{P}$
94	92 93	syl	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to S ((N - k) E A) = ((N - k) E A) \cdot_{P} 1_{P}$
95	70 73 94	3eqtr4d	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to (N - k) \underset{˙}{\times} S (A) = S ((N - k) E A)$
96	95	oveq1d	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to ((N - k) \underset{˙}{\times} S (A)) \underset{˙}{\times} (k \underset{˙}{\times} X) = S ((N - k) E A) \underset{˙}{\times} (k \underset{˙}{\times} X)$
97	96	oveq2d	$⊢ ((R \in CRing \land N \in ℕ_{0} \land A \in K) \land k \in (0 \dots N)) \to (\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} S (A)) \underset{˙}{\times} (k \underset{˙}{\times} X)) = (\binom{N}{k}) \underset{˙}{\cdot} (S ((N - k) E A) \underset{˙}{\times} (k \underset{˙}{\times} X))$
98	97	mpteq2dva	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to (k \in (0 \dots N) ⟼ (\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} S (A)) \underset{˙}{\times} (k \underset{˙}{\times} X))) = (k \in (0 \dots N) ⟼ (\binom{N}{k}) \underset{˙}{\cdot} (S ((N - k) E A) \underset{˙}{\times} (k \underset{˙}{\times} X)))$
99	98	oveq2d	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to {\sum_{P}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} S (A)) \underset{˙}{\times} (k \underset{˙}{\times} X))) = {\sum_{P}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (S ((N - k) E A) \underset{˙}{\times} (k \underset{˙}{\times} X)))$
100	32 99	eqtrd	$⊢ (R \in CRing \land N \in ℕ_{0} \land A \in K) \to N \underset{˙}{\times} (X \underset{˙}{+} S (A)) = {\sum_{P}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (S ((N - k) E A) \underset{˙}{\times} (k \underset{˙}{\times} X)))$

Metamath Proof Explorer

Theorem lply1binomsc

Proof