This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝑋 ) ) ) ) ) )