Theorem crngbinom

Description: The binomial theorem for commutative rings (special case of csrgbinom ): ( A + B ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ k ) x. ( B ^ ( N - k ) ) . (Contributed by AV, 24-Aug-2019)

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

Proof

Step	Hyp	Ref	Expression
1		crngbinom.s	⊢ 𝑆 = ( Base ‘ 𝑅 )
2		crngbinom.m	⊢ × = ( .r ‘ 𝑅 )
3		crngbinom.t	⊢ · = ( .g ‘ 𝑅 )
4		crngbinom.a	⊢ + = ( +g ‘ 𝑅 )
5		crngbinom.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
6		crngbinom.e	⊢ ↑ = ( .g ‘ 𝐺 )
7		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
8		ringsrg	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ SRing )
9	7 8	syl	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ SRing )
10	9	adantr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ) → 𝑅 ∈ SRing )
11	5	crngmgp	⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ CMnd )
12	11	adantr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ) → 𝐺 ∈ CMnd )
13		simpr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
14	10 12 13	3jca	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ) → ( 𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ∧ 𝑁 ∈ ℕ0 ) )
15	1 2 3 4 5 6	csrgbinom	⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
16	14 15	sylan	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )