:: The Binomial Theorem for Algebraic Structures
:: by Christoph Schwarzweller
::
:: Received November 20, 2000
:: Copyright (c) 2000 Association of Mizar Users

registration

cluster non empty right_add-cancelable Abelian -> non empty left_add-cancelable addLoopStr ;
coherence
for b₁ being non empty addLoopStr st b₁ is Abelian & b₁ is right_add-cancelable holds
b₁ is left_add-cancelable

proof end;

cluster non empty left_add-cancelable Abelian -> non empty right_add-cancelable addLoopStr ;
coherence
for b₁ being non empty addLoopStr st b₁ is Abelian & b₁ is left_add-cancelable holds
b₁ is right_add-cancelable

proof end;

end;

registration

cluster non empty right_complementable add-associative right_zeroed -> non empty right_add-cancelable addLoopStr ;
coherence
for b₁ being non empty addLoopStr st b₁ is right_zeroed & b₁ is right_complementable & b₁ is add-associative holds
b₁ is right_add-cancelable ;

end;

registration

cluster non empty add-cancelable left_zeroed unital associative commutative distributive Abelian add-associative right_zeroed doubleLoopStr ;
existence
ex b₁ being non empty doubleLoopStr st
( b₁ is Abelian & b₁ is add-associative & b₁ is left_zeroed & b₁ is right_zeroed & b₁ is commutative & b₁ is associative & b₁ is add-cancelable & b₁ is distributive & b₁ is unital )

proof end;

end;

theorem Th1: :: BINOM:1

for R being non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr
for a being Element of R holds (0. R) * a = 0. R

proof end;

theorem Th2: :: BINOM:2

for R being non empty right_add-cancelable left_zeroed right-distributive doubleLoopStr
for a being Element of R holds a * (0. R) = 0. R

proof end;

scheme :: BINOM:sch 1
RecDef1{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of F₂(), F₄() -> Function of [:F₁(),F₂():],F₂() } :

ex g being Function of [:NAT ,F₁():],F₂() st
for a being Element of F₁() holds
( g . 0 ,a = F₃() & ( for n being Element of NAT holds g . (n + 1),a = F₄() . a,(g . n,a) ) )

proof end;

scheme :: BINOM:sch 2
RecDef2{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of F₂(), F₄() -> Function of [:F₂(),F₁():],F₂() } :

ex g being Function of [:F₁(),NAT :],F₂() st
for a being Element of F₁() holds
( g . a,0 = F₃() & ( for n being Element of NAT holds g . a,(n + 1) = F₄() . (g . a,n),a ) )

proof end;

theorem Th3: :: BINOM:3

for L being non empty left_zeroed addLoopStr
for a being Element of L holds Sum <*a*> = a

proof end;

theorem :: BINOM:4

for R being non empty right_add-cancelable left_zeroed right-distributive doubleLoopStr
for a being Element of R
for p being FinSequence of the carrier of R holds Sum (a * p) = a * (Sum p)

proof end;

theorem Th5: :: BINOM:5

for R being non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr
for a being Element of R
for p being FinSequence of the carrier of R holds Sum (p * a) = (Sum p) * a

proof end;

theorem :: BINOM:6

for R being non empty commutative doubleLoopStr
for a being Element of R
for p being FinSequence of the carrier of R holds Sum (p * a) = Sum (a * p)

proof end;

definition

canceled;
canceled;
canceled;
let R be non empty addLoopStr ;
let p, q be FinSequence of the carrier of R;
assume dom p = dom q ;
func p + q -> FinSequence of the carrier of R means :Def4: :: BINOM:def 4
( dom it = dom p & ( for i being Nat st 1 <= i & i <= len it holds
it /. i = (p /. i) + (q /. i) ) );
existence
ex b₁ being FinSequence of the carrier of R st
( dom b₁ = dom p & ( for i being Nat st 1 <= i & i <= len b₁ holds
b₁ /. i = (p /. i) + (q /. i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of R st dom b₁ = dom p & ( for i being Nat st 1 <= i & i <= len b₁ holds
b₁ /. i = (p /. i) + (q /. i) ) & dom b₂ = dom p & ( for i being Nat st 1 <= i & i <= len b₂ holds
b₂ /. i = (p /. i) + (q /. i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem BINOM:def 1 :

canceled;

:: deftheorem BINOM:def 2 :

canceled;

:: deftheorem BINOM:def 3 :

canceled;

:: deftheorem Def4 defines + BINOM:def 4 :

for R being non empty addLoopStr
for p, q being FinSequence of the carrier of R st dom p = dom q holds
for b₄ being FinSequence of the carrier of R holds
( b₄ = p + q iff ( dom b₄ = dom p & ( for i being Nat st 1 <= i & i <= len b₄ holds
b₄ /. i = (p /. i) + (q /. i) ) ) );

theorem Th7: :: BINOM:7

for R being non empty Abelian add-associative right_zeroed addLoopStr
for p, q being FinSequence of the carrier of R st dom p = dom q holds
Sum (p + q) = (Sum p) + (Sum q)

proof end;

definition

let R be non empty unital multMagma ;
let a be Element of R;
let n be Nat;
func a |^ n -> Element of R equals :: BINOM:def 5
(power R) . a,n;
coherence
(power R) . a,n is Element of R

proof end;

end;

:: deftheorem defines |^ BINOM:def 5 :

for R being non empty unital multMagma
for a being Element of R
for n being Nat holds a |^ n = (power R) . a,n;

theorem Th8: :: BINOM:8

for R being non empty unital multMagma
for a being Element of R holds
( a |^ 0 = 1_ R & a |^ 1 = a )

proof end;

theorem :: BINOM:9

canceled;

theorem :: BINOM:10

for R being non empty unital associative commutative multMagma
for a, b being Element of R
for n being Element of NAT holds (a * b) |^ n = (a |^ n) * (b |^ n)

proof end;

theorem Th11: :: BINOM:11

for R being non empty unital associative multMagma
for a being Element of R
for n, m being Element of NAT holds a |^ (n + m) = (a |^ n) * (a |^ m)

proof end;

theorem :: BINOM:12

for R being non empty unital associative multMagma
for a being Element of R
for n, m being Element of NAT holds (a |^ n) |^ m = a |^ (n * m)

proof end;

definition

let R be non empty addLoopStr ;
func Nat-mult-left R -> Function of [:NAT ,the carrier of R:],the carrier of R means :Def6: :: BINOM:def 6
for a being Element of R holds
( it . 0 ,a = 0. R & ( for n being Element of NAT holds it . (n + 1),a = a + (it . n,a) ) );
existence
ex b₁ being Function of [:NAT ,the carrier of R:],the carrier of R st
for a being Element of R holds
( b₁ . 0 ,a = 0. R & ( for n being Element of NAT holds b₁ . (n + 1),a = a + (b₁ . n,a) ) )

proof end;

uniqueness
for b₁, b₂ being Function of [:NAT ,the carrier of R:],the carrier of R st ( for a being Element of R holds
( b₁ . 0 ,a = 0. R & ( for n being Element of NAT holds b₁ . (n + 1),a = a + (b₁ . n,a) ) ) ) & ( for a being Element of R holds
( b₂ . 0 ,a = 0. R & ( for n being Element of NAT holds b₂ . (n + 1),a = a + (b₂ . n,a) ) ) ) holds
b₁ = b₂

proof end;

func Nat-mult-right R -> Function of [:the carrier of R,NAT :],the carrier of R means :Def7: :: BINOM:def 7
for a being Element of R holds
( it . a,0 = 0. R & ( for n being Element of NAT holds it . a,(n + 1) = (it . a,n) + a ) );
existence
ex b₁ being Function of [:the carrier of R,NAT :],the carrier of R st
for a being Element of R holds
( b₁ . a,0 = 0. R & ( for n being Element of NAT holds b₁ . a,(n + 1) = (b₁ . a,n) + a ) )

proof end;

uniqueness
for b₁, b₂ being Function of [:the carrier of R,NAT :],the carrier of R st ( for a being Element of R holds
( b₁ . a,0 = 0. R & ( for n being Element of NAT holds b₁ . a,(n + 1) = (b₁ . a,n) + a ) ) ) & ( for a being Element of R holds
( b₂ . a,0 = 0. R & ( for n being Element of NAT holds b₂ . a,(n + 1) = (b₂ . a,n) + a ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines Nat-mult-left BINOM:def 6 :

for R being non empty addLoopStr
for b₂ being Function of [:NAT ,the carrier of R:],the carrier of R holds
( b₂ = Nat-mult-left R iff for a being Element of R holds
( b₂ . 0 ,a = 0. R & ( for n being Element of NAT holds b₂ . (n + 1),a = a + (b₂ . n,a) ) ) );

:: deftheorem Def7 defines Nat-mult-right BINOM:def 7 :

for R being non empty addLoopStr
for b₂ being Function of [:the carrier of R,NAT :],the carrier of R holds
( b₂ = Nat-mult-right R iff for a being Element of R holds
( b₂ . a,0 = 0. R & ( for n being Element of NAT holds b₂ . a,(n + 1) = (b₂ . a,n) + a ) ) );

definition

let R be non empty addLoopStr ;
let a be Element of R;
let n be Element of NAT ;
func n * a -> Element of R equals :: BINOM:def 8
(Nat-mult-left R) . n,a;
coherence
(Nat-mult-left R) . n,a is Element of R ;
func a * n -> Element of R equals :: BINOM:def 9
(Nat-mult-right R) . a,n;
coherence
(Nat-mult-right R) . a,n is Element of R ;

end;

:: deftheorem defines * BINOM:def 8 :

for R being non empty addLoopStr
for a being Element of R
for n being Element of NAT holds n * a = (Nat-mult-left R) . n,a;

:: deftheorem defines * BINOM:def 9 :

for R being non empty addLoopStr
for a being Element of R
for n being Element of NAT holds a * n = (Nat-mult-right R) . a,n;

theorem :: BINOM:13

for R being non empty addLoopStr
for a being Element of R holds
( 0 * a = 0. R & a * 0 = 0. R ) by Def6, Def7;

theorem Th14: :: BINOM:14

for R being non empty right_zeroed addLoopStr
for a being Element of R holds 1 * a = a

proof end;

theorem Th15: :: BINOM:15

for R being non empty left_zeroed addLoopStr
for a being Element of R holds a * 1 = a

proof end;

theorem Th16: :: BINOM:16

for R being non empty left_zeroed add-associative addLoopStr
for a being Element of R
for n, m being Element of NAT holds (n + m) * a = (n * a) + (m * a)

proof end;

theorem Th17: :: BINOM:17

for R being non empty add-associative right_zeroed addLoopStr
for a being Element of R
for n, m being Element of NAT holds a * (n + m) = (a * n) + (a * m)

proof end;

theorem Th18: :: BINOM:18

for R being non empty left_zeroed add-associative right_zeroed addLoopStr
for a being Element of R
for n being Element of NAT holds n * a = a * n

proof end;

theorem :: BINOM:19

for R being non empty Abelian addLoopStr
for a being Element of R
for n being Element of NAT holds n * a = a * n

proof end;

theorem Th20: :: BINOM:20

for R being non empty left_add-cancelable left_zeroed left-distributive add-associative right_zeroed doubleLoopStr
for a, b being Element of R
for n being Element of NAT holds (n * a) * b = n * (a * b)

proof end;

theorem Th21: :: BINOM:21

for R being non empty right_add-cancelable left_zeroed distributive add-associative right_zeroed doubleLoopStr
for a, b being Element of R
for n being Element of NAT holds b * (n * a) = (b * a) * n

proof end;

theorem Th22: :: BINOM:22

for R being non empty add-cancelable left_zeroed distributive add-associative right_zeroed doubleLoopStr
for a, b being Element of R
for n being Element of NAT holds (a * n) * b = a * (n * b)

proof end;

definition

let k, n be Element of NAT ;
:: original: choose
redefine func n choose k -> Element of NAT ;
coherence
n choose k is Element of NAT by NEWTON:35;

end;

definition

let R be non empty unital doubleLoopStr ;
let a, b be Element of R;
let n be Element of NAT ;
func a,b In_Power n -> FinSequence of the carrier of R means :Def10: :: BINOM:def 10
( len it = n + 1 & ( for i, l, m being Element of NAT st i in dom it & m = i - 1 & l = n - m holds
it /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) );
existence
ex b₁ being FinSequence of the carrier of R st
( len b₁ = n + 1 & ( for i, l, m being Element of NAT st i in dom b₁ & m = i - 1 & l = n - m holds
b₁ /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of R st len b₁ = n + 1 & ( for i, l, m being Element of NAT st i in dom b₁ & m = i - 1 & l = n - m holds
b₁ /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len b₂ = n + 1 & ( for i, l, m being Element of NAT st i in dom b₂ & m = i - 1 & l = n - m holds
b₂ /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines In_Power BINOM:def 10 :

for R being non empty unital doubleLoopStr
for a, b being Element of R
for n being Element of NAT
for b₅ being FinSequence of the carrier of R holds
( b₅ = a,b In_Power n iff ( len b₅ = n + 1 & ( for i, l, m being Element of NAT st i in dom b₅ & m = i - 1 & l = n - m holds
b₅ /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) ) );

theorem Th23: :: BINOM:23

for R being non empty unital right_zeroed doubleLoopStr
for a, b being Element of R holds a,b In_Power 0 = <*(1_ R)*>

proof end;

theorem Th24: :: BINOM:24

for R being non empty unital right_zeroed doubleLoopStr
for a, b being Element of R
for n being Element of NAT holds (a,b In_Power n) . 1 = a |^ n

proof end;

theorem Th25: :: BINOM:25

for R being non empty unital right_zeroed doubleLoopStr
for a, b being Element of R
for n being Element of NAT holds (a,b In_Power n) . (n + 1) = b |^ n

proof end;

theorem :: BINOM:26

for R being non empty add-cancelable left_zeroed unital associative commutative distributive Abelian add-associative right_zeroed doubleLoopStr
for a, b being Element of R
for n being Element of NAT holds (a + b) |^ n = Sum (a,b In_Power n)

proof end;