Theorem 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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cply1binom.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	cply1binom.a	⊢ + = ( +g ‘ 𝑃 )
	cply1binom.m	⊢ × = ( .r ‘ 𝑃 )
	cply1binom.t	⊢ · = ( .g ‘ 𝑃 )
	cply1binom.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
	cply1binom.e	⊢ ↑ = ( .g ‘ 𝐺 )
	cply1binom.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion	lply1binom	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑁 ↑ ( 𝑋 + 𝐴 ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝑋 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cply1binom.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		cply1binom.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
3		cply1binom.a	⊢ + = ( +g ‘ 𝑃 )
4		cply1binom.m	⊢ × = ( .r ‘ 𝑃 )
5		cply1binom.t	⊢ · = ( .g ‘ 𝑃 )
6		cply1binom.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
7		cply1binom.e	⊢ ↑ = ( .g ‘ 𝐺 )
8		cply1binom.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
9		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
11		ringcmn	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
12	9 10 11	3syl	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CMnd )
13	12	3ad2ant1	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → 𝑃 ∈ CMnd )
14	2 1 8	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
15	9 14	syl	⊢ ( 𝑅 ∈ CRing → 𝑋 ∈ 𝐵 )
16	15	3ad2ant1	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
17		simp3	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
18	8 3	cmncom	⊢ ( ( 𝑃 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑋 + 𝐴 ) = ( 𝐴 + 𝑋 ) )
19	13 16 17 18	syl3anc	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑋 + 𝐴 ) = ( 𝐴 + 𝑋 ) )
20	19	oveq2d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑁 ↑ ( 𝑋 + 𝐴 ) ) = ( 𝑁 ↑ ( 𝐴 + 𝑋 ) ) )
21	1	ply1crng	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
22	21	3ad2ant1	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → 𝑃 ∈ CRing )
23		simp2	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → 𝑁 ∈ ℕ0 )
24	8	eleq2i	⊢ ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ( Base ‘ 𝑃 ) )
25	24	biimpi	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ ( Base ‘ 𝑃 ) )
26	25	3ad2ant3	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ ( Base ‘ 𝑃 ) )
27	15 8	eleqtrdi	⊢ ( 𝑅 ∈ CRing → 𝑋 ∈ ( Base ‘ 𝑃 ) )
28	27	3ad2ant1	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
29		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
30	29 4 5 3 6 7	crngbinom	⊢ ( ( ( 𝑃 ∈ CRing ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝐴 ∈ ( Base ‘ 𝑃 ) ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑁 ↑ ( 𝐴 + 𝑋 ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
31	22 23 26 28 30	syl22anc	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑁 ↑ ( 𝐴 + 𝑋 ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
32	20 31	eqtrd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑁 ↑ ( 𝑋 + 𝐴 ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝑋 ) ) ) ) ) )