srgbinom

Description: The binomial theorem for commuting elements of a semiring: ( A + B ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ k ) x. ( B ^ ( N - k ) ) (generalization of binom ). (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	srgbinom	⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_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		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 ↑ ( 𝐴 + 𝐵 ) ) = ( 0 ↑ ( 𝐴 + 𝐵 ) ) )
8		oveq2	⊢ ( 𝑥 = 0 → ( 0 ... 𝑥 ) = ( 0 ... 0 ) )
9		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 C 𝑘 ) = ( 0 C 𝑘 ) )
10		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 − 𝑘 ) = ( 0 − 𝑘 ) )
11	10	oveq1d	⊢ ( 𝑥 = 0 → ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) = ( ( 0 − 𝑘 ) ↑ 𝐴 ) )
12	11	oveq1d	⊢ ( 𝑥 = 0 → ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) )
13	9 12	oveq12d	⊢ ( 𝑥 = 0 → ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
14	8 13	mpteq12dv	⊢ ( 𝑥 = 0 → ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 0 ) ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
15	14	oveq2d	⊢ ( 𝑥 = 0 → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 0 ) ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
16	7 15	eqeq12d	⊢ ( 𝑥 = 0 → ( ( 𝑥 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ↔ ( 0 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 0 ) ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
17	16	imbi2d	⊢ ( 𝑥 = 0 → ( ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑥 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ↔ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 0 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 0 ) ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ) )
18		oveq1	⊢ ( 𝑥 = 𝑛 → ( 𝑥 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) )
19		oveq2	⊢ ( 𝑥 = 𝑛 → ( 0 ... 𝑥 ) = ( 0 ... 𝑛 ) )
20		oveq1	⊢ ( 𝑥 = 𝑛 → ( 𝑥 C 𝑘 ) = ( 𝑛 C 𝑘 ) )
21		oveq1	⊢ ( 𝑥 = 𝑛 → ( 𝑥 − 𝑘 ) = ( 𝑛 − 𝑘 ) )
22	21	oveq1d	⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) = ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) )
23	22	oveq1d	⊢ ( 𝑥 = 𝑛 → ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) )
24	20 23	oveq12d	⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
25	19 24	mpteq12dv	⊢ ( 𝑥 = 𝑛 → ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
26	25	oveq2d	⊢ ( 𝑥 = 𝑛 → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
27	18 26	eqeq12d	⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ↔ ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
28	27	imbi2d	⊢ ( 𝑥 = 𝑛 → ( ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑥 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ↔ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ) )
29		oveq1	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 ↑ ( 𝐴 + 𝐵 ) ) = ( ( 𝑛 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) )
30		oveq2	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 0 ... 𝑥 ) = ( 0 ... ( 𝑛 + 1 ) ) )
31		oveq1	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 C 𝑘 ) = ( ( 𝑛 + 1 ) C 𝑘 ) )
32		oveq1	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 − 𝑘 ) = ( ( 𝑛 + 1 ) − 𝑘 ) )
33	32	oveq1d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) = ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) )
34	33	oveq1d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) )
35	31 34	oveq12d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
36	30 35	mpteq12dv	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ↦ ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
37	36	oveq2d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ↦ ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
38	29 37	eqeq12d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ↔ ( ( 𝑛 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ↦ ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
39	38	imbi2d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑥 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ↔ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( ( 𝑛 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ↦ ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ) )
40		oveq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) )
41		oveq2	⊢ ( 𝑥 = 𝑁 → ( 0 ... 𝑥 ) = ( 0 ... 𝑁 ) )
42		oveq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 C 𝑘 ) = ( 𝑁 C 𝑘 ) )
43		oveq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 − 𝑘 ) = ( 𝑁 − 𝑘 ) )
44	43	oveq1d	⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) = ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) )
45	44	oveq1d	⊢ ( 𝑥 = 𝑁 → ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) )
46	42 45	oveq12d	⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
47	41 46	mpteq12dv	⊢ ( 𝑥 = 𝑁 → ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
48	47	oveq2d	⊢ ( 𝑥 = 𝑁 → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
49	40 48	eqeq12d	⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ↔ ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
50	49	imbi2d	⊢ ( 𝑥 = 𝑁 → ( ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑥 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑥 ) ↦ ( ( 𝑥 C 𝑘 ) · ( ( ( 𝑥 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ↔ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ) )
51		simpr1	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → 𝐴 ∈ 𝑆 )
52	5 1	mgpbas	⊢ 𝑆 = ( Base ‘ 𝐺 )
53	51 52	eleqtrdi	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → 𝐴 ∈ ( Base ‘ 𝐺 ) )
54		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
55		eqid	⊢ ( 0_g ‘ 𝐺 ) = ( 0_g ‘ 𝐺 )
56	54 55 6	mulg0	⊢ ( 𝐴 ∈ ( Base ‘ 𝐺 ) → ( 0 ↑ 𝐴 ) = ( 0_g ‘ 𝐺 ) )
57	53 56	syl	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 0 ↑ 𝐴 ) = ( 0_g ‘ 𝐺 ) )
58		simpr2	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → 𝐵 ∈ 𝑆 )
59	58 52	eleqtrdi	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → 𝐵 ∈ ( Base ‘ 𝐺 ) )
60	54 55 6	mulg0	⊢ ( 𝐵 ∈ ( Base ‘ 𝐺 ) → ( 0 ↑ 𝐵 ) = ( 0_g ‘ 𝐺 ) )
61	59 60	syl	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 0 ↑ 𝐵 ) = ( 0_g ‘ 𝐺 ) )
62	57 61	oveq12d	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) = ( ( 0_g ‘ 𝐺 ) × ( 0_g ‘ 𝐺 ) ) )
63	62	oveq2d	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) = ( 1 · ( ( 0_g ‘ 𝐺 ) × ( 0_g ‘ 𝐺 ) ) ) )
64		eqid	⊢ ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝑅 )
65	1 64	srgidcl	⊢ ( 𝑅 ∈ SRing → ( 1_r ‘ 𝑅 ) ∈ 𝑆 )
66	65	ancli	⊢ ( 𝑅 ∈ SRing → ( 𝑅 ∈ SRing ∧ ( 1_r ‘ 𝑅 ) ∈ 𝑆 ) )
67	66	adantr	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑅 ∈ SRing ∧ ( 1_r ‘ 𝑅 ) ∈ 𝑆 ) )
68	1 2 64	srglidm	⊢ ( ( 𝑅 ∈ SRing ∧ ( 1_r ‘ 𝑅 ) ∈ 𝑆 ) → ( ( 1_r ‘ 𝑅 ) × ( 1_r ‘ 𝑅 ) ) = ( 1_r ‘ 𝑅 ) )
69	67 68	syl	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( ( 1_r ‘ 𝑅 ) × ( 1_r ‘ 𝑅 ) ) = ( 1_r ‘ 𝑅 ) )
70	69	oveq2d	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( ( 1_r ‘ 𝑅 ) × ( 1_r ‘ 𝑅 ) ) ) = ( 1 · ( 1_r ‘ 𝑅 ) ) )
71		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
72	71 64	srgidcl	⊢ ( 𝑅 ∈ SRing → ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
73	71 3	mulg1	⊢ ( ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) → ( 1 · ( 1_r ‘ 𝑅 ) ) = ( 1_r ‘ 𝑅 ) )
74	72 73	syl	⊢ ( 𝑅 ∈ SRing → ( 1 · ( 1_r ‘ 𝑅 ) ) = ( 1_r ‘ 𝑅 ) )
75	74	adantr	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( 1_r ‘ 𝑅 ) ) = ( 1_r ‘ 𝑅 ) )
76	70 75	eqtrd	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( ( 1_r ‘ 𝑅 ) × ( 1_r ‘ 𝑅 ) ) ) = ( 1_r ‘ 𝑅 ) )
77	5 64	ringidval	⊢ ( 1_r ‘ 𝑅 ) = ( 0_g ‘ 𝐺 )
78		id	⊢ ( ( 1_r ‘ 𝑅 ) = ( 0_g ‘ 𝐺 ) → ( 1_r ‘ 𝑅 ) = ( 0_g ‘ 𝐺 ) )
79	78 78	oveq12d	⊢ ( ( 1_r ‘ 𝑅 ) = ( 0_g ‘ 𝐺 ) → ( ( 1_r ‘ 𝑅 ) × ( 1_r ‘ 𝑅 ) ) = ( ( 0_g ‘ 𝐺 ) × ( 0_g ‘ 𝐺 ) ) )
80	79	oveq2d	⊢ ( ( 1_r ‘ 𝑅 ) = ( 0_g ‘ 𝐺 ) → ( 1 · ( ( 1_r ‘ 𝑅 ) × ( 1_r ‘ 𝑅 ) ) ) = ( 1 · ( ( 0_g ‘ 𝐺 ) × ( 0_g ‘ 𝐺 ) ) ) )
81	80 78	eqeq12d	⊢ ( ( 1_r ‘ 𝑅 ) = ( 0_g ‘ 𝐺 ) → ( ( 1 · ( ( 1_r ‘ 𝑅 ) × ( 1_r ‘ 𝑅 ) ) ) = ( 1_r ‘ 𝑅 ) ↔ ( 1 · ( ( 0_g ‘ 𝐺 ) × ( 0_g ‘ 𝐺 ) ) ) = ( 0_g ‘ 𝐺 ) ) )
82	77 81	ax-mp	⊢ ( ( 1 · ( ( 1_r ‘ 𝑅 ) × ( 1_r ‘ 𝑅 ) ) ) = ( 1_r ‘ 𝑅 ) ↔ ( 1 · ( ( 0_g ‘ 𝐺 ) × ( 0_g ‘ 𝐺 ) ) ) = ( 0_g ‘ 𝐺 ) )
83	76 82	sylib	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( ( 0_g ‘ 𝐺 ) × ( 0_g ‘ 𝐺 ) ) ) = ( 0_g ‘ 𝐺 ) )
84	63 83	eqtrd	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) = ( 0_g ‘ 𝐺 ) )
85		fz0sn	⊢ ( 0 ... 0 ) = { 0 }
86	85	a1i	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 0 ... 0 ) = { 0 } )
87	86	mpteq1d	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑘 ∈ ( 0 ... 0 ) ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ { 0 } ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
88	87	oveq2d	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 0 ) ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ { 0 } ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
89		srgmnd	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
90	89	adantr	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → 𝑅 ∈ Mnd )
91		c0ex	⊢ 0 ∈ V
92	91	a1i	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → 0 ∈ V )
93	77 65	eqeltrrid	⊢ ( 𝑅 ∈ SRing → ( 0_g ‘ 𝐺 ) ∈ 𝑆 )
94	93	adantr	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 0_g ‘ 𝐺 ) ∈ 𝑆 )
95	84 94	eqeltrd	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 )
96		oveq2	⊢ ( 𝑘 = 0 → ( 0 C 𝑘 ) = ( 0 C 0 ) )
97		0nn0	⊢ 0 ∈ ℕ₀
98		bcn0	⊢ ( 0 ∈ ℕ₀ → ( 0 C 0 ) = 1 )
99	97 98	ax-mp	⊢ ( 0 C 0 ) = 1
100	96 99	eqtrdi	⊢ ( 𝑘 = 0 → ( 0 C 𝑘 ) = 1 )
101		oveq2	⊢ ( 𝑘 = 0 → ( 0 − 𝑘 ) = ( 0 − 0 ) )
102		0m0e0	⊢ ( 0 − 0 ) = 0
103	101 102	eqtrdi	⊢ ( 𝑘 = 0 → ( 0 − 𝑘 ) = 0 )
104	103	oveq1d	⊢ ( 𝑘 = 0 → ( ( 0 − 𝑘 ) ↑ 𝐴 ) = ( 0 ↑ 𝐴 ) )
105		oveq1	⊢ ( 𝑘 = 0 → ( 𝑘 ↑ 𝐵 ) = ( 0 ↑ 𝐵 ) )
106	104 105	oveq12d	⊢ ( 𝑘 = 0 → ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) )
107	100 106	oveq12d	⊢ ( 𝑘 = 0 → ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( 1 · ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) )
108	1 107	gsumsn	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ V ∧ ( 1 · ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 ) → ( 𝑅 Σ_g ( 𝑘 ∈ { 0 } ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( 1 · ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) )
109	90 92 95 108	syl3anc	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑅 Σ_g ( 𝑘 ∈ { 0 } ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( 1 · ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) )
110	88 109	eqtrd	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 0 ) ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( 1 · ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) )
111	1 4	mndcl	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 + 𝐵 ) ∈ 𝑆 )
112	90 51 58 111	syl3anc	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑆 )
113	112 52	eleqtrdi	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝐴 + 𝐵 ) ∈ ( Base ‘ 𝐺 ) )
114	54 55 6	mulg0	⊢ ( ( 𝐴 + 𝐵 ) ∈ ( Base ‘ 𝐺 ) → ( 0 ↑ ( 𝐴 + 𝐵 ) ) = ( 0_g ‘ 𝐺 ) )
115	113 114	syl	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 0 ↑ ( 𝐴 + 𝐵 ) ) = ( 0_g ‘ 𝐺 ) )
116	84 110 115	3eqtr4rd	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 0 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 0 ) ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
117		simprl	⊢ ( ( 𝑛 ∈ ℕ₀ ∧ ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) ) → 𝑅 ∈ SRing )
118	51	adantl	⊢ ( ( 𝑛 ∈ ℕ₀ ∧ ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) ) → 𝐴 ∈ 𝑆 )
119	58	adantl	⊢ ( ( 𝑛 ∈ ℕ₀ ∧ ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) ) → 𝐵 ∈ 𝑆 )
120		simprr3	⊢ ( ( 𝑛 ∈ ℕ₀ ∧ ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) ) → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
121		simpl	⊢ ( ( 𝑛 ∈ ℕ₀ ∧ ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) ) → 𝑛 ∈ ℕ₀ )
122		id	⊢ ( ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) → ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
123	1 2 3 4 5 6 117 118 119 120 121 122	srgbinomlem	⊢ ( ( ( 𝑛 ∈ ℕ₀ ∧ ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) ) ∧ ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) → ( ( 𝑛 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ↦ ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
124	123	exp31	⊢ ( 𝑛 ∈ ℕ₀ → ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) → ( ( 𝑛 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ↦ ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ) )
125	124	a2d	⊢ ( 𝑛 ∈ ℕ₀ → ( ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) → ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( ( 𝑛 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ↦ ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ) )
126	17 28 39 50 116 125	nn0ind	⊢ ( 𝑁 ∈ ℕ₀ → ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
127	126	expd	⊢ ( 𝑁 ∈ ℕ₀ → ( 𝑅 ∈ SRing → ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ) )
128	127	impcom	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ₀ ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
129	128	imp	⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )

Metamath Proof Explorer

Theorem srgbinom

Proof