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