Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lply1binom Structured version   Unicode version

Theorem lply1binom 18218
 Description: The binomial theorem for linear polynomials (monic polynomials of degree 1) over commutative rings: is the sum from to of . (Contributed by AV, 25-Aug-2019.)
Hypotheses
Ref Expression
cply1binom.p Poly1
cply1binom.x var1
cply1binom.a
cply1binom.m
cply1binom.t .g
cply1binom.g mulGrp
cply1binom.e .g
cply1binom.b
Assertion
Ref Expression
lply1binom g
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem lply1binom
StepHypRef Expression
1 crngring 17081 . . . . . 6
2 cply1binom.p . . . . . . 7 Poly1
32ply1ring 18159 . . . . . 6
4 ringcmn 17101 . . . . . 6 CMnd
51, 3, 43syl 20 . . . . 5 CMnd
653ad2ant1 1017 . . . 4 CMnd
7 cply1binom.x . . . . . . 7 var1
8 cply1binom.b . . . . . . 7
97, 2, 8vr1cl 18128 . . . . . 6
101, 9syl 16 . . . . 5
11103ad2ant1 1017 . . . 4
12 simp3 998 . . . 4
13 cply1binom.a . . . . 5
148, 13cmncom 16687 . . . 4 CMnd
156, 11, 12, 14syl3anc 1228 . . 3
1615oveq2d 6311 . 2
172ply1crng 18107 . . . 4
19 simp2 997 . . 3
208eleq2i 2545 . . . . 5
2120biimpi 194 . . . 4