This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lply1binomsc

Description: The binomial theorem for linear polynomials (monic polynomials of degree 1) over commutative rings, expressed by an element of this ring: ( X + A ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( X ^ k ) ) . (Contributed by AV, 25-Aug-2019)

Ref Expression
Hypotheses cply1binom.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cply1binom.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
cply1binom.a ⊢ + = ( +g ‘ 𝑃 )
cply1binom.m ⊢ × = ( .r ‘ 𝑃 )
cply1binom.t ⊢ · = ( .g ‘ 𝑃 )
cply1binom.g ⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
cply1binom.e ⊢ ↑ = ( .g ‘ 𝐺 )
lply1binomsc.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
lply1binomsc.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
lply1binomsc.h ⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
lply1binomsc.e ⊢ 𝐸 = ( .g ‘ 𝐻 )
Assertion lply1binomsc ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → ( 𝑁 ↑ ( 𝑋 + ( 𝑆 ‘ 𝐴 ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( 𝑆 ‘ ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ) × ( 𝑘 ↑ 𝑋 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cply1binom.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 cply1binom.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
3 cply1binom.a ⊢ + = ( +g ‘ 𝑃 )
4 cply1binom.m ⊢ × = ( .r ‘ 𝑃 )
5 cply1binom.t ⊢ · = ( .g ‘ 𝑃 )
6 cply1binom.g ⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
7 cply1binom.e ⊢ ↑ = ( .g ‘ 𝐺 )
8 lply1binomsc.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
9 lply1binomsc.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
10 lply1binomsc.h ⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
11 lply1binomsc.e ⊢ 𝐸 = ( .g ‘ 𝐻 )
12 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
13 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
14 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15 13 14 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
16 15 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝑃 ∈ Ring )
17 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
18 13 17 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ LMod )
19 18 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝑃 ∈ LMod )
20 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
21 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
22 9 12 16 19 20 21 asclf ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝑆 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ ( Base ‘ 𝑃 ) )
23 1 ply1sca ⊢ ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
24 23 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
25 24 fveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
26 8 25 eqtrid ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
27 26 feq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → ( 𝑆 : 𝐾 ⟶ ( Base ‘ 𝑃 ) ↔ 𝑆 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ ( Base ‘ 𝑃 ) ) )
28 22 27 mpbird ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝑆 : 𝐾 ⟶ ( Base ‘ 𝑃 ) )
29 simp3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ 𝐾 )
30 28 29 ffvelcdmd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → ( 𝑆 ‘ 𝐴 ) ∈ ( Base ‘ 𝑃 ) )
31 1 2 3 4 5 6 7 21 lply1binom ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑆 ‘ 𝐴 ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝑁 ↑ ( 𝑋 + ( 𝑆 ‘ 𝐴 ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ ( 𝑆 ‘ 𝐴 ) ) × ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
32 30 31 syld3an3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → ( 𝑁 ↑ ( 𝑋 + ( 𝑆 ‘ 𝐴 ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ ( 𝑆 ‘ 𝐴 ) ) × ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
33 1 ply1assa ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ AssAlg )
34 33 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝑃 ∈ AssAlg )
35 34 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑃 ∈ AssAlg )
36 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
37 36 adantl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
38 23 fveq2d ⊢ ( 𝑅 ∈ CRing → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
39 8 38 eqtrid ⊢ ( 𝑅 ∈ CRing → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
40 39 eleq2d ⊢ ( 𝑅 ∈ CRing → ( 𝐴 ∈ 𝐾 ↔ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) )
41 40 biimpa ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
42 41 3adant2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
43 42 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
44 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
45 21 44 ringidcl ⊢ ( 𝑃 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
46 15 45 syl ⊢ ( 𝑅 ∈ CRing → ( 1r ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
47 46 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → ( 1r ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
48 47 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 1r ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
49 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
50 eqid ⊢ ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) = ( mulGrp ‘ ( Scalar ‘ 𝑃 ) )
51 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) ) = ( .g ‘ ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) )
52 21 12 20 49 50 51 6 7 assamulgscm ⊢ ( ( 𝑃 ∈ AssAlg ∧ ( ( 𝑁 − 𝑘 ) ∈ ℕ0 ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 1r ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝑁 − 𝑘 ) ↑ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) ) = ( ( ( 𝑁 − 𝑘 ) ( .g ‘ ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) ) 𝐴 ) ( ·𝑠 ‘ 𝑃 ) ( ( 𝑁 − 𝑘 ) ↑ ( 1r ‘ 𝑃 ) ) ) )
53 35 37 43 48 52 syl13anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) ↑ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) ) = ( ( ( 𝑁 − 𝑘 ) ( .g ‘ ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) ) 𝐴 ) ( ·𝑠 ‘ 𝑃 ) ( ( 𝑁 − 𝑘 ) ↑ ( 1r ‘ 𝑃 ) ) ) )
54 23 fveq2d ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) )
55 10 54 eqtrid ⊢ ( 𝑅 ∈ CRing → 𝐻 = ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) )
56 55 fveq2d ⊢ ( 𝑅 ∈ CRing → ( .g ‘ 𝐻 ) = ( .g ‘ ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) ) )
57 11 56 eqtrid ⊢ ( 𝑅 ∈ CRing → 𝐸 = ( .g ‘ ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) ) )
58 57 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝐸 = ( .g ‘ ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) ) )
59 58 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐸 = ( .g ‘ ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) ) )
60 59 eqcomd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( .g ‘ ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) ) = 𝐸 )
61 60 oveqd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) ( .g ‘ ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) ) 𝐴 ) = ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) )
62 6 ringmgp ⊢ ( 𝑃 ∈ Ring → 𝐺 ∈ Mnd )
63 15 62 syl ⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ Mnd )
64 63 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝐺 ∈ Mnd )
65 6 21 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝐺 )
66 6 44 ringidval ⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝐺 )
67 65 7 66 mulgnn0z ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑁 − 𝑘 ) ∈ ℕ0 ) → ( ( 𝑁 − 𝑘 ) ↑ ( 1r ‘ 𝑃 ) ) = ( 1r ‘ 𝑃 ) )
68 64 36 67 syl2an ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) ↑ ( 1r ‘ 𝑃 ) ) = ( 1r ‘ 𝑃 ) )
69 61 68 oveq12d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑁 − 𝑘 ) ( .g ‘ ( mulGrp ‘ ( Scalar ‘ 𝑃 ) ) ) 𝐴 ) ( ·𝑠 ‘ 𝑃 ) ( ( 𝑁 − 𝑘 ) ↑ ( 1r ‘ 𝑃 ) ) ) = ( ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
70 53 69 eqtrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) ↑ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) ) = ( ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
71 9 12 20 49 44 asclval ⊢ ( 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) → ( 𝑆 ‘ 𝐴 ) = ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
72 43 71 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑆 ‘ 𝐴 ) = ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
73 72 oveq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) ↑ ( 𝑆 ‘ 𝐴 ) ) = ( ( 𝑁 − 𝑘 ) ↑ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) ) )
74 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
75 10 ringmgp ⊢ ( 𝑅 ∈ Ring → 𝐻 ∈ Mnd )
76 13 75 syl ⊢ ( 𝑅 ∈ CRing → 𝐻 ∈ Mnd )
77 76 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝐻 ∈ Mnd )
78 77 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐻 ∈ Mnd )
79 simpr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ 𝐾 )
80 10 8 mgpbas ⊢ 𝐾 = ( Base ‘ 𝐻 )
81 79 80 eleqtrdi ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ ( Base ‘ 𝐻 ) )
82 81 3adant2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ ( Base ‘ 𝐻 ) )
83 82 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ( Base ‘ 𝐻 ) )
84 74 11 78 37 83 mulgnn0cld ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ∈ ( Base ‘ 𝐻 ) )
85 24 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
86 85 eqcomd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
87 86 fveq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
88 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
89 10 88 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐻 )
90 87 89 eqtrdi ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝐻 ) )
91 84 90 eleqtrrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
92 9 12 20 49 44 asclval ⊢ ( ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) → ( 𝑆 ‘ ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ) = ( ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
93 91 92 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑆 ‘ ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ) = ( ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
94 70 73 93 3eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) ↑ ( 𝑆 ‘ 𝐴 ) ) = ( 𝑆 ‘ ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ) )
95 94 oveq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑁 − 𝑘 ) ↑ ( 𝑆 ‘ 𝐴 ) ) × ( 𝑘 ↑ 𝑋 ) ) = ( ( 𝑆 ‘ ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ) × ( 𝑘 ↑ 𝑋 ) ) )
96 95 oveq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ ( 𝑆 ‘ 𝐴 ) ) × ( 𝑘 ↑ 𝑋 ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( 𝑆 ‘ ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ) × ( 𝑘 ↑ 𝑋 ) ) ) )
97 96 mpteq2dva ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ ( 𝑆 ‘ 𝐴 ) ) × ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( 𝑆 ‘ ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ) × ( 𝑘 ↑ 𝑋 ) ) ) ) )
98 97 oveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ ( 𝑆 ‘ 𝐴 ) ) × ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( 𝑆 ‘ ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ) × ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
99 32 98 eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → ( 𝑁 ↑ ( 𝑋 + ( 𝑆 ‘ 𝐴 ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( 𝑆 ‘ ( ( 𝑁 − 𝑘 ) 𝐸 𝐴 ) ) × ( 𝑘 ↑ 𝑋 ) ) ) ) ) )