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 
|- P = ( Poly1 ` R )
cply1binom.x 
|- X = ( var1 ` R )
cply1binom.a 
|- .+ = ( +g ` P )
cply1binom.m 
|- .X. = ( .r ` P )
cply1binom.t 
|- .x. = ( .g ` P )
cply1binom.g 
|- G = ( mulGrp ` P )
cply1binom.e 
|- .^ = ( .g ` G )
lply1binomsc.k 
|- K = ( Base ` R )
lply1binomsc.s 
|- S = ( algSc ` P )
lply1binomsc.h 
|- H = ( mulGrp ` R )
lply1binomsc.e 
|- E = ( .g ` H )
Assertion lply1binomsc 
|- ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> ( N .^ ( X .+ ( S ` A ) ) ) = ( P gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( S ` ( ( N - k ) E A ) ) .X. ( k .^ X ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cply1binom.p 
 |-  P = ( Poly1 ` R )
2 cply1binom.x 
 |-  X = ( var1 ` R )
3 cply1binom.a 
 |-  .+ = ( +g ` P )
4 cply1binom.m 
 |-  .X. = ( .r ` P )
5 cply1binom.t 
 |-  .x. = ( .g ` P )
6 cply1binom.g 
 |-  G = ( mulGrp ` P )
7 cply1binom.e 
 |-  .^ = ( .g ` G )
8 lply1binomsc.k 
 |-  K = ( Base ` R )
9 lply1binomsc.s 
 |-  S = ( algSc ` P )
10 lply1binomsc.h 
 |-  H = ( mulGrp ` R )
11 lply1binomsc.e 
 |-  E = ( .g ` H )
12 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
13 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
15 13 14 syl 
 |-  ( R e. CRing -> P e. Ring )
16 15 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> P e. Ring )
17 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
18 13 17 syl 
 |-  ( R e. CRing -> P e. LMod )
19 18 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> P e. LMod )
20 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
21 eqid 
 |-  ( Base ` P ) = ( Base ` P )
22 9 12 16 19 20 21 asclf 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> S : ( Base ` ( Scalar ` P ) ) --> ( Base ` P ) )
23 1 ply1sca 
 |-  ( R e. CRing -> R = ( Scalar ` P ) )
24 23 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> R = ( Scalar ` P ) )
25 24 fveq2d 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
26 8 25 syl5eq 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> K = ( Base ` ( Scalar ` P ) ) )
27 26 feq2d 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> ( S : K --> ( Base ` P ) <-> S : ( Base ` ( Scalar ` P ) ) --> ( Base ` P ) ) )
28 22 27 mpbird 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> S : K --> ( Base ` P ) )
29 simp3 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> A e. K )
30 28 29 ffvelrnd 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> ( S ` A ) e. ( Base ` P ) )
31 1 2 3 4 5 6 7 21 lply1binom 
 |-  ( ( R e. CRing /\ N e. NN0 /\ ( S ` A ) e. ( Base ` P ) ) -> ( N .^ ( X .+ ( S ` A ) ) ) = ( P gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ ( S ` A ) ) .X. ( k .^ X ) ) ) ) ) )
32 30 31 syld3an3 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> ( N .^ ( X .+ ( S ` A ) ) ) = ( P gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ ( S ` A ) ) .X. ( k .^ X ) ) ) ) ) )
33 1 ply1assa 
 |-  ( R e. CRing -> P e. AssAlg )
34 33 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> P e. AssAlg )
35 34 adantr 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> P e. AssAlg )
36 fznn0sub 
 |-  ( k e. ( 0 ... N ) -> ( N - k ) e. NN0 )
37 36 adantl 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( N - k ) e. NN0 )
38 23 fveq2d 
 |-  ( R e. CRing -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
39 8 38 syl5eq 
 |-  ( R e. CRing -> K = ( Base ` ( Scalar ` P ) ) )
40 39 eleq2d 
 |-  ( R e. CRing -> ( A e. K <-> A e. ( Base ` ( Scalar ` P ) ) ) )
41 40 biimpa 
 |-  ( ( R e. CRing /\ A e. K ) -> A e. ( Base ` ( Scalar ` P ) ) )
42 41 3adant2 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> A e. ( Base ` ( Scalar ` P ) ) )
43 42 adantr 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> A e. ( Base ` ( Scalar ` P ) ) )
44 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
45 21 44 ringidcl 
 |-  ( P e. Ring -> ( 1r ` P ) e. ( Base ` P ) )
46 15 45 syl 
 |-  ( R e. CRing -> ( 1r ` P ) e. ( Base ` P ) )
47 46 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> ( 1r ` P ) e. ( Base ` P ) )
48 47 adantr 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( 1r ` P ) e. ( Base ` P ) )
49 eqid 
 |-  ( .s ` P ) = ( .s ` P )
50 eqid 
 |-  ( mulGrp ` ( Scalar ` P ) ) = ( mulGrp ` ( Scalar ` P ) )
51 eqid 
 |-  ( .g ` ( mulGrp ` ( Scalar ` P ) ) ) = ( .g ` ( mulGrp ` ( Scalar ` P ) ) )
52 21 12 20 49 50 51 6 7 assamulgscm 
 |-  ( ( P e. AssAlg /\ ( ( N - k ) e. NN0 /\ A e. ( Base ` ( Scalar ` P ) ) /\ ( 1r ` P ) e. ( Base ` P ) ) ) -> ( ( N - k ) .^ ( A ( .s ` P ) ( 1r ` P ) ) ) = ( ( ( N - k ) ( .g ` ( mulGrp ` ( Scalar ` P ) ) ) A ) ( .s ` P ) ( ( N - k ) .^ ( 1r ` P ) ) ) )
53 35 37 43 48 52 syl13anc 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( ( N - k ) .^ ( A ( .s ` P ) ( 1r ` P ) ) ) = ( ( ( N - k ) ( .g ` ( mulGrp ` ( Scalar ` P ) ) ) A ) ( .s ` P ) ( ( N - k ) .^ ( 1r ` P ) ) ) )
54 23 fveq2d 
 |-  ( R e. CRing -> ( mulGrp ` R ) = ( mulGrp ` ( Scalar ` P ) ) )
55 10 54 syl5eq 
 |-  ( R e. CRing -> H = ( mulGrp ` ( Scalar ` P ) ) )
56 55 fveq2d 
 |-  ( R e. CRing -> ( .g ` H ) = ( .g ` ( mulGrp ` ( Scalar ` P ) ) ) )
57 11 56 syl5eq 
 |-  ( R e. CRing -> E = ( .g ` ( mulGrp ` ( Scalar ` P ) ) ) )
58 57 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> E = ( .g ` ( mulGrp ` ( Scalar ` P ) ) ) )
59 58 adantr 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> E = ( .g ` ( mulGrp ` ( Scalar ` P ) ) ) )
60 59 eqcomd 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( .g ` ( mulGrp ` ( Scalar ` P ) ) ) = E )
61 60 oveqd 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( ( N - k ) ( .g ` ( mulGrp ` ( Scalar ` P ) ) ) A ) = ( ( N - k ) E A ) )
62 6 ringmgp 
 |-  ( P e. Ring -> G e. Mnd )
63 15 62 syl 
 |-  ( R e. CRing -> G e. Mnd )
64 63 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> G e. Mnd )
65 6 21 mgpbas 
 |-  ( Base ` P ) = ( Base ` G )
66 6 44 ringidval 
 |-  ( 1r ` P ) = ( 0g ` G )
67 65 7 66 mulgnn0z 
 |-  ( ( G e. Mnd /\ ( N - k ) e. NN0 ) -> ( ( N - k ) .^ ( 1r ` P ) ) = ( 1r ` P ) )
68 64 36 67 syl2an 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( ( N - k ) .^ ( 1r ` P ) ) = ( 1r ` P ) )
69 61 68 oveq12d 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( ( ( N - k ) ( .g ` ( mulGrp ` ( Scalar ` P ) ) ) A ) ( .s ` P ) ( ( N - k ) .^ ( 1r ` P ) ) ) = ( ( ( N - k ) E A ) ( .s ` P ) ( 1r ` P ) ) )
70 53 69 eqtrd 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( ( N - k ) .^ ( A ( .s ` P ) ( 1r ` P ) ) ) = ( ( ( N - k ) E A ) ( .s ` P ) ( 1r ` P ) ) )
71 9 12 20 49 44 asclval 
 |-  ( A e. ( Base ` ( Scalar ` P ) ) -> ( S ` A ) = ( A ( .s ` P ) ( 1r ` P ) ) )
72 43 71 syl 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( S ` A ) = ( A ( .s ` P ) ( 1r ` P ) ) )
73 72 oveq2d 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( ( N - k ) .^ ( S ` A ) ) = ( ( N - k ) .^ ( A ( .s ` P ) ( 1r ` P ) ) ) )
74 10 ringmgp 
 |-  ( R e. Ring -> H e. Mnd )
75 13 74 syl 
 |-  ( R e. CRing -> H e. Mnd )
76 75 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> H e. Mnd )
77 76 adantr 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> H e. Mnd )
78 simpr 
 |-  ( ( R e. CRing /\ A e. K ) -> A e. K )
79 10 8 mgpbas 
 |-  K = ( Base ` H )
80 78 79 eleqtrdi 
 |-  ( ( R e. CRing /\ A e. K ) -> A e. ( Base ` H ) )
81 80 3adant2 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> A e. ( Base ` H ) )
82 81 adantr 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> A e. ( Base ` H ) )
83 eqid 
 |-  ( Base ` H ) = ( Base ` H )
84 83 11 mulgnn0cl 
 |-  ( ( H e. Mnd /\ ( N - k ) e. NN0 /\ A e. ( Base ` H ) ) -> ( ( N - k ) E A ) e. ( Base ` H ) )
85 77 37 82 84 syl3anc 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( ( N - k ) E A ) e. ( Base ` H ) )
86 24 adantr 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> R = ( Scalar ` P ) )
87 86 eqcomd 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( Scalar ` P ) = R )
88 87 fveq2d 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
89 eqid 
 |-  ( Base ` R ) = ( Base ` R )
90 10 89 mgpbas 
 |-  ( Base ` R ) = ( Base ` H )
91 88 90 eqtrdi 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` H ) )
92 85 91 eleqtrrd 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( ( N - k ) E A ) e. ( Base ` ( Scalar ` P ) ) )
93 9 12 20 49 44 asclval 
 |-  ( ( ( N - k ) E A ) e. ( Base ` ( Scalar ` P ) ) -> ( S ` ( ( N - k ) E A ) ) = ( ( ( N - k ) E A ) ( .s ` P ) ( 1r ` P ) ) )
94 92 93 syl 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( S ` ( ( N - k ) E A ) ) = ( ( ( N - k ) E A ) ( .s ` P ) ( 1r ` P ) ) )
95 70 73 94 3eqtr4d 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( ( N - k ) .^ ( S ` A ) ) = ( S ` ( ( N - k ) E A ) ) )
96 95 oveq1d 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( ( ( N - k ) .^ ( S ` A ) ) .X. ( k .^ X ) ) = ( ( S ` ( ( N - k ) E A ) ) .X. ( k .^ X ) ) )
97 96 oveq2d 
 |-  ( ( ( R e. CRing /\ N e. NN0 /\ A e. K ) /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) .x. ( ( ( N - k ) .^ ( S ` A ) ) .X. ( k .^ X ) ) ) = ( ( N _C k ) .x. ( ( S ` ( ( N - k ) E A ) ) .X. ( k .^ X ) ) ) )
98 97 mpteq2dva 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ ( S ` A ) ) .X. ( k .^ X ) ) ) ) = ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( S ` ( ( N - k ) E A ) ) .X. ( k .^ X ) ) ) ) )
99 98 oveq2d 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> ( P gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ ( S ` A ) ) .X. ( k .^ X ) ) ) ) ) = ( P gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( S ` ( ( N - k ) E A ) ) .X. ( k .^ X ) ) ) ) ) )
100 32 99 eqtrd 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. K ) -> ( N .^ ( X .+ ( S ` A ) ) ) = ( P gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( S ` ( ( N - k ) E A ) ) .X. ( k .^ X ) ) ) ) ) )