:: BINOM semantic presentation

definition

let L be non empty LoopStr ;
canceled;
canceled;
attr L is add-cancelable means :Def3: :: BINOM:def 3
for a, b, c being Element of L holds
( ( a + b = a + c implies b = c ) & ( b + a = c + a implies b = c ) );

end;

:: deftheorem BINOM:def 1 :

:: deftheorem BINOM:def 2 :

:: deftheorem Def3 defines add-cancelable BINOM:def 3 :

registration

cluster non empty add-left-cancelable LoopStr ;
existence

proof end;

cluster non empty add-right-cancelable LoopStr ;
existence

proof end;

cluster non empty add-cancelable LoopStr ;
existence

proof end;

end;

registration

cluster non empty add-left-cancelable add-right-cancelable -> non empty add-cancelable LoopStr ;
coherence

proof end;

cluster non empty add-cancelable -> non empty add-left-cancelable add-right-cancelable LoopStr ;
coherence

proof end;

end;

registration

cluster non empty Abelian add-right-cancelable -> non empty add-left-cancelable LoopStr ;
coherence

proof end;

cluster non empty Abelian add-left-cancelable -> non empty add-right-cancelable LoopStr ;
coherence

proof end;

end;

registration

cluster non empty add-associative right_zeroed right_complementable -> non empty add-right-cancelable LoopStr ;
coherence

proof end;

end;

registration

cluster non empty Abelian add-associative right_zeroed unital associative commutative distributive left_zeroed add-left-cancelable add-right-cancelable add-cancelable doubleLoopStr ;
existence

proof end;

end;

theorem Th1: :: BINOM:1

for R being non empty right_zeroed left-distributive add-left-cancelable 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-distributive left_zeroed add-right-cancelable doubleLoopStr
for a being Element of R holds a * (0. R) = 0. R

proof end;

scheme :: BINOM:sch 1
Ind2{ F₁() -> Nat, P₁[ Nat] } :

for i being Nat st F₁() <= i holds
P₁[i]

provided

A1: P₁[F₁()] and
A2: for j being Nat st F₁() <= j & P₁[j] holds
P₁[j + 1]

proof end;

scheme :: BINOM:sch 2
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 Nat holds g . (n + 1),a = F₄() . a,(g . n,a) ) )

proof end;

scheme :: BINOM:sch 3
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 Nat holds g . a,(n + 1) = F₄() . (g . a,n),a ) )

proof end;

theorem Th3: :: BINOM:3

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

proof end;

theorem :: BINOM:4

for R being non empty right-distributive left_zeroed add-right-cancelable 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 right_zeroed left-distributive add-left-cancelable 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

let R be non empty LoopStr ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines + BINOM:def 4 :

theorem Th7: :: BINOM:7

for R being non empty Abelian add-associative right_zeroed LoopStr
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 HGrStr ;
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 ;

end;

:: deftheorem defines |^ BINOM:def 5 :

theorem Th8: :: BINOM:8

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

proof end;

theorem Th9: :: BINOM:9

for R being non empty unital HGrStr
for a being Element of R
for n being Nat holds a |^ (n + 1) = (a |^ n) * a by GROUP_1:def 8;

theorem :: BINOM:10

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

proof end;

theorem Th11: :: BINOM:11

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

proof end;

theorem :: BINOM:12

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

proof end;

definition

let R be non empty LoopStr ;
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 Nat holds it . (n + 1),a = a + (it . n,a) ) );
existence

proof end;

uniqueness

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 Nat holds it . a,(n + 1) = (it . a,n) + a ) );
existence

proof end;

uniqueness

proof end;

end;

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

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

definition

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

end;

:: deftheorem defines * BINOM:def 8 :

:: deftheorem defines * BINOM:def 9 :

theorem Th13: :: BINOM:13

for R being non empty LoopStr
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 LoopStr
for a being Element of R holds 1 * a = a

proof end;

theorem Th15: :: BINOM:15

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

proof end;

Lm1: for R being non empty LoopStr
for a being Element of R
for n being Nat holds (n + 1) * a = a + (n * a)
by Def6;

Lm2: for R being non empty LoopStr
for a being Element of R
for n being Nat holds a * (n + 1) = (a * n) + a
by Def7;

theorem Th16: :: BINOM:16

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

proof end;

theorem Th17: :: BINOM:17

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

proof end;

theorem Th18: :: BINOM:18

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

proof end;

theorem :: BINOM:19

for R being non empty Abelian LoopStr
for a being Element of R
for n being Nat holds n * a = a * n

proof end;

theorem Th20: :: BINOM:20

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

proof end;

theorem Th21: :: BINOM:21

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

proof end;

theorem Th22: :: BINOM:22

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

proof end;

definition

let k, n be Nat;
:: original: choose
redefine func n choose k -> Nat;
coherence by NEWTON:35;

end;

definition

let R be non empty unital doubleLoopStr ;
let a, b be Element of R;
let n be 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 Nat st i in dom it & m = i - 1 & l = n - m holds
it /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines In_Power BINOM:def 10 :

theorem Th23: :: BINOM:23

for R being non empty right_zeroed unital 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 right_zeroed unital doubleLoopStr
for a, b being Element of R
for n being Nat holds (a,b In_Power n) . 1 = a |^ n

proof end;

theorem Th25: :: BINOM:25

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

proof end;

theorem :: BINOM:26

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

proof end;