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

Metamath Proof Explorer

Theorem lply1binom

Description: The binomial theorem for linear polynomials (monic polynomials of degree 1) over commutative rings: ( 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 )
cply1binom.b 
|- B = ( Base ` P )
Assertion lply1binom 
|- ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> ( N .^ ( X .+ A ) ) = ( P gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ 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 cply1binom.b 
 |-  B = ( Base ` P )
9 crngring 
 |-  ( R e. CRing -> R e. Ring )
10 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
11 ringcmn 
 |-  ( P e. Ring -> P e. CMnd )
12 9 10 11 3syl 
 |-  ( R e. CRing -> P e. CMnd )
13 12 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> P e. CMnd )
14 2 1 8 vr1cl 
 |-  ( R e. Ring -> X e. B )
15 9 14 syl 
 |-  ( R e. CRing -> X e. B )
16 15 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> X e. B )
17 simp3 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> A e. B )
18 8 3 cmncom 
 |-  ( ( P e. CMnd /\ X e. B /\ A e. B ) -> ( X .+ A ) = ( A .+ X ) )
19 13 16 17 18 syl3anc 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> ( X .+ A ) = ( A .+ X ) )
20 19 oveq2d 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> ( N .^ ( X .+ A ) ) = ( N .^ ( A .+ X ) ) )
21 1 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
22 21 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> P e. CRing )
23 simp2 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> N e. NN0 )
24 8 eleq2i 
 |-  ( A e. B <-> A e. ( Base ` P ) )
25 24 biimpi 
 |-  ( A e. B -> A e. ( Base ` P ) )
26 25 3ad2ant3 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> A e. ( Base ` P ) )
27 15 8 eleqtrdi 
 |-  ( R e. CRing -> X e. ( Base ` P ) )
28 27 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> X e. ( Base ` P ) )
29 eqid 
 |-  ( Base ` P ) = ( Base ` P )
30 29 4 5 3 6 7 crngbinom 
 |-  ( ( ( P e. CRing /\ N e. NN0 ) /\ ( A e. ( Base ` P ) /\ X e. ( Base ` P ) ) ) -> ( N .^ ( A .+ X ) ) = ( P gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ X ) ) ) ) ) )
31 22 23 26 28 30 syl22anc 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> ( N .^ ( A .+ X ) ) = ( P gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ X ) ) ) ) ) )
32 20 31 eqtrd 
 |-  ( ( R e. CRing /\ N e. NN0 /\ A e. B ) -> ( N .^ ( X .+ A ) ) = ( P gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ X ) ) ) ) ) )