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