Metamath Proof Explorer

Theorem 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 ∧ 𝑁 ∈ ℕ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 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 ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
56 54 55 6 mulg0 ⊢ ( 𝐴 ∈ ( Base ‘ 𝐺 ) → ( 0 ↑ 𝐴 ) = ( 0g ‘ 𝐺 ) )
57 53 56 syl ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 0 ↑ 𝐴 ) = ( 0g ‘ 𝐺 ) )
58 simpr2 ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → 𝐵 ∈ 𝑆 )
59 58 52 eleqtrdi ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → 𝐵 ∈ ( Base ‘ 𝐺 ) )
60 54 55 6 mulg0 ⊢ ( 𝐵 ∈ ( Base ‘ 𝐺 ) → ( 0 ↑ 𝐵 ) = ( 0g ‘ 𝐺 ) )
61 59 60 syl ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 0 ↑ 𝐵 ) = ( 0g ‘ 𝐺 ) )
62 57 61 oveq12d ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) = ( ( 0g ‘ 𝐺 ) × ( 0g ‘ 𝐺 ) ) )
63 62 oveq2d ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) = ( 1 · ( ( 0g ‘ 𝐺 ) × ( 0g ‘ 𝐺 ) ) ) )
64 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
65 1 64 srgidcl ⊢ ( 𝑅 ∈ SRing → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
66 65 ancli ⊢ ( 𝑅 ∈ SRing → ( 𝑅 ∈ SRing ∧ ( 1r ‘ 𝑅 ) ∈ 𝑆 ) )
67 66 adantr ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑅 ∈ SRing ∧ ( 1r ‘ 𝑅 ) ∈ 𝑆 ) )
68 1 2 64 srglidm ⊢ ( ( 𝑅 ∈ SRing ∧ ( 1r ‘ 𝑅 ) ∈ 𝑆 ) → ( ( 1r ‘ 𝑅 ) × ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
69 67 68 syl ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( ( 1r ‘ 𝑅 ) × ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
70 69 oveq2d ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( ( 1r ‘ 𝑅 ) × ( 1r ‘ 𝑅 ) ) ) = ( 1 · ( 1r ‘ 𝑅 ) ) )
71 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
72 71 64 srgidcl ⊢ ( 𝑅 ∈ SRing → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
73 71 3 mulg1 ⊢ ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) → ( 1 · ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
74 72 73 syl ⊢ ( 𝑅 ∈ SRing → ( 1 · ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
75 74 adantr ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
76 70 75 eqtrd ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( ( 1r ‘ 𝑅 ) × ( 1r ‘ 𝑅 ) ) ) = ( 1r ‘ 𝑅 ) )
77 5 64 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝐺 )
78 id ⊢ ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝐺 ) → ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝐺 ) )
79 78 78 oveq12d ⊢ ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝐺 ) → ( ( 1r ‘ 𝑅 ) × ( 1r ‘ 𝑅 ) ) = ( ( 0g ‘ 𝐺 ) × ( 0g ‘ 𝐺 ) ) )
80 79 oveq2d ⊢ ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝐺 ) → ( 1 · ( ( 1r ‘ 𝑅 ) × ( 1r ‘ 𝑅 ) ) ) = ( 1 · ( ( 0g ‘ 𝐺 ) × ( 0g ‘ 𝐺 ) ) ) )
81 80 78 eqeq12d ⊢ ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝐺 ) → ( ( 1 · ( ( 1r ‘ 𝑅 ) × ( 1r ‘ 𝑅 ) ) ) = ( 1r ‘ 𝑅 ) ↔ ( 1 · ( ( 0g ‘ 𝐺 ) × ( 0g ‘ 𝐺 ) ) ) = ( 0g ‘ 𝐺 ) ) )
82 77 81 ax-mp ⊢ ( ( 1 · ( ( 1r ‘ 𝑅 ) × ( 1r ‘ 𝑅 ) ) ) = ( 1r ‘ 𝑅 ) ↔ ( 1 · ( ( 0g ‘ 𝐺 ) × ( 0g ‘ 𝐺 ) ) ) = ( 0g ‘ 𝐺 ) )
83 76 82 sylib ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( ( 0g ‘ 𝐺 ) × ( 0g ‘ 𝐺 ) ) ) = ( 0g ‘ 𝐺 ) )
84 63 83 eqtrd ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) = ( 0g ‘ 𝐺 ) )
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 → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
94 93 adantr ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
95 84 94 eqeltrd ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 1 · ( ( 0 ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 )
96 oveq2 ⊢ ( 𝑘 = 0 → ( 0 C 𝑘 ) = ( 0 C 0 ) )
97 0nn0 ⊢ 0 ∈ ℕ0
98 bcn0 ⊢ ( 0 ∈ ℕ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 ↑ ( 𝐴 + 𝐵 ) ) = ( 0g ‘ 𝐺 ) )
115 113 114 syl ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 0 ↑ ( 𝐴 + 𝐵 ) ) = ( 0g ‘ 𝐺 ) )
116 84 110 115 3eqtr4rd ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 0 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 0 ) ↦ ( ( 0 C 𝑘 ) · ( ( ( 0 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
117 simprl ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) ) → 𝑅 ∈ SRing )
118 51 adantl ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) ) → 𝐴 ∈ 𝑆 )
119 58 adantl ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) ) → 𝐵 ∈ 𝑆 )
120 simprr3 ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) ) → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
121 simpl ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) ) → 𝑛 ∈ ℕ0 )
122 id ⊢ ( ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) → ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
123 1 2 3 4 5 6 117 118 119 120 121 122 srgbinomlem ⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) ) ∧ ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) → ( ( 𝑛 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ↦ ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
124 123 exp31 ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) → ( ( 𝑛 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ↦ ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ) )
125 124 a2d ⊢ ( 𝑛 ∈ ℕ0 → ( ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑛 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑛 C 𝑘 ) · ( ( ( 𝑛 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) → ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( ( 𝑛 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ↦ ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( ( ( 𝑛 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ) )
126 17 28 39 50 116 125 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
127 126 expd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑅 ∈ SRing → ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) ) )
128 127 impcom ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
129 128 imp ⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) ) ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )