Metamath Proof Explorer

Theorem srgbinomlem3

Description: Lemma 3 for srgbinomlem . (Contributed by AV, 23-Aug-2019) (Proof shortened by AV, 27-Oct-2019)

Ref Expression
Hypotheses srgbinom.s ⊢ 𝑆 = ( Base ‘ 𝑅 )
srgbinom.m ⊢ × = ( .r ‘ 𝑅 )
srgbinom.t ⊢ · = ( .g ‘ 𝑅 )
srgbinom.a ⊢ + = ( +g ‘ 𝑅 )
srgbinom.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
srgbinom.e ⊢ ↑ = ( .g ‘ 𝐺 )
srgbinomlem.r ⊢ ( 𝜑 → 𝑅 ∈ SRing )
srgbinomlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
srgbinomlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
srgbinomlem.c ⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
srgbinomlem.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
srgbinomlem.i ⊢ ( 𝜓 → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
Assertion srgbinomlem3 ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐴 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )

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 srgbinomlem.r ⊢ ( 𝜑 → 𝑅 ∈ SRing )
8 srgbinomlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
9 srgbinomlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
10 srgbinomlem.c ⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
11 srgbinomlem.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12 srgbinomlem.i ⊢ ( 𝜓 → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
13 12 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
14 13 oveq1d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐴 ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) × 𝐴 ) )
15 srgcmn ⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ CMnd )
16 7 15 syl ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
17 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝜑 )
18 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
19 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
20 11 18 19 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
21 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
23 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ0 )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
25 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑁 C 𝑘 ) ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
26 17 20 22 24 25 syl13anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
27 1 4 16 11 26 gsummptfzsplit ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ { ( 𝑁 + 1 ) } ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
28 srgmnd ⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
29 7 28 syl ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
30 ovexd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ V )
31 id ⊢ ( 𝜑 → 𝜑 )
32 11 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
33 32 peano2zd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
34 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑁 + 1 ) ) ∈ ℕ0 )
35 11 33 34 syl2anc ⊢ ( 𝜑 → ( 𝑁 C ( 𝑁 + 1 ) ) ∈ ℕ0 )
36 11 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
37 peano2cn ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 + 1 ) ∈ ℂ )
38 36 37 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℂ )
39 38 subidd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) = 0 )
40 0nn0 ⊢ 0 ∈ ℕ0
41 39 40 eqeltrdi ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ∈ ℕ0 )
42 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
43 11 42 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
44 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑁 C ( 𝑁 + 1 ) ) ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) ) → ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ) ∈ 𝑆 )
45 31 35 41 43 44 syl13anc ⊢ ( 𝜑 → ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ) ∈ 𝑆 )
46 oveq2 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝑁 C 𝑘 ) = ( 𝑁 C ( 𝑁 + 1 ) ) )
47 oveq2 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( 𝑁 + 1 ) − 𝑘 ) = ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) )
48 47 oveq1d ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) = ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) )
49 oveq1 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝑘 ↑ 𝐵 ) = ( ( 𝑁 + 1 ) ↑ 𝐵 ) )
50 48 49 oveq12d ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) )
51 46 50 oveq12d ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ) )
52 1 51 gsumsn ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑁 + 1 ) ∈ V ∧ ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ) ∈ 𝑆 ) → ( 𝑅 Σg ( 𝑘 ∈ { ( 𝑁 + 1 ) } ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ) )
53 29 30 45 52 syl3anc ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ { ( 𝑁 + 1 ) } ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ) )
54 11 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
55 54 ltp1d ⊢ ( 𝜑 → 𝑁 < ( 𝑁 + 1 ) )
56 55 olcd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) < 0 ∨ 𝑁 < ( 𝑁 + 1 ) ) )
57 bcval4 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ ( ( 𝑁 + 1 ) < 0 ∨ 𝑁 < ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑁 + 1 ) ) = 0 )
58 11 33 56 57 syl3anc ⊢ ( 𝜑 → ( 𝑁 C ( 𝑁 + 1 ) ) = 0 )
59 58 oveq1d ⊢ ( 𝜑 → ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ) = ( 0 · ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ) )
60 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem1 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) ) → ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ∈ 𝑆 )
61 31 41 43 60 syl12anc ⊢ ( 𝜑 → ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ∈ 𝑆 )
62 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
63 1 62 3 mulg0 ⊢ ( ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ∈ 𝑆 → ( 0 · ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ) = ( 0g ‘ 𝑅 ) )
64 61 63 syl ⊢ ( 𝜑 → ( 0 · ( ( ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ↑ 𝐴 ) × ( ( 𝑁 + 1 ) ↑ 𝐵 ) ) ) = ( 0g ‘ 𝑅 ) )
65 53 59 64 3eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ { ( 𝑁 + 1 ) } ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( 0g ‘ 𝑅 ) )
66 65 oveq2d ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ { ( 𝑁 + 1 ) } ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 0g ‘ 𝑅 ) ) )
67 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
68 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝜑 )
69 bccl2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝑘 ) ∈ ℕ )
70 69 nnnn0d ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
71 70 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
72 fzelp1 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
73 72 22 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
74 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
75 74 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
76 68 71 73 75 25 syl13anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
77 76 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
78 1 16 67 77 gsummptcl ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ∈ 𝑆 )
79 1 4 62 mndrid ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ∈ 𝑆 ) → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 0g ‘ 𝑅 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
80 29 78 79 syl2anc ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 0g ‘ 𝑅 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
81 27 66 80 3eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
82 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑅 ∈ SRing )
83 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ 𝑆 )
84 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ 𝑆 )
85 10 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
86 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
87 86 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
88 1 2 5 6 82 83 84 75 85 87 3 71 srgpcomppsc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) × 𝐴 ) = ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 − 𝑘 ) + 1 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
89 36 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℂ )
90 1cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 1 ∈ ℂ )
91 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℤ )
92 91 zcnd ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℂ )
93 92 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
94 89 90 93 addsubd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) = ( ( 𝑁 − 𝑘 ) + 1 ) )
95 94 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) = ( ( ( 𝑁 − 𝑘 ) + 1 ) ↑ 𝐴 ) )
96 95 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( ( ( 𝑁 − 𝑘 ) + 1 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) )
97 96 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 − 𝑘 ) + 1 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
98 88 97 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) × 𝐴 ) = ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
99 98 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) × 𝐴 ) ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
100 99 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) × 𝐴 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
101 ovexd ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
102 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑁 C 𝑘 ) ∈ ℕ0 ∧ ( 𝑁 − 𝑘 ) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
103 68 71 87 75 102 syl13anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
104 eqid ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
105 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ V )
106 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
107 104 67 105 106 fsuppmptdm ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
108 1 62 4 2 7 101 8 103 107 srgsummulcr ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) × 𝐴 ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) × 𝐴 ) )
109 81 100 108 3eqtr2rd ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) × 𝐴 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
110 109 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) × 𝐴 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
111 14 110 eqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐴 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )