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

Metamath Proof Explorer

Theorem csrgbinom

Description: The binomial theorem for commutative semirings. (Contributed by AV, 24-Aug-2019)

Ref Expression
Hypotheses srgbinom.s ⊢ 𝑆 = ( Base ‘ 𝑅 )
srgbinom.m ⊢ × = ( .r ‘ 𝑅 )
srgbinom.t ⊢ · = ( .g ‘ 𝑅 )
srgbinom.a ⊢ + = ( +g ‘ 𝑅 )
srgbinom.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
srgbinom.e ⊢ ↑ = ( .g ‘ 𝐺 )
Assertion csrgbinom ( ( ( 𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 srgbinom.s ⊢ 𝑆 = ( Base ‘ 𝑅 )
2 srgbinom.m ⊢ × = ( .r ‘ 𝑅 )
3 srgbinom.t ⊢ · = ( .g ‘ 𝑅 )
4 srgbinom.a ⊢ + = ( +g ‘ 𝑅 )
5 srgbinom.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
6 srgbinom.e ⊢ ↑ = ( .g ‘ 𝐺 )
7 3simpb ⊢ ( ( 𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ∧ 𝑁 ∈ ℕ0 ) → ( 𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0 ) )
8 7 adantr ⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0 ) )
9 simprl ⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → 𝐴 ∈ 𝑆 )
10 simprr ⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → 𝐵 ∈ 𝑆 )
11 simpl2 ⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → 𝐺 ∈ CMnd )
12 5 1 mgpbas ⊢ 𝑆 = ( Base ‘ 𝐺 )
13 5 2 mgpplusg ⊢ × = ( +g ‘ 𝐺 )
14 12 13 cmncom ⊢ ( ( 𝐺 ∈ CMnd ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
15 11 9 10 14 syl3anc ⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
16 1 2 3 4 5 6 srgbinom ⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
17 8 9 10 15 16 syl13anc ⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )