Copyright (c) 2000 Association of Mizar Users
environ
vocabulary RLVECT_1, ALGSTR_1, VECTSP_2, ARYTM_1, BINOP_1, LATTICES, GROUP_1,
VECTSP_1, ALGSTR_2, FUNCT_1, FUNCT_2, MCART_1, RELAT_1, FINSEQ_1,
FINSEQ_4, NEWTON, FINSEQ_2, BOOLE, BINOM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
STRUCT_0, FINSEQ_1, FUNCT_1, FUNCT_2, NAT_1, FINSEQ_4, RELSET_1, BINOP_1,
ALGSTR_1, FINSEQ_2, VECTSP_1, VECTSP_2, GROUP_1, NEWTON, RLVECT_1,
MCART_1, POLYNOM1;
constructors BINOP_1, REAL_1, ALGSTR_2, NEWTON, DOMAIN_1, POLYNOM1, MONOID_0,
MEMBERED;
clusters STRUCT_0, ALGSTR_1, RELSET_1, FUNCT_2, MONOID_0, FINSEQ_2, VECTSP_2,
INT_1, VECTSP_1, MEMBERED, ZFMISC_1, ORDINAL2, NUMBERS;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
theorems TARSKI, FUNCT_2, VECTSP_1, RLVECT_1, ALGSTR_1, NAT_1, MCART_1,
FINSEQ_1, AXIOMS, GROUP_1, NEWTON, FINSEQ_2, REAL_1, FINSEQ_4, BINOP_1,
FUNCT_1, ZFMISC_1, INT_1, RELSET_1, RELAT_1, POLYNOM1, XBOOLE_0,
XCMPLX_1;
schemes NAT_1, RECDEF_1, POLYNOM2;
begin :: Preliminaries
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let L be non empty LoopStr;
canceled 2;
attr L is add-cancelable means :Def3:
for a,b,c being Element of L
holds (a + b = a + c implies b = c) & (b + a = c + a implies b = c);
end;
definition
cluster add-left-cancelable (non empty LoopStr);
existence
proof
consider R being comRing;
take R;
thus thesis;
end;
cluster add-right-cancelable (non empty LoopStr);
existence
proof
consider R being comRing;
take R;
thus thesis;
end;
cluster add-cancelable (non empty LoopStr);
existence
proof
consider R being comRing;
take R;
now let a,b,c be Element of R;
now assume A1: b + a = c + a;
thus b = b + 0.R by RLVECT_1:def 7
.= b + (a + -a) by RLVECT_1:16
.= (c + a) + -a by A1,RLVECT_1:def 6
.= c + (a + -a) by RLVECT_1:def 6
.= c + 0.R by RLVECT_1:16
.= c by RLVECT_1:def 7;
end;
hence (a + b = a + c implies b = c) & (b + a = c + a implies b = c);
end;
hence thesis by Def3;
end;
end;
definition
cluster add-left-cancelable add-right-cancelable ->
add-cancelable (non empty LoopStr);
coherence
proof
let R be non empty LoopStr;
assume R is add-left-cancelable add-right-cancelable;
then for a,b,c being Element of R holds
(a + b = a + c implies b = c) & (b + a = c + a implies b = c)
by ALGSTR_1:def 6,def 7;
hence thesis by Def3;
end;
cluster add-cancelable ->
add-left-cancelable add-right-cancelable (non empty LoopStr);
coherence
proof
let R be non empty LoopStr;
assume R is add-cancelable;
then for a,b,c being Element of R
holds (a + b = a + c implies b = c) & (b + a = c + a implies b = c) by Def3;
hence thesis by ALGSTR_1:def 6,def 7;
end;
end;
definition
cluster Abelian add-right-cancelable ->
add-left-cancelable (non empty LoopStr);
coherence
proof
let R be non empty LoopStr;
assume A1: R is Abelian add-right-cancelable;
now let a,b,c be Element of R;
assume a + b = a + c;
then b + a = a + c by A1,RLVECT_1:def 5
.= c + a by A1,RLVECT_1:def 5;
hence b = c by A1,ALGSTR_1:def 7;
end;
hence thesis by ALGSTR_1:def 6;
end;
cluster Abelian add-left-cancelable ->
add-right-cancelable (non empty LoopStr);
coherence
proof
let R be non empty LoopStr;
assume A2: R is Abelian add-left-cancelable;
now let a,b,c be Element of R;
assume b + a = c + a;
then a + b = c + a by A2,RLVECT_1:def 5
.= a + c by A2,RLVECT_1:def 5;
hence b = c by A2,ALGSTR_1:def 6;
end;
hence thesis by ALGSTR_1:def 7;
end;
end;
definition
cluster right_zeroed right_complementable add-associative ->
add-right-cancelable (non empty LoopStr);
coherence
proof
let R be (non empty LoopStr);
assume A1: R is right_zeroed right_complementable add-associative;
now let a,b,c be Element of R;
assume A2: b + a = c + a;
thus b = b + 0.R by A1,RLVECT_1:def 7
.= b + (a + -a) by A1,RLVECT_1:16
.= (c + a) + -a by A1,A2,RLVECT_1:def 6
.= c + (a + -a) by A1,RLVECT_1:def 6
.= c + 0.R by A1,RLVECT_1:16
.= c by A1,RLVECT_1:def 7;
end;
hence thesis by ALGSTR_1:def 7;
end;
end;
definition
cluster Abelian add-associative left_zeroed right_zeroed
commutative associative add-cancelable
distributive unital (non empty doubleLoopStr);
existence
proof
consider R being comRing;
take R;
thus thesis;
end;
end;
theorem Th1:
for R being right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr),
a being Element of R
holds 0.R * a = 0.R
proof
let R be right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr),
a be Element of R;
0.R * a = (0.R + 0.R) * a by RLVECT_1:def 7
.= 0.R * a + 0.R * a by VECTSP_1:def 12;
then 0.R * a + 0.R * a = 0.R * a + 0.R by RLVECT_1:def 7;
hence 0.R * a = 0.R by ALGSTR_1:def 6;
end;
theorem Th2:
for R being left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
a being Element of R
holds a * 0.R = 0.R
proof
let R be left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
a be Element of R;
a * 0.R = a * (0.R + 0.R) by ALGSTR_1:def 5
.= a * 0.R + a * 0.R by VECTSP_1:def 11;
then a * 0.R + a * 0.R = 0.R + a * 0.R by ALGSTR_1:def 5;
hence thesis by ALGSTR_1:def 7;
end;
scheme Ind2{M() -> Nat, P[Nat]} :
for i being Nat st M() <= i holds P[i]
provided
A1:P[M()] and
A2:for j being Nat st M() <= j holds P[j] implies P[j+1]
proof
let i be Nat;
assume A3: M() <= i;
defpred Q[Nat] means P[M() + $1];
A4: Q[0] by A1;
A5: now let m be Nat;
assume A6: Q[m];
M() <= M() + m by NAT_1:29;
then P[(M() + m) + 1] by A2,A6;
hence Q[m+1] by XCMPLX_1:1;
end;
A7: for m being Nat holds Q[m] from Ind(A4,A5);
ex m being Nat st i = M() + m by A3,NAT_1:28;
hence thesis by A7;
end;
scheme RecDef1 {C,D() -> non empty set,
b() -> Element of D(),
F() -> Function of [:C(),D():],D()} :
ex g being Function of [:NAT,C():],D() st
for a being Element of C() holds g.(0,a) = b() &
for n being Nat holds g.(n+1,a) = F().(a,g.(n,a))
proof
A1: for a being Element of C() holds
ex f being Function of NAT,D()
st f.0 = b() &
for n being Nat holds f.(n+1) = F().(a,f.n)
proof
let a be Element of C();
defpred P[Nat,Element of D(),Element of D()] means $3 = F().(a,$2);
A2: for n being Nat for x being Element of D()
ex y being Element of D() st P[n,x,y];
ex f being Function of NAT,D() st
f.0 = b() &
for n being Element of NAT holds P[n,f.n,f.(n+1)] from RecExD(A2);
hence thesis;
end;
ex g being Function of C(),Funcs(NAT,D())
st for a being Element of C() holds
ex f being Function of NAT,D()
st g.a = f &
f.0 = b() &
for n being Nat holds f.(n+1) = F().(a,f.n)
proof
set h = {[a,l] where a is Element of C(),
l is Element of Funcs(NAT,D()) :
ex f being Function of NAT,D()
st f = l & f.0 = b() &
for n being Nat holds f.(n+1) = F().(a,f.n) };
A3: now let x,y1,y2 be set;
assume A4: [x,y1] in h & [x,y2] in h;
then consider a1 being Element of C(),
l1 being Element of Funcs(NAT,D()) such that
A5: [x,y1] = [a1,l1] &
ex f being Function of NAT,D()
st f = l1 & f.0 = b() &
for n being Nat holds f.(n+1) = F().(a1,f.n);
consider f1 being Function of NAT,D() such that
A6: f1 = l1 & f1.0 = b() &
for n being Nat holds f1.(n+1) = F().(a1,f1.n) by A5;
consider a2 being Element of C(),
l2 being Element of Funcs(NAT,D()) such that
A7: [x,y2] = [a2,l2] &
ex f being Function of NAT,D()
st f = l2 & f.0 = b() &
for n being Nat holds f.(n+1) = F().(a2,f.n) by A4;
consider f2 being Function of NAT,D() such that
A8: f2 = l2 & f2.0 = b() &
for n being Nat holds f2.(n+1) = F().(a2,f2.n) by A7;
A9: a1 = [x,y1]`1 by A5,MCART_1:def 1
.= x by MCART_1:def 1
.= [a2,l2]`1 by A7,MCART_1:def 1
.= a2 by MCART_1:def 1;
A10: NAT = dom f1 & NAT = dom f2 by FUNCT_2:def 1;
A11: now let x be set;
assume x in NAT;
then reconsider x' = x as Nat;
defpred _P[Nat] means f1.$1 = f2.$1 ;
A12: _P[0] by A6,A8;
A13: now let n be Nat;
assume A14: _P[n];
f1.(n+1) = F().(a2,f1.n) by A6,A9
.= f2.(n+1) by A8,A14;
hence _P[n+1];
end;
for n being Nat holds _P[n] from Ind(A12,A13);
hence f1.x = f2.x' .= f2.x;
end;
thus y1 = [a1,l1]`2 by A5,MCART_1:def 2
.= l1 by MCART_1:def 2
.= l2 by A6,A8,A10,A11,FUNCT_1:9
.= [x,y2]`2 by A7,MCART_1:def 2
.= y2 by MCART_1:def 2;
end;
now let x be set;
assume x in h;
then consider a being Element of C(),
l being Element of Funcs(NAT,D()) such that
A15: x = [a,l] &
ex f being Function of NAT,D()
st f = l & f.0 = b() &
for n being Nat holds f.(n+1) = F().(a,f.n);
thus x in [:C(),Funcs(NAT,D()):] by A15,ZFMISC_1:def 2;
end;
then h c= [:C(),Funcs(NAT,D()):] by TARSKI:def 3;
then reconsider h as Relation of C(),Funcs(NAT,D()) by RELSET_1:def 1;
A16: for x being set holds x in dom h implies x in C();
for x being set holds x in C() implies x in dom h
proof
let x be set;
assume A17: x in C();
then consider f being Function of NAT,D() such that
A18: f.0 = b() &
for n being Nat holds f.(n+1) = F().(x,f.n) by A1;
reconsider f' = f as Element of Funcs(NAT,D()) by FUNCT_2:11;
[x,f'] in h by A17,A18;
hence thesis by RELAT_1:def 4;
end;
then dom h = C() by A16,TARSKI:2;
then reconsider h as Function of C(),Funcs(NAT,D())
by A3,FUNCT_1:def 1,FUNCT_2:def 1;
take h;
for a being Element of C() holds
ex f being Function of NAT,D()
st h.a = f &
f.0 = b() &
for n being Nat holds f.(n+1) = F().(a,f.n)
proof
let a be Element of C();
dom h = C() by FUNCT_2:def 1;
then [a,h.a] in h by FUNCT_1:8;
then consider a' being Element of C(),
l being Element of Funcs(NAT,D()) such that
A19: [a,h.a] = [a',l] &
ex f' being Function of NAT,D()
st f' = l & f'.0 = b() &
for n being Nat holds f'.(n+1) = F().(a',f'.n);
consider f' being Function of NAT,D() such that
A20: f' = l & f'.0 = b() &
for n being Nat holds f'.(n+1) = F().(a',f'.n) by A19;
A21: a = [a',l]`1 by A19,MCART_1:def 1
.= a' by MCART_1:def 1;
h.a = [a',l]`2 by A19,MCART_1:def 2
.= l by MCART_1:def 2;
hence thesis by A20,A21;
end;
hence thesis;
end;
then consider g being Function of C(),Funcs(NAT,D()) such that
A22: for a being Element of C() holds
ex f being Function of NAT,D()
st g.a = f &
f.0 = b() &
for n being Nat holds f.(n+1) = F().(a,f.n);
set h = { [[n,a],z] where n is Nat, a is Element of C(), z is Element of D() :
ex f being Function of NAT,D() st f = g.a & z = f.n };
A23: now let x,y1,y2 be set;
assume A24: [x,y1] in h & [x,y2] in h;
then consider n1 being Nat,
a1 being Element of C(),
z1 being Element of D() such that
A25: [x,y1] = [[n1,a1],z1] &
ex f1 being Function of NAT,D() st f1 = g.a1 & z1 = f1.n1;
consider n2 being Nat,
a2 being Element of C(),
z2 being Element of D() such that
A26: [x,y2] = [[n2,a2],z2] &
ex f2 being Function of NAT,D() st f2 = g.a2 & z2 = f2.n2 by A24;
A27: [n1,a1] = [x,y1]`1 by A25,MCART_1:def 1
.= x by MCART_1:def 1
.= [[n2,a2],z2]`1 by A26,MCART_1:def 1
.= [n2,a2] by MCART_1:def 1;
then A28: n1 = [n2,a2]`1 by MCART_1:def 1
.= n2 by MCART_1:def 1;
a1 = [n2,a2]`2 by A27,MCART_1:def 2
.= a2 by MCART_1:def 2;
hence y1 = [x,y2]`2 by A25,A26,A28,MCART_1:def 2
.= y2 by MCART_1:def 2;
end;
now let x be set;
assume x in h;
then consider n1 being Nat,
a1 being Element of C(),
z1 being Element of D() such that
A29: x = [[n1,a1],z1] &
ex f1 being Function of NAT,D() st f1 = g.a1 & z1 = f1.n1;
[n1,a1] in [:NAT,C():] by ZFMISC_1:def 2;
hence x in [:[:NAT,C():],D():] by A29,ZFMISC_1:def 2;
end;
then h c= [:[:NAT,C():],D():] by TARSKI:def 3;
then reconsider h as Relation of [:NAT,C():],D() by RELSET_1:def 1;
A30: for x being set holds x in dom h implies x in [:NAT,C():];
for x being set holds x in [:NAT,C():] implies x in dom h
proof
let x be set;
assume x in [:NAT,C():];
then consider n,d being set such that
A31: n in NAT & d in C() & x = [n,d] by ZFMISC_1:def 2;
reconsider n as Nat by A31;
reconsider d as Element of C() by A31;
consider f' being Function of NAT,D() such that
A32: g.d = f' &
f'.0 = b() &
for n being Nat holds f'.(n+1) = F().(d,f'.n) by A22;
ex z being Element of D() st
ex f being Function of NAT,D() st f = g.d & z = f.n
proof
take f'.n;
take f';
thus thesis by A32;
end;
then consider z being Element of D() such that
A33: ex f being Function of NAT,D() st f = g.d & z = f.n;
[x,z] in h by A31,A33;
hence thesis by RELAT_1:def 4;
end;
then dom h = [:NAT,C():] by A30,TARSKI:2;
then reconsider h as Function of [:NAT,C():],D()
by A23,FUNCT_1:def 1,FUNCT_2:def 1;
take h;
for a being Element of C() holds h.(0,a) = b() &
for n being Nat holds h.(n+1,a) = F().(a,h.(n,a))
proof
let a be Element of C();
consider f' being Function of NAT,D() such that
A34: g.a = f' &
f'.0 = b() &
for n being Nat holds f'.(n+1) = F().(a,f'.n) by A22;
[0,a] in [:NAT,C():] by ZFMISC_1:def 2;
then [0,a] in dom h by FUNCT_2:def 1;
then consider u being set such that
A35: [[0,a],u] in h by RELAT_1:def 4;
consider n being Nat,
d being Element of C(),
z being Element of D() such that
A36: [[0,a],u] = [[n,d],z] &
ex f1 being Function of NAT,D() st f1 = g.d & z = f1.n by A35;
consider f1 being Function of NAT,D() such that
A37: f1 = g.d & z = f1.n by A36;
A38: [0,a] = [[n,d],z]`1 by A36,MCART_1:def 1
.= [n,d] by MCART_1:def 1;
then A39: n = [0,a]`1 by MCART_1:def 1
.= 0 by MCART_1:def 1;
A40: u = [[n,d],z]`2 by A36,MCART_1:def 2
.= z by MCART_1:def 2;
A41: d = [0,a]`2 by A38,MCART_1:def 2
.= a by MCART_1:def 2;
A42: h.(0,a) = h.[0,a] by BINOP_1:def 1
.= b() by A34,A35,A37,A39,A40,A41,FUNCT_1:8;
now let k be Nat;
[k+1,a] in [:NAT,C():] by ZFMISC_1:def 2;
then [k+1,a] in dom h by FUNCT_2:def 1;
then consider u being set such that
A43: [[k+1,a],u] in h by RELAT_1:def 4;
consider n being Nat,
d being Element of C(),
z being Element of D() such that
A44: [[k+1,a],u] = [[n,d],z] &
ex f1 being Function of NAT,D() st f1 = g.d & z = f1.n by A43;
consider f1 being Function of NAT,D() such that
A45: f1 = g.d & z = f1.n by A44;
A46: [k+1,a] = [[n,d],z]`1 by A44,MCART_1:def 1
.= [n,d] by MCART_1:def 1;
then A47: n = [k+1,a]`1 by MCART_1:def 1
.= k+1 by MCART_1:def 1;
A48: u = [[n,d],z]`2 by A44,MCART_1:def 2
.= z by MCART_1:def 2;
A49: d = [k+1,a]`2 by A46,MCART_1:def 2
.= a by MCART_1:def 2;
[k,a] in [:NAT,C():] by ZFMISC_1:def 2;
then [k,a] in dom h by FUNCT_2:def 1;
then consider v being set such that
A50: [[k,a],v] in h by RELAT_1:def 4;
consider n1 being Nat,
d1 being Element of C(),
z1 being Element of D() such that
A51: [[k,a],v] = [[n1,d1],z1] &
ex f2 being Function of NAT,D() st f2 = g.d1 & z1 = f2.n1 by A50;
consider f2 being Function of NAT,D() such that
A52: f2 = g.d1 & z1 = f2.n1 by A51;
A53: [k,a] = [[n1,d1],z1]`1 by A51,MCART_1:def 1
.= [n1,d1] by MCART_1:def 1;
then A54: n1 = [k,a]`1 by MCART_1:def 1
.= k by MCART_1:def 1;
A55: v = [[n1,d1],z1]`2 by A51,MCART_1:def 2
.= z1 by MCART_1:def 2;
A56: d1 = [k,a]`2 by A53,MCART_1:def 2
.= a by MCART_1:def 2;
thus h.(k+1,a) = h.[k+1,a] by BINOP_1:def 1
.= f'.(k+1) by A34,A43,A45,A47,A48,A49,FUNCT_1:8
.= F().(a,z1) by A34,A52,A54,A56
.= F().(a,h.[k,a]) by A50,A55,FUNCT_1:8
.= F().(a,h.(k,a)) by BINOP_1:def 1;
end;
hence thesis by A42;
end;
hence thesis;
end;
scheme RecDef2 {C,D() -> non empty set,
b() -> Element of D(),
F() -> Function of [:D(),C():],D()} :
ex g being Function of [:C(),NAT:],D() st
for a being Element of C() holds g.(a,0) = b() &
for n being Nat holds g.(a,n+1) = F().(g.(a,n),a)
proof
A1: for a being Element of C() holds
ex f being Function of NAT,D()
st f.0 = b() &
for n being Nat holds f.(n+1) = F().(f.n,a)
proof
let a be Element of C();
defpred P[Nat,Element of D(),Element of D()] means $3 = F().($2,a);
A2: for n being Nat for x being Element of D()
ex y being Element of D() st P[n,x,y];
ex f being Function of NAT,D() st
f.0 = b() &
for n being Element of NAT holds P[n,f.n,f.(n+1)] from RecExD(A2);
hence thesis;
end;
ex g being Function of C(),Funcs(NAT,D())
st for a being Element of C() holds
ex f being Function of NAT,D()
st g.a = f &
f.0 = b() &
for n being Nat holds f.(n+1) = F().(f.n,a)
proof
set h = {[a,l] where a is Element of C(),
l is Element of Funcs(NAT,D()) :
ex f being Function of NAT,D()
st f = l & f.0 = b() &
for n being Nat holds f.(n+1) = F().(f.n,a) };
A3: now let x,y1,y2 be set;
assume A4: [x,y1] in h & [x,y2] in h;
then consider a1 being Element of C(),
l1 being Element of Funcs(NAT,D()) such that
A5: [x,y1] = [a1,l1] &
ex f being Function of NAT,D()
st f = l1 & f.0 = b() &
for n being Nat holds f.(n+1) = F().(f.n,a1);
consider f1 being Function of NAT,D() such that
A6: f1 = l1 & f1.0 = b() &
for n being Nat holds f1.(n+1) = F().(f1.n,a1) by A5;
consider a2 being Element of C(),
l2 being Element of Funcs(NAT,D()) such that
A7: [x,y2] = [a2,l2] &
ex f being Function of NAT,D()
st f = l2 & f.0 = b() &
for n being Nat holds f.(n+1) = F().(f.n,a2) by A4;
consider f2 being Function of NAT,D() such that
A8: f2 = l2 & f2.0 = b() &
for n being Nat holds f2.(n+1) = F().(f2.n,a2) by A7;
A9: a1 = [x,y1]`1 by A5,MCART_1:def 1
.= x by MCART_1:def 1
.= [a2,l2]`1 by A7,MCART_1:def 1
.= a2 by MCART_1:def 1;
A10: NAT = dom f1 & NAT = dom f2 by FUNCT_2:def 1;
A11: now let x be set;
assume x in NAT;
then reconsider x' = x as Nat;
defpred _P[Nat] means f1.$1 = f2.$1 ;
A12: _P[0] by A6,A8;
A13: now let n be Nat;
assume A14: _P[n];
f1.(n+1) = F().(f1.n,a2) by A6,A9
.= f2.(n+1) by A8,A14;
hence _P[n+1];
end;
for n being Nat holds _P[n] from Ind(A12,A13);
hence f1.x = f2.x' .= f2.x;
end;
thus y1 = [a1,l1]`2 by A5,MCART_1:def 2
.= l1 by MCART_1:def 2
.= l2 by A6,A8,A10,A11,FUNCT_1:9
.= [x,y2]`2 by A7,MCART_1:def 2
.= y2 by MCART_1:def 2;
end;
now let x be set;
assume x in h;
then consider a being Element of C(),
l being Element of Funcs(NAT,D()) such that
A15: x = [a,l] &
ex f being Function of NAT,D()
st f = l & f.0 = b() &
for n being Nat holds f.(n+1) = F().(f.n,a);
thus x in [:C(),Funcs(NAT,D()):] by A15,ZFMISC_1:def 2;
end;
then h c= [:C(),Funcs(NAT,D()):] by TARSKI:def 3;
then reconsider h as Relation of C(),Funcs(NAT,D()) by RELSET_1:def 1;
A16: for x being set holds x in dom h implies x in C();
for x being set holds x in C() implies x in dom h
proof
let x be set;
assume A17: x in C();
then consider f being Function of NAT,D() such that
A18: f.0 = b() &
for n being Nat holds f.(n+1) = F().(f.n,x) by A1;
reconsider f' = f as Element of Funcs(NAT,D()) by FUNCT_2:11;
[x,f'] in h by A17,A18;
hence thesis by RELAT_1:def 4;
end;
then dom h = C() by A16,TARSKI:2;
then reconsider h as Function of C(),Funcs(NAT,D())
by A3,FUNCT_1:def 1,FUNCT_2:def 1;
take h;
for a being Element of C() holds
ex f being Function of NAT,D()
st h.a = f &
f.0 = b() &
for n being Nat holds f.(n+1) = F().(f.n,a)
proof
let a be Element of C();
dom h = C() by FUNCT_2:def 1;
then [a,h.a] in h by FUNCT_1:8;
then consider a' being Element of C(),
l being Element of Funcs(NAT,D()) such that
A19: [a,h.a] = [a',l] &
ex f' being Function of NAT,D()
st f' = l & f'.0 = b() &
for n being Nat holds f'.(n+1) = F().(f'.n,a');
consider f' being Function of NAT,D() such that
A20: f' = l & f'.0 = b() &
for n being Nat holds f'.(n+1) = F().(f'.n,a') by A19;
A21: a = [a',l]`1 by A19,MCART_1:def 1
.= a' by MCART_1:def 1;
h.a = [a',l]`2 by A19,MCART_1:def 2
.= l by MCART_1:def 2;
hence thesis by A20,A21;
end;
hence thesis;
end;
then consider g being Function of C(),Funcs(NAT,D()) such that
A22: for a being Element of C() holds
ex f being Function of NAT,D()
st g.a = f &
f.0 = b() &
for n being Nat holds f.(n+1) = F().(f.n,a);
set h = { [[a,n],z] where n is Nat, a is Element of C(), z is Element of D() :
ex f being Function of NAT,D() st f = g.a & z = f.n };
A23: now let x,y1,y2 be set;
assume A24: [x,y1] in h & [x,y2] in h;
then consider n1 being Nat,
a1 being Element of C(),
z1 being Element of D() such that
A25: [x,y1] = [[a1,n1],z1] &
ex f1 being Function of NAT,D() st f1 = g.a1 & z1 = f1.n1;
consider n2 being Nat,
a2 being Element of C(),
z2 being Element of D() such that
A26: [x,y2] = [[a2,n2],z2] &
ex f2 being Function of NAT,D() st f2 = g.a2 & z2 = f2.n2 by A24;
A27: [a1,n1] = [x,y1]`1 by A25,MCART_1:def 1
.= x by MCART_1:def 1
.= [[a2,n2],z2]`1 by A26,MCART_1:def 1
.= [a2,n2] by MCART_1:def 1;
then A28: a1 = [a2,n2]`1 by MCART_1:def 1
.= a2 by MCART_1:def 1;
n1 = [a2,n2]`2 by A27,MCART_1:def 2
.= n2 by MCART_1:def 2;
hence y1 = [x,y2]`2 by A25,A26,A28,MCART_1:def 2
.= y2 by MCART_1:def 2;
end;
now let x be set;
assume x in h;
then consider n1 being Nat,
a1 being Element of C(),
z1 being Element of D() such that
A29: x = [[a1,n1],z1] &
ex f1 being Function of NAT,D() st f1 = g.a1 & z1 = f1.n1;
[a1,n1] in [:C(),NAT:] by ZFMISC_1:def 2;
hence x in [:[:C(),NAT:],D():] by A29,ZFMISC_1:def 2;
end;
then h c= [:[:C(),NAT:],D():] by TARSKI:def 3;
then reconsider h as Relation of [:C(),NAT:],D() by RELSET_1:def 1;
A30: for x being set holds x in dom h implies x in [:C(),NAT:];
for x being set holds x in [:C(),NAT:] implies x in dom h
proof
let x be set;
assume x in [:C(),NAT:];
then consider d,n being set such that
A31: d in C() & n in NAT & x = [d,n] by ZFMISC_1:def 2;
reconsider n as Nat by A31;
reconsider d as Element of C() by A31;
consider f' being Function of NAT,D() such that
A32: g.d = f' &
f'.0 = b() &
for n being Nat holds f'.(n+1) = F().(f'.n,d) by A22;
ex z being Element of D() st
ex f being Function of NAT,D() st f = g.d & z = f.n
proof
take f'.n;
take f';
thus thesis by A32;
end;
then consider z being Element of D() such that
A33: ex f being Function of NAT,D() st f = g.d & z = f.n;
[x,z] in h by A31,A33;
hence thesis by RELAT_1:def 4;
end;
then dom h = [:C(),NAT:] by A30,TARSKI:2;
then reconsider h as Function of [:C(),NAT:],D()
by A23,FUNCT_1:def 1,FUNCT_2:def 1;
take h;
for a being Element of C() holds h.(a,0) = b() &
for n being Nat holds h.(a,n+1) = F().(h.(a,n),a)
proof
let a be Element of C();
consider f' being Function of NAT,D() such that
A34: g.a = f' &
f'.0 = b() &
for n being Nat holds f'.(n+1) = F().(f'.n,a) by A22;
[a,0] in [:C(),NAT:] by ZFMISC_1:def 2;
then [a,0] in dom h by FUNCT_2:def 1;
then consider u being set such that
A35: [[a,0],u] in h by RELAT_1:def 4;
consider n being Nat,
d being Element of C(),
z being Element of D() such that
A36: [[a,0],u] = [[d,n],z] &
ex f1 being Function of NAT,D() st f1 = g.d & z = f1.n by A35;
consider f1 being Function of NAT,D() such that
A37: f1 = g.d & z = f1.n by A36;
A38: [a,0] = [[d,n],z]`1 by A36,MCART_1:def 1
.= [d,n] by MCART_1:def 1;
then A39: n = [a,0]`2 by MCART_1:def 2
.= 0 by MCART_1:def 2;
A40: u = [[d,n],z]`2 by A36,MCART_1:def 2
.= z by MCART_1:def 2;
A41: d = [a,0]`1 by A38,MCART_1:def 1
.= a by MCART_1:def 1;
A42: h.(a,0) = h.[a,0] by BINOP_1:def 1
.= b() by A34,A35,A37,A39,A40,A41,FUNCT_1:8;
now let k be Nat;
[a,k+1] in [:C(),NAT:] by ZFMISC_1:def 2;
then [a,k+1] in dom h by FUNCT_2:def 1;
then consider u being set such that
A43: [[a,k+1],u] in h by RELAT_1:def 4;
consider n being Nat,
d being Element of C(),
z being Element of D() such that
A44: [[a,k+1],u] = [[d,n],z] &
ex f1 being Function of NAT,D() st f1 = g.d & z = f1.n by A43;
consider f1 being Function of NAT,D() such that
A45: f1 = g.d & z = f1.n by A44;
A46: [a,k+1] = [[d,n],z]`1 by A44,MCART_1:def 1
.= [d,n] by MCART_1:def 1;
then A47: n = [a,k+1]`2 by MCART_1:def 2
.= k+1 by MCART_1:def 2;
A48: u = [[d,n],z]`2 by A44,MCART_1:def 2
.= z by MCART_1:def 2;
A49: d = [a,k+1]`1 by A46,MCART_1:def 1
.= a by MCART_1:def 1;
[a,k] in [:C(),NAT:] by ZFMISC_1:def 2;
then [a,k] in dom h by FUNCT_2:def 1;
then consider v being set such that
A50: [[a,k],v] in h by RELAT_1:def 4;
consider n1 being Nat,
d1 being Element of C(),
z1 being Element of D() such that
A51: [[a,k],v] = [[d1,n1],z1] &
ex f2 being Function of NAT,D() st f2 = g.d1 & z1 = f2.n1 by A50;
consider f2 being Function of NAT,D() such that
A52: f2 = g.d1 & z1 = f2.n1 by A51;
A53: [a,k] = [[d1,n1],z1]`1 by A51,MCART_1:def 1
.= [d1,n1] by MCART_1:def 1;
then A54: n1 = [a,k]`2 by MCART_1:def 2
.= k by MCART_1:def 2;
A55: v = [[d1,n1],z1]`2 by A51,MCART_1:def 2
.= z1 by MCART_1:def 2;
A56: d1 = [a,k]`1 by A53,MCART_1:def 1
.= a by MCART_1:def 1;
thus h.(a,k+1) = h.[a,k+1] by BINOP_1:def 1
.= f'.n by A34,A43,A45,A48,A49,FUNCT_1:8
.= F().(f2.n1,a) by A34,A47,A52,A54,A56
.= F().(h.[a,k],a) by A50,A52,A55,FUNCT_1:8
.= F().(h.(a,k),a) by BINOP_1:def 1;
end;
hence thesis by A42;
end;
hence thesis;
end;
begin :: On Finite Sequences
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem Th3:
for L being left_zeroed (non empty LoopStr),
a being Element of L
holds Sum <* a *> = a
proof
let V be left_zeroed (non empty LoopStr),
v be Element of V;
reconsider a = v as Element of V;
set S = <* v *>;
consider f being Function of NAT, the carrier of V such that
A1: Sum(S) = f.(len S) and
A2: f.0 = 0.V and
A3: for j being Nat for v being Element of V
st j < len S & v = S.(j + 1) holds
f.(j + 1) = f.j + v by RLVECT_1:def 12;
A4: len <* a *> = 1 by FINSEQ_1:56;
0 < 1;
then consider j being Nat such that A5: j < len S by A4;
A6: j = 0 by A4,A5,RLVECT_1:98;
S.(j + 1) = S.(0 + 1) by A4,A5,RLVECT_1:98
.= v by FINSEQ_1:57;
then f.1 = 0.V + v by A2,A3,A5,A6
.= a by ALGSTR_1:def 5;
hence thesis by A1,FINSEQ_1:56;
end;
theorem
for R being left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
a being Element of R,
p being FinSequence of the carrier of R
holds Sum(a * p) = a * Sum p
proof
let R be left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
a be Element of R,
p be FinSequence of the carrier of R;
consider f being Function of NAT,the carrier of R such that
A1: Sum p = f.(len p) &
f.0 = 0.R &
for j being Nat, v being Element of R
st j < len p & v = p.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
consider fa being Function of NAT,the carrier of R such that
A2: Sum(a * p) = fa.(len(a * p)) &
fa.0 = 0.R &
for j being Nat, v being Element of R
st j < len(a * p) & v = (a * p).(j + 1) holds fa.(j + 1) = fa.j + v
by RLVECT_1:def 12;
A3: Seg(len(a * p)) = dom(a * p) by FINSEQ_1:def 3
.= dom p by POLYNOM1:def 2
.= Seg(len p) by FINSEQ_1:def 3;
defpred _P[Nat] means a * f.$1 = fa.$1;
A4: _P[0] by A1,A2,Th2;
A5: now let j be Nat;
assume A6: 0 <= j & j < len p;
thus _P[j] implies _P[j+1] proof
assume A7: _P[j];
A8: j < len(a * p) by A3,A6,FINSEQ_1:8;
then A9: j + 1 <= len(a * p) by NAT_1:38;
A10: j + 1 <= len p by A6,NAT_1:38;
A11: 0 + 1 <= j + 1 by A6,AXIOMS:24;
then j + 1 in Seg len(a * p) by A9,FINSEQ_1:3;
then j + 1 in dom(a * p) by FINSEQ_1:def 3;
then A12: (a * p)/.(j + 1) = (a * p).(j + 1) by FINSEQ_4:def 4;
j + 1 in Seg len p by A10,A11,FINSEQ_1:3;
then A13: j + 1 in dom p by FINSEQ_1:def 3;
then A14: p/.(j + 1) = p.(j + 1) by FINSEQ_4:def 4;
thus fa.(j+1) = a * f.j + (a * p)/.(j + 1) by A2,A7,A8,A12
.= a * f.j + a * p/.(j + 1) by A13,POLYNOM1:def 2
.= a * (f.j + p/.(j + 1)) by VECTSP_1:def 11
.= a * f.(j+1) by A1,A6,A14;
end;
end;
A15: for i being Nat st 0 <= i & i <= len p holds _P[i] from FinInd(A4,A5);
A16: 0 <= len p by NAT_1:18;
thus Sum(a * p) = fa.(len p) by A2,A3,FINSEQ_1:8
.= a * Sum p by A1,A15,A16;
end;
theorem Th5:
for R being right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr),
a being Element of R,
p being FinSequence of the carrier of R
holds Sum(p * a) = Sum p * a
proof
let R be right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr),
a be Element of R,
p be FinSequence of the carrier of R;
consider f being Function of NAT,the carrier of R such that
A1: Sum p = f.(len p) &
f.0 = 0.R &
for j being Nat, v being Element of R
st j < len p & v = p.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
consider fa being Function of NAT,the carrier of R such that
A2: Sum(p * a) = fa.(len(p * a)) &
fa.0 = 0.R &
for j being Nat, v being Element of R
st j < len(p * a) & v = (p * a).(j + 1) holds fa.(j + 1) = fa.j + v
by RLVECT_1:def 12;
A3: Seg(len(p * a)) = dom(p * a) by FINSEQ_1:def 3
.= dom p by POLYNOM1:def 3
.= Seg(len p) by FINSEQ_1:def 3;
defpred _P[Nat] means f.$1 * a = fa.$1;
A4: _P[0] by A1,A2,Th1;
A5: now let j be Nat;
assume A6: 0 <= j & j < len p;
thus _P[j] implies _P[j+1] proof
assume A7: f.j * a = fa.j;
A8: j < len(p * a) by A3,A6,FINSEQ_1:8;
then A9: j + 1 <= len(p * a) by NAT_1:38;
A10: 0 + 1 <= j + 1 by A6,AXIOMS:24;
then j + 1 in Seg len(p * a) by A9,FINSEQ_1:3;
then j + 1 in dom(p * a) by FINSEQ_1:def 3;
then A11: (p * a)/.(j + 1) = (p * a).(j + 1) by FINSEQ_4:def 4;
j + 1 in Seg len p by A3,A9,A10,FINSEQ_1:3;
then A12: j + 1 in dom p by FINSEQ_1:def 3;
then A13: p/.(j + 1) = p.(j + 1) by FINSEQ_4:def 4;
thus fa.(j+1) = f.j * a + (p * a)/.(j + 1) by A2,A7,A8,A11
.= f.j * a + p/.(j + 1) * a by A12,POLYNOM1:def 3
.= (f.j + p/.(j + 1)) * a by VECTSP_1:def 12
.= f.(j+1) * a by A1,A6,A13;
end;
end;
A14: for i being Nat st 0 <= i & i <= len p holds _P[i] from FinInd(A4,A5);
A15: 0 <= len p by NAT_1:18;
thus Sum(p * a) = fa.(len p) by A2,A3,FINSEQ_1:8
.= Sum p * a by A1,A14,A15;
end;
theorem
for R being commutative (non empty doubleLoopStr),
a being Element of R,
p being FinSequence of the carrier of R
holds Sum(p * a) = Sum(a * p)
proof
let R be commutative (non empty doubleLoopStr),
a be Element of R,
p be FinSequence of the carrier of R;
consider f being Function of NAT,the carrier of R such that
A1: Sum(p * a) = f.(len(p * a)) &
f.0 = 0.R &
for j being Nat, v being Element of R
st j < len(p * a) & v = (p * a).(j + 1) holds f.(j + 1) = f.j + v
by RLVECT_1:def 12;
consider g being Function of NAT,the carrier of R such that
A2: Sum(a * p) = g.(len(a * p)) &
g.0 = 0.R &
for j being Nat, v being Element of R
st j < len(a * p) & v = (a * p).(j + 1) holds g.(j + 1) = g.j + v
by RLVECT_1:def 12;
A3: Seg(len(a * p)) = dom(a * p) by FINSEQ_1:def 3
.= dom p by POLYNOM1:def 2
.= Seg(len p) by FINSEQ_1:def 3;
A4: Seg(len(p * a)) = dom(p * a) by FINSEQ_1:def 3
.= dom p by POLYNOM1:def 3
.= Seg(len p) by FINSEQ_1:def 3;
defpred _P[Nat] means f.$1 = g.$1;
A5: _P[0] by A1,A2;
A6: now let j be Nat;
assume A7: 0 <= j & j < len p;
thus _P[j] implies _P[j+1]
proof
assume A8: f.j = g.j;
A9: j < len(p * a) by A4,A7,FINSEQ_1:8;
then A10: j + 1 <= len(p * a) by NAT_1:38;
A11: 0 + 1 <= j + 1 by A7,AXIOMS:24;
then j + 1 in Seg len(p * a) by A10,FINSEQ_1:3;
then j + 1 in dom(p * a) by FINSEQ_1:def 3;
then A12: (p * a)/.(j + 1) = (p * a).(j + 1) by FINSEQ_4:def 4;
A13: j < len(a * p) by A3,A7,FINSEQ_1:8;
j + 1 in Seg len(a * p) by A3,A4,A10,A11,FINSEQ_1:3;
then A14: j + 1 in dom(a * p) by FINSEQ_1:def 3;
then A15: j + 1 in dom p by POLYNOM1:def 2;
A16: (a * p)/.(j + 1) = (a * p).(j + 1) by A14,FINSEQ_4:def 4;
thus f.(j+1) = g.j + (p * a)/.(j + 1) by A1,A8,A9,A12
.= g.j + p/.(j + 1) * a by A15,POLYNOM1:def 3
.= g.j + (a * p)/.(j + 1) by A15,POLYNOM1:def 2
.= g.(j+1) by A2,A13,A16;
end;
end;
A17: for i being Nat st 0 <= i & i <= len p holds _P[i] from FinInd(A5,A6);
A18: 0 <= len p by NAT_1:18;
thus Sum(p * a) = f.(len p) by A1,A4,FINSEQ_1:8
.= g.(len p) by A17,A18
.= Sum(a * p) by A2,A3,FINSEQ_1:8;
end;
definition
let R be non empty LoopStr,
p,q be FinSequence of the carrier of R such that dom p = dom q;
func p + q -> FinSequence of the carrier of R means :Def4:
dom it = dom p &
for i being Nat st 1 <= i & i <= len it holds it/.i = p/.i + q/.i;
existence
proof
defpred P[Nat,Element of R]
means $2 = (p/.($1)) + (q/.($1));
A1: for k being Nat st k in Seg(len p)
ex x being Element of R st P[k,x];
consider f being FinSequence of the carrier of R such that
A2: dom f = Seg(len p) &
for k being Nat st k in Seg(len p) holds P[k,f/.k]
from SeqExD(A1);
take f;
A3: len f = len p by A2,FINSEQ_1:def 3;
now let m be Nat;
assume 1 <= m & m <= len f;
then m in Seg(len p) by A3,FINSEQ_1:3;
hence f/.m = p/.m + q/.m by A2;
end;
hence thesis by A2,FINSEQ_1:def 3;
end;
uniqueness
proof
let y1,y2 be FinSequence of the carrier of R;
assume that
A4: dom y1 = dom p &
for i being Nat st 1 <= i & i <= len y1 holds y1/.i = p/.i + q/.i and
A5: dom y2 = dom p &
for i being Nat st 1 <= i & i <= len y2 holds y2/.i = p/.i + q/.i;
A6: Seg(len y1) = dom y2 by A4,A5,FINSEQ_1:def 3
.= Seg(len y2) by FINSEQ_1:def 3;
then A7: len y1 = len y2 by FINSEQ_1:8;
now let i be Nat;
assume A8: 1 <= i & i <= len y1;
then i in Seg (len y1) & i in Seg (len y2) by A6,FINSEQ_1:3;
then A9: i in dom y1 & i in dom y2 by FINSEQ_1:def 3;
hence y1.i = y1/.i by FINSEQ_4:def 4
.= p/.i + q/.i by A4,A8
.= y2/.i by A5,A7,A8
.= y2.i by A9,FINSEQ_4:def 4;
end;
hence thesis by A7,FINSEQ_1:18;
end;
end;
theorem Th7:
for R being Abelian right_zeroed add-associative (non empty LoopStr),
p,q being FinSequence of the carrier of R st dom p = dom q
holds Sum(p + q) = Sum p + Sum q
proof
let R be Abelian right_zeroed add-associative (non empty LoopStr),
p,q be FinSequence of the carrier of R;
assume A1: dom p = dom q;
then A2: Seg(len p) = dom q by FINSEQ_1:def 3
.= Seg(len q) by FINSEQ_1:def 3;
then A3: len q = len p by FINSEQ_1:8;
A4: Seg(len p) = dom p by FINSEQ_1:def 3
.= dom(p+q) by A1,Def4
.= Seg(len(p+q)) by FINSEQ_1:def 3;
then A5: len(p+q) = len p by FINSEQ_1:8;
consider fp being Function of NAT,the carrier of R such that
A6: Sum p = fp.(len p) &
fp.0 = 0.R &
for j being Nat, v being Element of R
st j < len p & v = p.(j + 1) holds fp.(j + 1) = fp.j + v
by RLVECT_1:def 12;
consider fq being Function of NAT,the carrier of R such that
A7: Sum q = fq.(len q) &
fq.0 = 0.R &
for j being Nat, v being Element of R
st j < len q & v = q.(j + 1) holds fq.(j + 1) = fq.j + v
by RLVECT_1:def 12;
consider fa being Function of NAT,the carrier of R such that
A8: Sum(p+q) = fa.(len(p+q)) &
fa.0 = 0.R &
for j being Nat, v being Element of R
st j < len(p+q) & v = (p+q).(j + 1) holds fa.(j + 1) = fa.j + v
by RLVECT_1:def 12;
defpred _P[Nat] means fp.$1 + fq.$1 = fa.$1;
A9: _P[0] by A6,A7,A8,RLVECT_1:def 7;
A10: now let j be Nat;
assume A11: 0 <= j & j < len p;
thus _P[j] implies _P[j+1]
proof
assume A12: _P[j];
A13: j + 1 <= len(p+q) by A5,A11,NAT_1:38;
A14: j + 1 <= len p by A11,NAT_1:38;
A15: 0 + 1 <= j + 1 by A11,AXIOMS:24;
then j + 1 in Seg len(p+q) by A13,FINSEQ_1:3;
then j + 1 in dom(p+q) by FINSEQ_1:def 3;
then A16: (p+q)/.(j + 1) = (p+q).(j + 1) by FINSEQ_4:def 4;
j + 1 in Seg len p by A14,A15,FINSEQ_1:3;
then j + 1 in dom p by FINSEQ_1:def 3;
then A17: p/.(j + 1) = p.(j + 1) by FINSEQ_4:def 4;
j + 1 in Seg len q by A2,A14,A15,FINSEQ_1:3;
then j + 1 in dom q by FINSEQ_1:def 3;
then A18: q/.(j + 1) = q.(j + 1) by FINSEQ_4:def 4;
fa.(j+1) = fa.j + (p+q)/.(j + 1) by A5,A8,A11,A16
.= (fp.j + fq.j) + (p/.(j + 1) + q/.(j + 1)) by A1,A12,A13,A15,
Def4
.= fp.j + (fq.j + (p/.(j + 1) + q/.(j + 1))) by RLVECT_1:def 6
.= fp.j + (p/.(j + 1) + (fq.j + q/.(j + 1))) by RLVECT_1:def 6
.= (fp.j + p/.(j + 1)) + (fq.j + q/.(j + 1)) by RLVECT_1:def 6
.= fp.(j+1) + (fq.j + q/.(j + 1)) by A6,A11,A17
.= fp.(j+1) + fq.(j+1) by A3,A7,A11,A18;
hence thesis;
end;
end;
A19: for i being Nat st 0 <= i & i <= len p holds _P[i] from FinInd(A9,A10);
A20: 0 <= len p by NAT_1:18;
thus Sum(p + q) = fa.(len p) by A4,A8,FINSEQ_1:8
.= Sum p + Sum q by A3,A6,A7,A19,A20;
end;
begin :: On Powers in Rings
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R be unital (non empty HGrStr),
a be Element of R,
n be Nat;
func a|^n -> Element of R equals :Def5:
power(R).(a,n);
coherence ;
end;
theorem Th8:
for R being unital (non empty HGrStr),
a being Element of R
holds a|^0 = 1.R & a|^1 = a
proof
let R be unital (non empty HGrStr),
a be Element of R;
power(R).(a,0) = 1.R by GROUP_1:def 7;
hence a|^0 = 1.R by Def5;
0 + 1 = 1;
then power(R).(a,1) = power(R).(a,0) * a by GROUP_1:def 7
.= 1.R * a by GROUP_1:def 7
.= a by GROUP_1:def 4;
hence thesis by Def5;
end;
theorem Th9:
for R being unital (non empty HGrStr),
a being Element of R,
n being Nat
holds a|^(n+1) = (a|^n) * a
proof
let R be unital (non empty HGrStr),
a be Element of R,
n be Nat;
thus a|^(n+1) = power(R).(a,n+1) by Def5
.= power(R).(a,n) * a by GROUP_1:def 7
.= (a|^n) * a by Def5;
end;
theorem
for R being unital associative commutative (non empty HGrStr),
a,b being Element of R,
n being Nat
holds (a * b)|^n = (a|^n) * (b|^n)
proof
let R be unital associative commutative (non empty HGrStr),
a,b be Element of R,
n be Nat;
defpred _P[Nat] means
power(R).(a * b,$1) = power(R).(a,$1) * power(R).(b,$1);
power(R).(a * b,0) = 1.R by GROUP_1:def 7
.= 1.R * 1.R by GROUP_1:def 4
.= power(R).(a,0) * 1.R by GROUP_1:def 7
.= power(R).(a,0) * power(R).(b,0) by GROUP_1:def 7; then
A1: _P[0];
A2: now let m be Nat;
assume _P[m]; then
power(R).(a * b,m+1)
= (power(R).(a,m) * power(R).(b,m)) * (a * b) by GROUP_1:def 7
.= ((power(R).(a,m) * power(R).(b,m)) * a) * b by VECTSP_1:def 16
.= ((power(R).(a,m) * a) * power(R).(b,m)) * b by VECTSP_1:def 16
.= (power(R).(a,m) * a) * (power(R).(b,m) * b) by VECTSP_1:def 16
.= power(R).(a,m+1) * (power(R).(b,m) * b) by GROUP_1:def 7
.= power(R).(a,m+1) * power(R).(b,m+1) by GROUP_1:def 7;
hence _P[m+1];
end;
A3: for m being Nat holds _P[m] from Ind(A1,A2);
thus (a * b)|^n = power(R).(a * b,n) by Def5
.= power(R).(a,n) * power(R).(b,n) by A3
.= a|^n * power(R).(b,n) by Def5
.= (a|^n) * (b|^n) by Def5;
end;
theorem Th11:
for R being unital associative (non empty HGrStr),
a being Element of R,
n,m being Nat
holds a|^(n+m) = (a|^n) * (a|^m)
proof
let R be unital associative (non empty HGrStr),
a be Element of R,
n,m be Nat;
defpred _P[Nat] means
power(R).(a,n+$1) = power(R).(a,n) * power(R).(a,$1);
power(R).(a,n + 0) = power(R).(a,n) * 1.R by GROUP_1:def 4
.= power(R).(a,n) * power(R).(a,0) by GROUP_1:def 7; then
A1: _P[0];
A2: now let m be Nat;
assume A3: _P[m];
power(R).(a,n+(m+1))
= power(R).(a,(n+m)+1) by XCMPLX_1:1
.= (power(R).(a,n) * power(R).(a,m)) * a by A3,GROUP_1:def 7
.= power(R).(a,n) * (power(R).(a,m) * a) by VECTSP_1:def 16
.= power(R).(a,n) * power(R).(a,(m+1)) by GROUP_1:def 7;
hence _P[m+1];
end;
A4: for m being Nat holds _P[m] from Ind(A1,A2);
thus a|^(n+m) = power(R).(a,n+m) by Def5
.= power(R).(a,n) * power(R).(a,m) by A4
.= a|^n * power(R).(a,m) by Def5
.= (a|^n) * (a|^m) by Def5;
end;
theorem
for R being unital associative (non empty HGrStr),
a being Element of R,
n,m being Nat
holds (a|^n)|^m = a|^(n * m)
proof
let R be unital associative (non empty HGrStr),
a be Element of R,
n,m be Nat;
defpred _P[Nat] means power(R).(a|^n,$1) = power(R).(a,n * $1);
power(R).(a|^n,0) = 1.R by GROUP_1:def 7
.= power(R).(a,n * 0) by GROUP_1:def 7; then
A1: _P[0];
A2: now let m be Nat;
assume A3: _P[m];
A4: n * m + n = n * m + n * 1
.= n * (m + 1) by XCMPLX_1:8;
power(R).(a|^n,m+1)
= power(R).(a,n * m) * (a|^n) by A3,GROUP_1:def 7
.= a|^(n * m) * (a|^n) by Def5
.= a|^(n * m + n) by Th11
.= power(R).(a,n * (m + 1)) by A4,Def5;
hence _P[m+1];
end;
A5: for k being Nat holds _P[k] from Ind(A1,A2);
thus (a|^n)|^m = power(R).(a|^n,m) by Def5
.= power(R).(a,n * m) by A5
.= a|^(n * m) by Def5;
end;
begin :: On Natural Products in Rings
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
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:
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
set D = the carrier of R;
consider g being Function of [:NAT,D:],D such that
A1: for a being Element of D
holds g.(0,a) = 0.R &
for n being Nat holds g.(n+1,a) = (the add of R).(a,g.(n,a))
from RecDef1;
take g;
for a being Element of R
holds g.(0,a) = 0.R &
for n being Nat holds g.(n+1,a) = a + g.(n,a)
proof
let a be Element of R;
thus g.(0,a) = 0.R by A1;
for n being Nat holds g.(n+1,a) = a + g.(n,a)
proof
let n be Nat;
reconsider a' = a as Element of R;
g.(n+1,a) = (the add of R).(a,g.(n,a)) by A1
.= (the add of R).[a,g.(n,a)] by BINOP_1:def 1
.= a' + g.(n,a) by RLVECT_1:def 3;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let f,g be Function of [:NAT,the carrier of R:],the carrier of R;
assume A2: for a being Element of R
holds f.(0,a) = 0.R &
for n being Nat holds f.(n+1,a) = a + f.(n,a);
assume A3: for a being Element of R
holds g.(0,a) = 0.R &
for n being Nat holds g.(n+1,a) = a + g.(n,a);
defpred _P[Nat] means for a being Element of R holds f.($1,a) = g.($1,a);
A4: _P[0] proof let a be Element of R;
thus f.(0,a) = 0.R by A2 .= g.(0,a) by A3;
end;
A5: now let n be Nat;
assume A6: _P[n];
now let a be Element of R;
thus f.(n+1,a) = a + f.(n,a) by A2
.= a + g.(n,a) by A6
.= g.(n+1,a) by A3;
end;
hence _P[n+1];
end;
A7: for n being Nat holds _P[n] from Ind(A4,A5);
A8: dom f = [:NAT,the carrier of R:] by FUNCT_2:def 1;
A9: dom g = [:NAT,the carrier of R:] by FUNCT_2:def 1;
now let x be set;
assume x in [:NAT,the carrier of R:];
then consider u,v being set such that
A10: u in NAT & v in the carrier of R & x = [u,v] by ZFMISC_1:def 2;
reconsider u as Nat by A10;
reconsider v as Element of R by A10;
thus f.x = f.(u,v) by A10,BINOP_1:def 1
.= g.(u,v) by A7
.= g.x by A10,BINOP_1:def 1;
end;
hence thesis by A8,A9,FUNCT_1:9;
end;
func Nat-mult-right(R)
-> Function of [:the carrier of R,NAT:],the carrier of R means :Def7:
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
consider g being Function of [:the carrier of R,NAT:],the carrier of R
such that
A11: for a being Element of R
holds g.(a,0) = 0.R &
for n being Nat holds g.(a,n+1) = (the add of R).(g.(a,n),a)
from RecDef2;
take g;
for a being Element of R
holds g.(a,0) = 0.R &
for n being Nat holds g.(a,n+1) = g.(a,n) + a
proof
let a be Element of R;
thus g.(a,0) = 0.R by A11;
for n being Nat holds g.(a,n+1) = g.(a,n) + a
proof
let n be Nat;
reconsider a' = a as Element of R;
g.(a,n+1) = (the add of R).(g.(a,n),a) by A11
.= (the add of R).[g.(a,n),a] by BINOP_1:def 1
.= g.(a,n) + a' by RLVECT_1:def 3;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let f,g be Function of [:the carrier of R,NAT:],the carrier of R;
assume A12: for a being Element of R
holds f.(a,0) = 0.R &
for n being Nat holds f.(a,n+1) = f.(a,n) + a;
assume A13: for a being Element of R
holds g.(a,0) = 0.R &
for n being Nat holds g.(a,n+1) = g.(a,n) + a;
defpred _P[Nat] means for a being Element of R holds f.(a,$1) = g.(a,$1);
A14: _P[0] proof let a be Element of R;
thus f.(a,0) = 0.R by A12 .= g.(a,0) by A13;
end;
A15: now let n be Nat;
assume A16: _P[n];
now let a be Element of R;
thus f.(a,n+1) = f.(a,n) + a by A12
.= g.(a,n) + a by A16
.= g.(a,n+1) by A13;
end;
hence _P[n+1];
end;
A17: for n being Nat holds _P[n] from Ind(A14,A15);
A18: dom f = [:the carrier of R,NAT:] by FUNCT_2:def 1;
A19: dom g = [:the carrier of R,NAT:] by FUNCT_2:def 1;
now let x be set;
assume x in [:the carrier of R,NAT:];
then consider v,u being set such that
A20: v in the carrier of R & u in NAT & x = [v,u] by ZFMISC_1:def 2;
reconsider u as Nat by A20;
reconsider v as Element of R by A20;
thus f.x = f.(v,u) by A20,BINOP_1:def 1
.= g.(v,u) by A17
.= g.x by A20,BINOP_1:def 1;
end;
hence thesis by A18,A19,FUNCT_1:9;
end;
end;
definition
let R be non empty LoopStr,
a be Element of R,
n be Nat;
func n * a -> Element of R equals :Def8:
(Nat-mult-left(R)).(n,a);
coherence ;
func a * n -> Element of R equals :Def9:
(Nat-mult-right(R)).(a,n);
coherence ;
end;
theorem Th13:
for R being non empty LoopStr,
a being Element of R
holds 0 * a = 0.R & a * 0 = 0.R
proof
let R be non empty LoopStr,
a be Element of R;
thus 0 * a = (Nat-mult-left(R)).(0,a) by Def8 .= 0.R by Def6;
thus a * 0 = (Nat-mult-right(R)).(a,0) by Def9 .= 0.R by Def7;
end;
theorem Th14:
for R being right_zeroed (non empty LoopStr),
a being Element of R
holds 1 * a = a
proof
let R be right_zeroed (non empty LoopStr),
a be Element of R;
thus 1 * a = (Nat-mult-left(R)).(0+1,a) by Def8
.= a + (Nat-mult-left(R)).(0,a) by Def6
.= a + 0.R by Def6
.= a by RLVECT_1:def 7;
end;
theorem Th15:
for R being left_zeroed (non empty LoopStr),
a being Element of R
holds a * 1 = a
proof
let R be left_zeroed (non empty LoopStr),
a be Element of R;
thus a * 1 = (Nat-mult-right(R)).(a,0+1) by Def9
.= (Nat-mult-right(R)).(a,0) + a by Def7
.= 0.R + a by Def7
.= a by ALGSTR_1:def 5;
end;
Lm1:
for R being non empty LoopStr,
a being Element of R,
n being Nat
holds (n+1) * a = a + n * a
proof
let R be non empty LoopStr,
a be Element of R,
n be Nat;
thus (n+1) * a = (Nat-mult-left(R)).(n+1,a) by Def8
.= a + (Nat-mult-left(R)).(n,a) by Def6
.= a + n * a by Def8;
end;
Lm2:
for R being non empty LoopStr,
a being Element of R,
n being Nat
holds a * (n+1) = a * n + a
proof
let R be (non empty LoopStr),
a be Element of R,
n be Nat;
thus a * (n+1) = (Nat-mult-right(R)).(a,n+1) by Def9
.= (Nat-mult-right(R)).(a,n) + a by Def7
.= a * n + a by Def9;
end;
theorem Th16:
for R being left_zeroed add-associative (non empty LoopStr),
a being Element of R,
n,m being Nat
holds (n + m) * a = n * a + m * a
proof
let R be left_zeroed add-associative (non empty LoopStr),
a be Element of R,
n,m be Nat;
defpred _P[Nat] means ($1 + m) * a = $1 * a + m * a;
(0 + m) * a = 0.R + m * a by ALGSTR_1:def 5 .= 0 * a + m * a by Th13; then
A1: _P[0];
A2: now let k be Nat;
assume A3: _P[k];
((k+1) + m) * a = ((k+m) + 1) * a by XCMPLX_1:1
.= a + (k * a + m * a) by A3,Lm1
.= (a + k * a) + m * a by RLVECT_1:def 6
.= (k+1) * a + m * a by Lm1;
hence _P[k+1];
end;
for n being Nat holds _P[n] from Ind(A1,A2);
hence thesis;
end;
theorem Th17:
for R being right_zeroed add-associative (non empty LoopStr),
a being Element of R,
n,m being Nat
holds a * (n + m) = a * n + a * m
proof
let R be right_zeroed add-associative (non empty LoopStr),
a be Element of R,
n,m be Nat;
defpred _P[Nat] means a * (n + $1) = a * n + a * $1;
a * (n + 0) = a * n + 0.R by RLVECT_1:def 7 .= a * n + a * 0 by Th13; then
A1: _P[0];
A2: now let k be Nat;
assume A3: _P[k];
a * (n + (k+1)) = a * ((n+k) + 1) by XCMPLX_1:1
.= (a * n + a * k) + a by A3,Lm2
.= a * n + (a * k + a) by RLVECT_1:def 6
.= a * n + a * (k+1) by Lm2;
hence _P[k+1];
end;
for m being Nat holds _P[m] from Ind(A1,A2);
hence thesis;
end;
theorem Th18:
for R being left_zeroed right_zeroed add-associative (non empty LoopStr),
a being Element of R,
n being Nat
holds n * a = a * n
proof
let R be left_zeroed right_zeroed
add-associative (non empty LoopStr),
a be Element of R,
n be Nat;
defpred _P[Nat] means $1 * a = a * $1;
0 * a = 0.R by Th13 .= a * 0 by Th13; then
A1: _P[0];
A2: now let k be Nat;
assume A3: _P[k];
(k + 1) * a = k * a + 1 * a by Th16
.= k * a + a by Th14
.= a * k + a * 1 by A3,Th15
.= a * (k + 1) by Th17;
hence _P[k+1];
end;
for n being Nat holds _P[n] from Ind(A1,A2);
hence thesis;
end;
theorem
for R being Abelian (non empty LoopStr),
a being Element of R,
n being Nat
holds n * a = a * n
proof
let R be Abelian (non empty LoopStr),
a be Element of R,
n be Nat;
defpred _P[Nat] means $1 * a = a * $1;
0 * a = 0.R by Th13 .= a * 0 by Th13; then
A1: _P[0];
A2: now let k be Nat;
assume _P[k];
then (k + 1) * a = a + a * k by Lm1
.= a * (k + 1) by Lm2;
hence _P[k+1];
end;
for n being Nat holds _P[n] from Ind(A1,A2);
hence thesis;
end;
theorem Th20:
for R being left_zeroed right_zeroed add-left-cancelable add-associative
left-distributive (non empty doubleLoopStr),
a,b being Element of R,
n being Nat
holds (n * a) * b = n * (a * b)
proof
let R be left_zeroed right_zeroed add-left-cancelable add-associative
left-distributive (non empty doubleLoopStr),
a,b be Element of R,
n be Nat;
defpred _P[Nat] means ($1 * a) * b = $1 * (a * b);
(0 * a) * b = 0.R * b by Th13 .= 0.R by Th1 .= 0 * (a * b) by Th13; then
A1: _P[0];
A2: now let k be Nat;
assume A3: _P[k];
((k+1) * a) * b = (a + k * a) * b by Lm1
.= a * b + k * (a * b) by A3,VECTSP_1:def 12
.= 1 * (a * b) + k * (a * b) by Th14
.= (k + 1) * (a * b) by Th16;
hence _P[k+1];
end;
for n being Nat holds _P[n] from Ind(A1,A2);
hence thesis;
end;
theorem Th21:
for R being left_zeroed right_zeroed add-right-cancelable add-associative
distributive (non empty doubleLoopStr),
a,b being Element of R,
n being Nat
holds b * (n * a) = (b * a) * n
proof
let R be left_zeroed right_zeroed add-associative
add-right-cancelable distributive (non empty doubleLoopStr),
a,b be Element of R,
n be Nat;
defpred _P[Nat] means b * ($1 * a) = (b * a) * $1;
b * (0 * a) = b * 0.R by Th13 .= 0.R by Th2 .= (b * a) * 0 by Th13; then
A1: _P[0];
A2: now let k be Nat;
assume A3: _P[k];
b * ((k+1)* a) = b * (a + k * a) by Lm1
.= b * a + (b * a) * k by A3,VECTSP_1:def 11
.= (b * a) * 1 + (b * a) * k by Th15
.= (b * a) * (k + 1) by Th17;
hence _P[k+1];
end;
for n being Nat holds _P[n] from Ind(A1,A2);
hence thesis;
end;
theorem Th22:
for R being left_zeroed right_zeroed add-associative
add-cancelable distributive (non empty doubleLoopStr),
a,b being Element of R,
n being Nat
holds (a * n) * b = a * (n * b)
proof
let R be left_zeroed right_zeroed distributive add-cancelable
add-associative (non empty doubleLoopStr),
a,b be Element of R,
n be Nat;
thus (a * n) * b = (n * a) * b by Th18
.= n * (a * b) by Th20
.= (a * b) * n by Th18
.= a * (n * b) by Th21;
end;
begin :: The Binomial Theorem
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let k,n be Nat;
redefine func n choose k -> Nat;
coherence by NEWTON:35;
end;
definition
let R be unital (non empty doubleLoopStr),
a,b be Element of R,
n be Nat;
func (a,b) In_Power n -> FinSequence of the carrier of R means :Def10:
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
defpred P[Nat,Element of R] means
for l,m being Nat st m = $1 - 1 & l = n - m
holds $2 = (n choose m) * a|^l * b|^m;
A1: for k being Nat st k in Seg(n+1)
ex y being Element of R st P[k,y]
proof
let k be Nat;
assume k in Seg(n+1);
then A2: k >= 1 & k <= n+1 by FINSEQ_1:3;
then reconsider m1 = k-1 as Nat by INT_1:18;
k-1<=n+1-1 by A2,REAL_1:49;
then m1<=n by XCMPLX_1:26;
then reconsider l1 = n-m1 as Nat by INT_1:18;
reconsider z = (n choose m1) * a|^l1 * b|^m1
as Element of R;
take z;
thus thesis;
end;
consider p being FinSequence of the carrier of R such that
A3: dom p = Seg(n+1) &
for k being Nat st k in Seg(n+1) holds P[k,p/.k] from SeqExD(A1);
take p;
thus thesis by A3,FINSEQ_1:def 3;
end;
uniqueness
proof
let f,g be FinSequence of the carrier of R;
assume
A4: len f = n + 1 &
for i,l,m being Nat st i in dom f & m = i - 1 & l = n - m
holds f/.i = (n choose m) * a|^l * b|^m;
assume
A5: len g = n + 1 &
for i,l,m being Nat st i in dom g & m = i - 1 & l = n - m
holds g/.i = (n choose m) * a|^l * b|^m;
for i being Nat st 1 <= i & i <= len f holds f.i = g.i
proof
let i be Nat;
assume A6: 1 <= i & i <= len f;
then A7: i in Seg (n+1) by A4,FINSEQ_1:3;
then A8: i in dom g by A5,FINSEQ_1:def 3;
A9: i in dom f by A4,A7,FINSEQ_1:def 3;
reconsider m = i-1 as Nat by A6,INT_1:18;
i-1<=n+1-1 by A4,A6,REAL_1:49;
then m<=n by XCMPLX_1:26;
then reconsider l = n-m as Nat by INT_1:18;
thus g.i = g/.i by A8,FINSEQ_4:def 4
.= (n choose m) * a|^l * b|^m by A5,A8
.= f/.i by A4,A9
.= f.i by A9,FINSEQ_4:def 4;
end;
hence f = g by A4,A5,FINSEQ_1:18;
end;
end;
theorem Th23:
for R being right_zeroed unital (non empty doubleLoopStr),
a,b being Element of R
holds (a,b) In_Power 0 = <*1.R*>
proof
let R be right_zeroed unital (non empty doubleLoopStr),
a,b being Element of R;
set p = (a,b) In_Power 0;
A1: len p = 0 + 1 by Def10 .= 1;
then A2: dom p = {1} by FINSEQ_1:4,def 3;
then A3: 1 in dom p by TARSKI:def 1;
then consider i being Nat such that A4: i in dom p;
A5: i = 1 by A2,A4,TARSKI:def 1;
then reconsider m = i - 1 as Nat by INT_1:18;
reconsider l = 0 - m as Nat by A5;
p.1 = p/.1 by A3,FINSEQ_4:def 4
.= (0 choose m) * a|^l * b|^m by A3,A5,Def10
.= 1 * a|^0 * 1.R by A5,Th8,NEWTON:27
.= 1 * 1.R * 1.R by Th8
.= 1.R * 1.R by Th14
.= 1.R by GROUP_1:def 4;
hence thesis by A1,FINSEQ_1:57;
end;
theorem Th24:
for R being right_zeroed unital (non empty doubleLoopStr),
a,b being Element of R,
n being Nat
holds ((a,b) In_Power n).1 = a|^n
proof
let R be right_zeroed unital (non empty doubleLoopStr),
a,b be Element of R, n be Nat;
reconsider m = 1 - 1 as Nat by NEWTON:27;
A1: 0 <= n by NAT_1:18;
reconsider l = n - m as Nat;
len((a,b) In_Power n) = n + 1 by Def10;
then A2: dom(((a,b) In_Power n)) = Seg(n + 1) by FINSEQ_1:def 3;
0 + 1 <= n + 1 by A1,AXIOMS:24;
then A3: 1 in dom(((a,b) In_Power n)) by A2,FINSEQ_1:3;
hence ((a,b) In_Power n).1 = ((a,b) In_Power n)/.1 by FINSEQ_4:def 4
.= (n choose 0) * a|^l * b|^m by A3,Def10
.= 1 * a|^n * b|^0 by NEWTON:29
.= a|^n * b|^0 by Th14
.= a|^n * 1.R by Th8
.= a|^n by GROUP_1:def 4;
end;
theorem Th25:
for R being right_zeroed unital (non empty doubleLoopStr),
a,b being Element of R,
n being Nat
holds ((a,b) In_Power n).(n+1) = b|^n
proof
let R be right_zeroed unital (non empty doubleLoopStr),
a,b be Element of R,
n be Nat;
1 <= n + 1 by NAT_1:37;
then reconsider m = n + 1 - 1 as Nat by INT_1:18;
A1: m = n by XCMPLX_1:26;
then reconsider l = n - m as Nat by INT_1:18;
A2: l = n - n by XCMPLX_1:26 .= 0 by XCMPLX_1:14;
len((a,b) In_Power n) = n + 1 by Def10;
then dom((a,b) In_Power n) = Seg(n + 1) by FINSEQ_1:def 3;
then A3: n + 1 in dom((a,b) In_Power n) by FINSEQ_1:6;
hence ((a,b) In_Power n).(n+1) = ((a,b) In_Power n)/.(n+1) by FINSEQ_4:def 4
.= (n choose n) * a|^0 * b|^n by A1,A2,A3,Def10
.= 1 * a|^0 * b|^n by NEWTON:31
.= 1 * 1.R * b|^n by Th8
.= 1.R * b|^n by Th14
.= b|^n by GROUP_1:def 4;
end;
theorem
for R being Abelian add-associative left_zeroed right_zeroed
commutative associative add-cancelable
distributive unital (non empty doubleLoopStr),
a,b being Element of R,
n being Nat
holds (a+b)|^n = Sum((a,b) In_Power n)
proof
let R be add-associative left_zeroed right_zeroed distributive associative
Abelian add-cancelable commutative unital (non empty doubleLoopStr),
a,b be Element of R, n be Nat;
defpred _P[Nat] means (a+b)|^$1 = Sum((a,b) In_Power $1);
A1: _P[0] proof
thus (a+b)|^0 = 1.R by Th8
.= Sum <*1.R*> by Th3
.= Sum((a,b) In_Power 0) by Th23;
end;
A2: for n being Nat st _P[n] holds _P[n+1] proof
let n be Nat;
assume _P[n];
then A3: (a+b)|^(n+1)
= Sum((a,b) In_Power n) * (a + b) by Th9
.= Sum((a,b) In_Power n) * a + Sum
((a,b) In_Power n) * b by VECTSP_1:def 11
.= Sum(((a,b) In_Power n) * a) + Sum((a,b) In_Power n) * b by Th5
.= Sum(((a,b) In_Power n) * a) + Sum(((a,b) In_Power n) * b)by Th5;
set G1 = (((a,b) In_Power n) * a)^<*0.R*>;
set G2 = <*0.R*>^(((a,b) In_Power n) * b);
A4: Seg(len(((a,b) In_Power n) * a))
= dom(((a,b) In_Power n) * a) by FINSEQ_1:def 3
.= dom((a,b) In_Power n) by POLYNOM1:def 3
.= Seg(len((a,b) In_Power n)) by FINSEQ_1:def 3;
A5: Seg(len(((a,b) In_Power n) * b))
= dom(((a,b) In_Power n) * b) by FINSEQ_1:def 3
.= dom((a,b) In_Power n) by POLYNOM1:def 3
.= Seg(len((a,b) In_Power n)) by FINSEQ_1:def 3;
len G1 = len(((a,b) In_Power n) * a) + len<*0.R*> by FINSEQ_1:35
.= len(((a,b) In_Power n) * a) + 1 by FINSEQ_1:57
.= len((a,b) In_Power n) + 1 by A4,FINSEQ_1:8
.= n + 1 + 1 by Def10;
then reconsider F1 = G1 as Element of (n+1+1)-tuples_on the carrier of R
by FINSEQ_2:110;
len G2 = len(((a,b) In_Power n) * b) + len<*0.R*> by FINSEQ_1:35
.= len(((a,b) In_Power n) * b) + 1 by FINSEQ_1:57
.= len((a,b) In_Power n) + 1 by A5,FINSEQ_1:8
.= n + 1 + 1 by Def10;
then reconsider F2 = G2 as Element of (n+1+1)-tuples_on the carrier of R
by FINSEQ_2:110;
A6: len F1 = n+1+1 by FINSEQ_2:109;
A7: len F2 = n+1+1 by FINSEQ_2:109;
A8: dom F1 = Seg(len F1) by FINSEQ_1:def 3
.= dom F2 by A6,A7,FINSEQ_1:def 3;
A9: Sum F1 = Sum(((a,b) In_Power n) * a) + Sum<*0.R*> by RLVECT_1:58
.= Sum(((a,b) In_Power n) * a) + 0.R by Th3
.= Sum(((a,b) In_Power n) * a) by RLVECT_1:def 7;
Sum F2 = Sum<*0.R*> + Sum(((a,b) In_Power n) * b) by RLVECT_1:58
.= 0.R + Sum(((a,b) In_Power n) * b) by Th3
.= Sum(((a,b) In_Power n) * b) by ALGSTR_1:def 5;
then A10: Sum(G1+G2) = Sum(((a,b) In_Power n) * a) + Sum
(((a,b) In_Power n) * b)
by A8,A9,Th7;
set F = F1 + F2;
A11: Seg(len F) = dom F by FINSEQ_1:def 3
.= dom F1 by A8,Def4
.= Seg(len F1) by FINSEQ_1:def 3;
then A12: len F = n + 1 + 1 by A6,FINSEQ_1:8;
A13: for i being Nat st 1 <= i & i <= len((a,b) In_Power (n+1))
holds F.i = ((a,b) In_Power (n+1)).i
proof
let i be Nat;
assume A14: 1 <= i & i <= len((a,b) In_Power (n+1));
A15: len((a,b) In_Power (n+1)) = n+1+1 by Def10;
then A16: dom((a,b) In_Power (n+1)) = Seg(n+1+1) by FINSEQ_1:def 3;
then A17: i in dom((a,b) In_Power (n+1)) by A14,A15,FINSEQ_1:3;
A18: i in Seg(n+1+1) by A14,A15,FINSEQ_1:3;
reconsider j = i - 1 as Nat by A14,INT_1:18;
A19: i in dom F by A6,A11,A18,FINSEQ_1:def 3;
A20: i in dom F1 by A6,A18,FINSEQ_1:def 3;
A21: i in dom F2 by A7,A18,FINSEQ_1:def 3;
A22: i = j+1 by XCMPLX_1:27;
A23: n+1+1>=1 by NAT_1:37;
set x = ((a,b) In_Power n)/.j;
set r = ((a,b) In_Power n)/.i;
set r1 = F1/.i;
set r2 = F2/.i;
A24: i <= len(F1+F2) by A12,A14,Def10;
A25: i in {1} implies F.i = ((a,b) In_Power (n+1)).i
proof
assume i in {1};
then A26: i = 1 by TARSKI:def 1;
n >= 0 by NAT_1:18;
then n+1 >= 0+1 by AXIOMS:24;
then 1 in Seg (n+1) by FINSEQ_1:3;
then A27: 1 in Seg len(((a,b) In_Power n)) by Def10;
then A28: 1 in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
A29: 1 in dom (((a,b) In_Power n) * a) by A4,A27,FINSEQ_1:def 3;
A30: r = ((a,b) In_Power n).i by A26,A28,FINSEQ_4:def 4;
A31: r1 = ((((a,b) In_Power n) * a)^<*0.R*>).1
by A20,A26,FINSEQ_4:def 4
.= (((a,b) In_Power n) * a).1 by A29,FINSEQ_1:def 7
.= (((a,b) In_Power n) * a)/.1 by A29,FINSEQ_4:def 4
.= (((a,b) In_Power n)/.1) * a by A28,POLYNOM1:def 3
.= a|^n * a by A26,A30,Th24
.= a|^(n+1) by Th9;
A32: r2 = (<*0.R*>^(((a,b) In_Power n) * b)).1
by A21,A26,FINSEQ_4:def 4
.= 0.R by FINSEQ_1:58;
thus F.i = F/.i by A19,FINSEQ_4:def 4
.= r1 + F2/.i by A8,A14,A24,Def4
.= a|^(n+1) by A31,A32,RLVECT_1:def 7
.= ((a,b) In_Power (n+1)).i by A26,Th24;
end;
A33: i in {n+1+1} implies F.i = ((a,b) In_Power (n+1)).i
proof
assume A34: i in {n+1+1};
then A35: i = n+1+1 by TARSKI:def 1;
dom F = Seg(n+1+1) by A6,A11,FINSEQ_1:def 3;
then A36: i in dom F by A14,A35,FINSEQ_1:3;
A37: j = n+1+1-1 by A34,TARSKI:def 1 .= n+1 by XCMPLX_1:26;
A38: n+1 = len ((a,b) In_Power n) by Def10
.= len(((a,b) In_Power n) * a) by A4,FINSEQ_1:8;
n+1 in Seg (n+1) by FINSEQ_1:6;
then A39: j in Seg len (((a,b) In_Power n)) by A37,Def10;
then A40: j in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
A41: j in dom (((a,b) In_Power n) * b) by A5,A39,FINSEQ_1:def 3;
A42: x = ((a,b) In_Power n).(n+1) by A37,A40,FINSEQ_4:def 4
.= b|^n by Th25;
A43: r1 = ((((a,b) In_Power n)*a)^<*0.R*>).
(len(((a,b) In_Power n)*a)+1)
by A20,A35,A38,FINSEQ_4:def 4
.= 0.R by FINSEQ_1:59;
A44: r2 = (<*0.R*>^(((a,b) In_Power n) * b)).(1+(n+1))
by A21,A35,FINSEQ_4:def 4
.= (<*0.R*>^(((a,b) In_Power n) * b)).(len <*0.R*> + j)
by A37,FINSEQ_1:56
.= (((a,b) In_Power n) * b).j by A41,FINSEQ_1:def 7
.= (((a,b) In_Power n) * b)/.j by A41,FINSEQ_4:def 4
.= b|^n * b by A40,A42,POLYNOM1:def 3
.= b|^(n+1) by Th9;
thus F.i = F/.i by A36,FINSEQ_4:def 4
.= 0.R + r2 by A8,A14,A24,A43,Def4
.= b|^(n+1) by A44,ALGSTR_1:def 5
.= ((a,b) In_Power (n+1)).i by A35,Th25;
end;
A45: i in {k where k is Nat: k>1 & k<n+1+1}
implies F.i = ((a,b) In_Power (n+1)).i
proof
assume i in {k where k is Nat: 1 < k & k < n+1+1};
then A46: ex k being Nat st k = i & 1 < k & k < n+1+1;
then A47: 1 <= i & i <= n+1 by NAT_1:38;
then i in Seg (n+1) by FINSEQ_1:3;
then A48: i in Seg len ((a,b) In_Power n) by Def10;
then A49: i in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
A50: i in dom (((a,b) In_Power n) * a) by A4,A48,FINSEQ_1:def 3;
reconsider m1 = i-1 as Nat by A46,INT_1:18;
i-1 <= n+1-1 by A47,REAL_1:49;
then m1 <= n by XCMPLX_1:26;
then reconsider l1 = n - m1 as Nat by INT_1:18;
A51: 1 <= j & j+1 <= n+1+1 by A22,A46,NAT_1:38;
A52: 1 <= j & j <= n+1 by A22,A46,AXIOMS:24,NAT_1:38;
then j in Seg (n+1) by FINSEQ_1:3;
then A53: j in Seg len ((a,b) In_Power n) by Def10;
then A54: j in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
A55: j in dom (((a,b) In_Power n) * b) by A5,A53,FINSEQ_1:def 3;
reconsider m2 = j - 1 as Nat by A51,INT_1:18;
A56: m2 + 1 = i - 1 by XCMPLX_1:27;
l1 = n-i+1 by XCMPLX_1:37 .= n+1-i by XCMPLX_1:29;
then A57: l1+1 = n+1-(m2+1) by A56,XCMPLX_1:37;
j < n+1 by A22,A46,AXIOMS:24;
then m2<n+1-1 by REAL_1:54
;
then A58: m2<n+(1-1) by XCMPLX_1:29;
j-1<=n+1-1 by A52,REAL_1:49;
then m2<=n by XCMPLX_1:26;
then reconsider l2 = n-m2 as Nat by INT_1:18;
A59: m1 = m2+1 by XCMPLX_1:27;
A60: j in dom (((a,b) In_Power n) * b) by A5,A53,FINSEQ_1:def 3;
A61: r1=((((a,b) In_Power n)*a)^<*0.R*>).i by A20,FINSEQ_4:def 4;
A62: r2=(<*0.R*>^(((a,b) In_Power n)*b)).i by A21,FINSEQ_4:def 4;
A63: l2 = l1 + 1 by XCMPLX_1:37;
A64: r1 = (((a,b) In_Power n) * a).i by A50,A61,FINSEQ_1:def 7
.= (((a,b) In_Power n) * a)/.i by A50,FINSEQ_4:def 4
.= r * a by A49,POLYNOM1:def 3;
A65: r2 = (<*0.R*>^(((a,b) In_Power n) * b)).(len <*0.R*> +j)
by A22,A62,FINSEQ_1:57
.= (((a,b) In_Power n) * b).j by A55,FINSEQ_1:def 7
.= (((a,b) In_Power n) * b)/.j by A60,FINSEQ_4:def 4
.= x * b by A54,POLYNOM1:def 3;
thus
F.i = F/.i by A19,FINSEQ_4:def 4
.= F1/.i + x * b by A8,A14,A24,A65,Def4
.= ((n choose m1) * a|^l1 * b|^m1) * a + x * b by A49,A64,Def10
.= (a|^l1 * (n choose m1) * b|^m1) * a + x * b by Th18
.= a * (a|^l1 *((n choose m1) * b|^m1)) + x * b by Th22
.= a * a|^l1 *((n choose m1) * b|^m1) + x * b
by VECTSP_1:def 16
.= a|^(l1+1) * ((n choose m1) * b|^m1) + x * b by Th9
.= a|^(l1+1) * ((n choose m1) * b|^m1) +
b|^m2 * ((n choose m2) * a|^l2) * b by A54,Def10
.= a|^(l1+1) * ((n choose m1) * b|^m1) +
(b|^m2 * b) * ((n choose m2) * a|^l2) by VECTSP_1:def 16
.= a|^(l1+1) * ((n choose (m2+1)) * b|^(m2+1)) +
b|^(m2+1) * ((n choose m2) * a|^l2) by A59,Th9
.= (b|^(m2+1) * a|^(l1+1)) * (n choose (m2+1)) +
b|^(m2+1) * ((n choose m2) * a|^l2) by Th21
.= b|^(m2+1) * ((n choose (m2+1)) * a|^(l1+1)) +
b|^(m2+1) * ((n choose m2) * a|^l2) by Th21
.= b|^(m2+1) * (a|^(l1+1) * (n choose (m2+1))) +
b|^(m2+1) * ((n choose m2) * a|^l2) by Th18
.= ((a|^(l1+1) * (n choose (m2+1))) +
((n choose m2) * a|^l2)) * b|^(m2+1) by VECTSP_1:def 18
.= (((n choose (m2+1)) * a|^(l1+1)) +
((n choose m2) * a|^(l1+1))) * b|^(m2+1) by A63,Th18
.= ((n choose (m2+1)) + (n choose m2)) * a|^(l1+1) * b|^(m2+1)
by Th16
.= ((n+1) choose (m2+1)) * a|^(l1+1) * b|^(m2+1)
by A58,NEWTON:32
.= ((a,b) In_Power (n+1))/.i by A17,A56,A57,Def10
.= ((a,b) In_Power (n+1)).i by A17,FINSEQ_4:def 4;
end;
now assume i in {1} \/ {k where k is Nat: 1<k & k<n+1+1} \/ {n+1+1};
then i in {1} \/ {k where k is Nat: 1<k & k<n+1+1}
or i in {n+1+1} by XBOOLE_0:def 2;
hence F.i = ((a,b) In_Power (n+1)).i by A25,A33,A45,XBOOLE_0:def 2
;
end;
hence thesis by A16,A17,A23,NEWTON:5;
end;
len ((a,b) In_Power (n+1)) = len F by A12,Def10;
hence thesis by A3,A10,A13,FINSEQ_1:18;
end;
for n being Nat holds _P[n] from Ind(A1,A2);
hence thesis;
end;