:: BINOM semantic presentation

definition

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

end;

:: deftheorem Def1 BINOM:def 1 :

:: deftheorem Def2 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 b₁ being non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr
for b₂ being Element of b₁ holds (0. b₁) * b₂ = 0. b₁

proof end;

theorem Th2: :: BINOM:2

for b₁ being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr
for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁

proof end;

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

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

provided

E4: P₁[F₁()] and
E5: for b₁ being Nat st F₁() <= b₁ & P₁[b₁] holds
P₁[b₁ + 1]

proof end;

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

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

proof end;

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

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

proof end;

theorem Th3: :: BINOM:3

for b₁ being non empty left_zeroed LoopStr
for b₂ being Element of b₁ holds Sum <*b₂*> = b₂

proof end;

theorem Th4: :: BINOM:4

for b₁ being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr
for b₂ being Element of b₁
for b₃ being FinSequence of the carrier of b₁ holds Sum (b₂ * b₃) = b₂ * (Sum b₃)

proof end;

theorem Th5: :: BINOM:5

for b₁ being non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr
for b₂ being Element of b₁
for b₃ being FinSequence of the carrier of b₁ holds Sum (b₃ * b₂) = (Sum b₃) * b₂

proof end;

theorem Th6: :: BINOM:6

for b₁ being non empty commutative doubleLoopStr
for b₂ being Element of b₁
for b₃ being FinSequence of the carrier of b₁ holds Sum (b₃ * b₂) = Sum (b₂ * b₃)

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be FinSequence of the carrier of c₁;
assume dom c₂ = dom c₃ ;
func c₂ + c₃ -> FinSequence of the carrier of a₁ means :Def4: :: BINOM:def 4
( dom a₄ = dom a₂ & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₄ holds
a₄ /. b₁ = (a₂ /. b₁) + (a₃ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines + BINOM:def 4 :

theorem Th7: :: BINOM:7

for b₁ being non empty Abelian add-associative right_zeroed LoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ st dom b₂ = dom b₃ holds
Sum (b₂ + b₃) = (Sum b₂) + (Sum b₃)

proof end;

definition

let c₁ be non empty unital HGrStr ;
let c₂ be Element of c₁;
let c₃ be Nat;
func c₂ |^ c₃ -> Element of a₁ equals :: BINOM:def 5
(power a₁) . a₂,a₃;
coherence ;

end;

:: deftheorem Def5 defines |^ BINOM:def 5 :

theorem Th8: :: BINOM:8

for b₁ being non empty unital HGrStr
for b₂ being Element of b₁ holds
( b₂ |^ 0 = 1. b₁ & b₂ |^ 1 = b₂ )

proof end;

theorem Th9: :: BINOM:9

for b₁ being non empty unital HGrStr
for b₂ being Element of b₁
for b₃ being Nat holds b₂ |^ (b₃ + 1) = (b₂ |^ b₃) * b₂ by GROUP_1:def 8;

theorem Th10: :: BINOM:10

for b₁ being non empty unital associative commutative HGrStr
for b₂, b₃ being Element of b₁
for b₄ being Nat holds (b₂ * b₃) |^ b₄ = (b₂ |^ b₄) * (b₃ |^ b₄)

proof end;

theorem Th11: :: BINOM:11

for b₁ being non empty unital associative HGrStr
for b₂ being Element of b₁
for b₃, b₄ being Nat holds b₂ |^ (b₃ + b₄) = (b₂ |^ b₃) * (b₂ |^ b₄)

proof end;

theorem Th12: :: BINOM:12

for b₁ being non empty unital associative HGrStr
for b₂ being Element of b₁
for b₃, b₄ being Nat holds (b₂ |^ b₃) |^ b₄ = b₂ |^ (b₃ * b₄)

proof end;

definition

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

proof end;

uniqueness

proof end;

func Nat-mult-right c₁ -> Function of [:the carrier of a₁,NAT :],the carrier of a₁ means :Def7: :: BINOM:def 7
for b₁ being Element of a₁ holds
( a₂ . b₁,0 = 0. a₁ & ( for b₂ being Nat holds a₂ . b₁,(b₂ + 1) = (a₂ . b₁,b₂) + b₁ ) );
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 c₁ be non empty LoopStr ;
let c₂ be Element of c₁;
let c₃ be Nat;
func c₃ * c₂ -> Element of a₁ equals :: BINOM:def 8
(Nat-mult-left a₁) . a₃,a₂;
coherence ;
func c₂ * c₃ -> Element of a₁ equals :: BINOM:def 9
(Nat-mult-right a₁) . a₂,a₃;
coherence ;

end;

:: deftheorem Def8 defines * BINOM:def 8 :

:: deftheorem Def9 defines * BINOM:def 9 :

theorem Th13: :: BINOM:13

for b₁ being non empty LoopStr
for b₂ being Element of b₁ holds
( 0 * b₂ = 0. b₁ & b₂ * 0 = 0. b₁ ) by Def6, Def7;

theorem Th14: :: BINOM:14

for b₁ being non empty right_zeroed LoopStr
for b₂ being Element of b₁ holds 1 * b₂ = b₂

proof end;

theorem Th15: :: BINOM:15

for b₁ being non empty left_zeroed LoopStr
for b₂ being Element of b₁ holds b₂ * 1 = b₂

proof end;

Lemma16: for b₁ being non empty LoopStr
for b₂ being Element of b₁
for b₃ being Nat holds (b₃ + 1) * b₂ = b₂ + (b₃ * b₂)
by Def6;

Lemma17: for b₁ being non empty LoopStr
for b₂ being Element of b₁
for b₃ being Nat holds b₂ * (b₃ + 1) = (b₂ * b₃) + b₂
by Def7;

theorem Th16: :: BINOM:16

for b₁ being non empty add-associative left_zeroed LoopStr
for b₂ being Element of b₁
for b₃, b₄ being Nat holds (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂)

proof end;

theorem Th17: :: BINOM:17

for b₁ being non empty add-associative right_zeroed LoopStr
for b₂ being Element of b₁
for b₃, b₄ being Nat holds b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄)

proof end;

theorem Th18: :: BINOM:18

for b₁ being non empty add-associative right_zeroed left_zeroed LoopStr
for b₂ being Element of b₁
for b₃ being Nat holds b₃ * b₂ = b₂ * b₃

proof end;

theorem Th19: :: BINOM:19

for b₁ being non empty Abelian LoopStr
for b₂ being Element of b₁
for b₃ being Nat holds b₃ * b₂ = b₂ * b₃

proof end;

theorem Th20: :: BINOM:20

for b₁ being non empty add-associative right_zeroed left-distributive left_zeroed add-left-cancelable doubleLoopStr
for b₂, b₃ being Element of b₁
for b₄ being Nat holds (b₄ * b₂) * b₃ = b₄ * (b₂ * b₃)

proof end;

theorem Th21: :: BINOM:21

for b₁ being non empty add-associative right_zeroed distributive left_zeroed add-right-cancelable doubleLoopStr
for b₂, b₃ being Element of b₁
for b₄ being Nat holds b₃ * (b₄ * b₂) = (b₃ * b₂) * b₄

proof end;

theorem Th22: :: BINOM:22

for b₁ being non empty add-associative right_zeroed distributive left_zeroed add-cancelable doubleLoopStr
for b₂, b₃ being Element of b₁
for b₄ being Nat holds (b₂ * b₄) * b₃ = b₂ * (b₄ * b₃)

proof end;

definition

let c₁, c₂ be Nat;
redefine func choose as c₂ choose c₁ -> Nat;
coherence by NEWTON:35;

end;

definition

let c₁ be non empty unital doubleLoopStr ;
let c₂, c₃ be Element of c₁;
let c₄ be Nat;
func c₂,c₃ In_Power c₄ -> FinSequence of the carrier of a₁ means :Def10: :: BINOM:def 10
( len a₅ = a₄ + 1 & ( for b₁, b₂, b₃ being Nat st b₁ in dom a₅ & b₃ = b₁ - 1 & b₂ = a₄ - b₃ holds
a₅ /. b₁ = ((a₄ choose b₃) * (a₂ |^ b₂)) * (a₃ |^ b₃) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines In_Power BINOM:def 10 :

theorem Th23: :: BINOM:23

for b₁ being non empty right_zeroed unital doubleLoopStr
for b₂, b₃ being Element of b₁ holds b₂,b₃ In_Power 0 = <*(1. b₁)*>

proof end;

theorem Th24: :: BINOM:24

for b₁ being non empty right_zeroed unital doubleLoopStr
for b₂, b₃ being Element of b₁
for b₄ being Nat holds (b₂,b₃ In_Power b₄) . 1 = b₂ |^ b₄

proof end;

theorem Th25: :: BINOM:25

for b₁ being non empty right_zeroed unital doubleLoopStr
for b₂, b₃ being Element of b₁
for b₄ being Nat holds (b₂,b₃ In_Power b₄) . (b₄ + 1) = b₃ |^ b₄

proof end;

theorem Th26: :: BINOM:26

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

proof end;