Copyright (c) 2000 Association of Mizar Users
environ
vocabulary RLVECT_1, ALGSTR_1, VECTSP_1, VECTSP_2, BINOM, BINOP_1, LATTICES,
REALSET1, FINSEQ_1, FILTER_2, ALGSTR_2, COLLSP, BOOLE, ARYTM_1, GROUP_1,
RELAT_1, FUNCT_1, FUNCT_7, ARYTM_3, FINSEQ_4, PRELAMB, MCART_1, SETFAM_1,
RLVECT_3, SUBSET_1, GCD_1, LATTICE3, SQUARE_1, NEWTON, FINSET_1, INT_3,
WAYBEL_0, TARSKI, NORMSP_1, GR_CY_1, IDEAL_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CQC_SIM1, FINSET_1, FUNCT_1,
FINSEQ_1, VECTSP_1, INT_3, NORMSP_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1,
RELSET_1, RLVECT_1, PARTFUN1, FUNCT_2, ALGSTR_1, PRE_TOPC, GR_CY_1,
PRE_CIRC, MCART_1, DOMAIN_1, FINSEQ_4, POLYNOM1, SETFAM_1, STRUCT_0,
GROUP_1, BINOP_1, VECTSP_2, FUNCT_7, REALSET1, GCD_1, BINOM;
constructors INT_3, CQC_SIM1, PRE_CIRC, GROUP_2, ALGSEQ_1, BINOM, GCD_1,
ALGSTR_2, DOMAIN_1, POLYNOM1, MONOID_0, BINOP_1, PRE_TOPC;
clusters INT_3, RELSET_1, FINSET_1, SUBSET_1, VECTSP_2, STRUCT_0, PRE_TOPC,
FINSEQ_1, FINSEQ_5, XBOOLE_0, POLYNOM1, INT_1, GCD_1, BINOM, REALSET1,
VECTSP_1, NAT_1, XREAL_0, MEMBERED, RELAT_1, FUNCT_2, PRE_CIRC, NUMBERS,
ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems INT_3, CQC_SIM1, TARSKI, ZFMISC_1, RLVECT_1, REALSET1, VECTSP_1,
GCD_1, FUNCT_1, FUNCT_2, POLYNOM1, VECTSP_2, PRE_TOPC, RELAT_1, FINSET_1,
PRE_CIRC, NAT_1, GR_CY_1, ALGSTR_1, NORMSP_1, REAL_1, AXIOMS, MCART_1,
FINSEQ_1, FINSEQ_2, FINSEQ_3, JORDAN3, SETFAM_1, BINOP_1, INT_1, FUNCT_7,
FINSEQ_4, FINSEQ_5, POLYNOM2, BINOM, XBOOLE_0, XBOOLE_1, XCMPLX_0,
XCMPLX_1, ORDINAL2;
schemes NAT_1, RECDEF_1, FUNCT_2, POLYNOM2, BINOM, FINSEQ_2;
begin :: Preliminaries
definition
cluster add-associative left_zeroed right_zeroed (non empty LoopStr);
existence
proof consider R being non degenerated comRing; take R; thus thesis; end;
end;
definition
cluster
Abelian left_zeroed right_zeroed add-cancelable well-unital add-associative
associative commutative distributive non trivial (non empty doubleLoopStr);
existence
proof consider R being non degenerated comRing; take R; thus thesis; end;
end;
theorem Th1:
for V being add-associative left_zeroed right_zeroed (non empty LoopStr),
v,u being Element of V
holds Sum <* v,u *> = v + u
proof let V be add-associative left_zeroed right_zeroed (non empty LoopStr),
v,u be Element of V;
<* v,u *> = <* v *> ^ <* u *> by FINSEQ_1:def 9;
then Sum<* v,u *> = Sum<* v *> + Sum<* u *> by RLVECT_1:58 .= v + Sum
<* u *> by BINOM:3
.= v + u by BINOM:3;
hence thesis;
end;
begin :: Ideals
definition
let L be non empty LoopStr, F being Subset of L;
attr F is add-closed means :Def1:
for x, y being Element of L st x in F & y in F holds x+y in
F;
end;
definition
let L be non empty HGrStr, F be Subset of L;
attr F is left-ideal means :Def2:
for p, x being Element of L st x in F holds p*x in F;
attr F is right-ideal means :Def3:
for p, x being Element of L st x in F holds x*p in F;
end;
definition
let L be non empty LoopStr;
cluster add-closed (non empty Subset of L);
existence proof set M = the carrier of L;
for u being set holds u in M implies u in the carrier of L;
then reconsider M as Subset of L by TARSKI:def 3;
reconsider M as non empty Subset of L;
take M;
for x, y being Element of L st x in M & y in M holds x+y in M
;
hence thesis by Def1;
end;
end;
definition
let L be non empty HGrStr;
cluster left-ideal (non empty Subset of L);
existence proof set M = the carrier of L;
for u being set holds u in M implies u in the carrier of L;
then reconsider M as Subset of L by TARSKI:def 3;
reconsider M as non empty Subset of L;
take M;
for p, x being Element of L st x in M holds p*x in M;
hence thesis by Def2;
end;
cluster right-ideal (non empty Subset of L);
existence proof set M = the carrier of L;
for u being set holds u in M implies u in the carrier of L;
then reconsider M as Subset of L by TARSKI:def 3;
reconsider M as non empty Subset of L;
take M;
for p, x being Element of L st x in M holds x*p in M;
hence thesis by Def3;
end;
end;
definition
let L be non empty doubleLoopStr;
cluster add-closed left-ideal right-ideal (non empty Subset of L);
existence proof set M = the carrier of L;
for u being set holds u in M implies u in the carrier of L;
then reconsider M as Subset of L by TARSKI:def 3;
reconsider M as non empty Subset of L;
take M;
A1: for x,y being Element of L st x in M & y in M holds x+y in
M;
A2: for p,x being Element of L st x in M holds p*x in M;
for p, x being Element of L st x in M holds x*p in M;
hence thesis by A1,A2,Def1,Def2,Def3;
end;
cluster add-closed right-ideal (non empty Subset of L);
existence proof set M = the carrier of L;
for u being set holds u in M implies u in the carrier of L;
then reconsider M as Subset of L by TARSKI:def 3;
reconsider M as non empty Subset of L;
take M;
A3: for x,y being Element of L st x in M & y in M holds x+y in
M;
for p, x being Element of L st x in M holds x*p in M;
hence thesis by A3,Def1,Def3;
end;
cluster add-closed left-ideal (non empty Subset of L);
existence proof set M = the carrier of L;
for u being set holds u in M implies u in the carrier of L;
then reconsider M as Subset of L by TARSKI:def 3;
reconsider M as non empty Subset of L;
take M;
A4: for x,y being Element of L st x in M & y in M holds x+y in
M;
for p, x being Element of L st x in M holds p*x in M;
hence thesis by A4,Def1,Def2;
end;
end;
definition
let R be commutative (non empty HGrStr);
cluster left-ideal -> right-ideal (non empty Subset of R);
coherence proof let I be non empty Subset of R; assume I is left-ideal;
then for p,x being Element of R st x in I holds x*p in
I by Def2;
hence thesis by Def3;
end;
cluster right-ideal -> left-ideal (non empty Subset of R);
coherence proof let I be non empty Subset of R; assume I is right-ideal;
then for p,x being Element of R st x in I holds p*x in
I by Def3;
hence thesis by Def2;
end;
end;
definition
let L be non empty doubleLoopStr;
mode Ideal of L is add-closed left-ideal right-ideal (non empty Subset of L);
end;
definition
let L be non empty doubleLoopStr;
mode RightIdeal of L is add-closed right-ideal (non empty Subset of L);
end;
definition
let L be non empty doubleLoopStr;
mode LeftIdeal of L is add-closed left-ideal (non empty Subset of L);
end;
theorem Th2:
for R being right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr),
I being left-ideal (non empty Subset of R)
holds 0.R in I
proof let R be right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr);
let I be left-ideal (non empty Subset of R);
consider a being Element of I; 0.R*a in I by Def2;
hence thesis by BINOM:1;
end;
theorem Th3:
for R being left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
I being right-ideal (non empty Subset of R)
holds 0.R in I
proof let R be left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr);
let I be right-ideal (non empty Subset of R);
consider a being Element of I; a*0.R in I by Def3;
hence thesis by BINOM:2;
end;
theorem Th4:
for L being right_zeroed (non empty doubleLoopStr) holds {0.L} is add-closed
proof let L be right_zeroed (non empty doubleLoopStr);
let x,y be Element of L;
assume x in {0.L} & y in {0.L}; then x = 0.L & y= 0.L by TARSKI:def 1;
then x + y = 0.L by RLVECT_1:def 7;
hence x + y in {0.L} by TARSKI:def 1;
end;
theorem Th5:
for L being left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr)
holds {0.L} is left-ideal
proof let L be left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr);
let p,x be Element of L;
assume x in {0.L}; then A1: x = 0.L by TARSKI:def 1;
reconsider p' = p as Element of L;
p'*x = 0.L by A1,BINOM:2;
hence p*x in {0.L} by TARSKI:def 1;
end;
theorem Th6:
for L being right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr)
holds {0.L} is right-ideal
proof let L be right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr);
let p,x be Element of L;
assume x in {0.L}; then A1: x = 0.L by TARSKI:def 1;
reconsider p' = p as Element of L;
x*p' = 0.L by A1,BINOM:1;
hence x*p in {0.L} by TARSKI:def 1;
end;
theorem Th7:
for L being add-associative right_zeroed right_complementable
distributive (non empty doubleLoopStr)
holds {0.L} is Ideal of L
proof let L be add-associative right_zeroed right_complementable
distributive (non empty doubleLoopStr);
A1: {0.L} is add-closed proof let x,y be Element of L;
assume x in {0.L} & y in {0.L}; then x = 0.L & y= 0.L by TARSKI:def 1;
then x + y = 0.L by RLVECT_1:10;
hence x + y in {0.L} by TARSKI:def 1;
end;
A2: {0.L} is left-ideal proof let p,x be Element of L;
assume x in {0.L}; then x = 0.L by TARSKI:def 1;
then p*x = 0.L by VECTSP_1:36;
hence p*x in {0.L} by TARSKI:def 1;
end;
{0.L} is right-ideal proof let p,x be Element of L;
assume x in {0.L}; then x = 0.L by TARSKI:def 1;
then x*p = 0.L by VECTSP_1:39;
hence x*p in {0.L} by TARSKI:def 1;
end;
hence thesis by A1,A2;
end;
theorem
for L being add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr)
holds {0.L} is LeftIdeal of L
proof let L be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
A1: {0.L} is add-closed proof
let x,y be Element of L; assume x in {0.L} & y in
{0.L};
then x = 0.L & y= 0.L by TARSKI:def 1; then x+y = 0.L by RLVECT_1:10;
hence x + y in {0.L} by TARSKI:def 1;
end;
{0.L} is left-ideal proof let p,x be Element of L;
assume x in {0.L}; then x = 0.L by TARSKI:def 1;
then p*x = 0.L by VECTSP_1:36;
hence p*x in {0.L} by TARSKI:def 1;
end;
hence thesis by A1;
end;
theorem
for L being add-associative right_zeroed right_complementable
left-distributive (non empty doubleLoopStr)
holds {0.L} is RightIdeal of L
proof let L be add-associative right_zeroed right_complementable
left-distributive (non empty doubleLoopStr);
A1: {0.L} is add-closed proof let x,y be Element of L;
assume x in {0.L} & y in {0.L}; then x = 0.L & y= 0.L by TARSKI:def 1;
then x + y = 0.L by RLVECT_1:10;
hence x + y in {0.L} by TARSKI:def 1;
end;
{0.L} is right-ideal proof let p,x be Element of L;
assume x in {0.L};
then x = 0.L by TARSKI:def 1; then x*p = 0.L by VECTSP_1:39;
hence x*p in {0.L} by TARSKI:def 1;
end;
hence thesis by A1;
end;
theorem Th10:
for L being non empty doubleLoopStr holds the carrier of L is Ideal of L
proof let L be non empty doubleLoopStr;
the carrier of L c= the carrier of L;
then reconsider cL = the carrier of L as Subset of L;
A1: cL is add-closed proof let x, y be Element of L;
thus thesis; end;
A2: cL is left-ideal proof let x, y be Element of L;
thus thesis; end;
cL is right-ideal proof let x, y be Element of L;
thus thesis; end;
hence thesis by A1,A2;
end;
theorem Th11:
for L being non empty doubleLoopStr holds the carrier of L is LeftIdeal of L
proof let L be non empty doubleLoopStr;
the carrier of L c= the carrier of L;
then reconsider cL = the carrier of L as Subset of L;
A1: cL is add-closed proof let x, y be Element of L;
thus thesis; end;
cL is left-ideal proof let x, y be Element of L;
thus thesis; end;
hence thesis by A1;
end;
theorem Th12:
for L being non empty doubleLoopStr holds the carrier of L is RightIdeal of L
proof let L be non empty doubleLoopStr;
the carrier of L c= the carrier of L;
then reconsider cL = the carrier of L as Subset of L;
A1: cL is add-closed proof let x, y be Element of L;
thus thesis; end;
cL is right-ideal proof let x, y be Element of L;
thus thesis; end;
hence thesis by A1;
end;
definition
let R be left_zeroed right_zeroed add-cancelable
distributive (non empty doubleLoopStr),
I be Ideal of R;
redefine attr I is trivial means
I = {0.R};
compatibility proof
now assume I is trivial;
then consider x being set such that A1: I = {x} by REALSET1:def 12;
0.R in {x} by A1,Th3;
hence I = {0.R} by A1,TARSKI:def 1;
end;
hence thesis by REALSET1:def 12;
end;
end;
definition
let S be 1-sorted,
T be Subset of S;
attr T is proper means :Def5:
T <> the carrier of S;
end;
definition
let S be non empty 1-sorted;
cluster proper Subset of S;
existence proof for u being set holds u in {} implies u in the carrier of S;
then reconsider e = {} as Subset of S by TARSKI:def 3;
reconsider e as Subset of S;
take e; thus thesis by Def5;
end;
end;
definition
let R be non trivial left_zeroed right_zeroed add-cancelable
distributive (non empty doubleLoopStr);
cluster proper Ideal of R;
existence proof
reconsider M = {0.R} as Ideal of R by Th4,Th5,Th6;
ex a being Element of R st a <> 0.R proof
assume A1: not(ex a being Element of R st a <> 0.R);
A2: for u being set holds u in {0.R} implies u in the carrier of R;
for u being set holds u in the carrier of R implies u in {0.R} proof
let u be set; assume u in the carrier of R;
then reconsider u as Element of R; u = 0.R by A1;
hence thesis by TARSKI:def 1;
end;
then A3: the carrier of R = {0.R} by A2,TARSKI:2;
the carrier of R is non trivial by REALSET1:def 13;
hence thesis by A3,REALSET1:def 12;
end;
then {0.R} <> the carrier of R by TARSKI:def 1; then M is proper by Def5;
hence thesis;
end;
end;
theorem Th13:
for L being add-associative right_zeroed right_complementable
left-distributive left_unital (non empty doubleLoopStr),
I being left-ideal (non empty Subset of L),
x being Element of L
st x in I holds -x in I
proof let L be add-associative right_zeroed right_complementable
left-distributive left_unital (non empty doubleLoopStr);
let I be left-ideal (non empty Subset of L);
let x being Element of L;
assume x in I;
then A1: (- 1_ L)*x in I by Def2;
0. L = 0.L*x by VECTSP_1:39 .= (1_ L + (- 1_ L))*x by RLVECT_1:def 10
.= 1_ L*x + (- 1_ L)*x by VECTSP_1:def 12
.= x + (- 1_ L)*x by VECTSP_1:def 19;
hence - x in I by A1,RLVECT_1:def 10;
end;
theorem Th14:
for L being add-associative right_zeroed right_complementable
right-distributive right_unital (non empty doubleLoopStr),
I being right-ideal (non empty Subset of L),
x being Element of L
st x in I holds -x in I
proof let L be add-associative right_zeroed right_complementable
right-distributive right_unital (non empty doubleLoopStr);
let I be right-ideal (non empty Subset of L);
let x being Element of L;
assume x in I;
then A1: x*(- 1_ L) in I by Def3;
0. L = x*0.L by VECTSP_1:36 .= x*(1_ L + (- 1_ L)) by RLVECT_1:def 10
.= x*1_ L + x*(- 1_ L) by VECTSP_1:def 11
.= x + x*(- 1_ L) by VECTSP_1:def 13;
hence -x in I by A1,RLVECT_1:def 10;
end;
theorem
for L being add-associative right_zeroed right_complementable
left-distributive left_unital (non empty doubleLoopStr),
I being LeftIdeal of L, x,y being Element of L
st x in I & y in I holds x-y in I
proof let L being add-associative right_zeroed right_complementable
left-distributive left_unital (non empty doubleLoopStr);
let I being LeftIdeal of L; let x, y being Element of L;
assume A1: x in I & y in I; then - y in I by Th13; then x + (- y) in
I by A1,Def1;
hence x - y in I by RLVECT_1:def 11;
end;
theorem
for L being add-associative right_zeroed right_complementable
right-distributive right_unital (non empty doubleLoopStr),
I being RightIdeal of L, x,y being Element of L
st x in I & y in I holds x-y in I
proof let L being add-associative right_zeroed right_complementable
right-distributive right_unital (non empty doubleLoopStr);
let I being RightIdeal of L; let x, y being Element of L;
assume A1: x in I & y in I; then - y in I by Th14; then x + (- y) in
I by A1,Def1
;
hence x - y in I by RLVECT_1:def 11;
end;
theorem Th17:
for R being left_zeroed right_zeroed add-cancelable
add-associative distributive (non empty doubleLoopStr),
I being add-closed right-ideal (non empty Subset of R),
a being Element of I, n being Nat
holds n*a in I
proof let R be left_zeroed right_zeroed add-cancelable
add-associative distributive (non empty doubleLoopStr),
I be add-closed right-ideal (non empty Subset of R),
a be Element of I, n be Nat;
defpred P[Nat] means $1*a in I;
0*a = 0.R by BINOM:13;
then A1: P[0] by Th3;
A2: for n being Nat holds P[n] implies P[n+1] proof
let n be Nat;
assume A3: n*a in I;
(n+1)*a = 1*a + n*a by BINOM:16 .= a + n*a by BINOM:14;
hence thesis by A3,Def1;
end;
for n being Nat holds P[n] from Ind(A1,A2);
hence thesis;
end;
theorem
for R being unital left_zeroed right_zeroed add-cancelable associative
distributive (non empty doubleLoopStr),
I being right-ideal (non empty Subset of R),
a being Element of I, n being Nat
st n <> 0 holds a|^n in I
proof let R be unital left_zeroed right_zeroed add-cancelable associative
distributive (non empty doubleLoopStr),
I be right-ideal (non empty Subset of R),
a be Element of I, n be Nat;
defpred P[Nat] means a|^$1 in I;
assume n <> 0; then A1: 1 <= n by RLVECT_1:99;
a|^1 = a by BINOM:8;
then A2: P[1];
A3: for n being Nat st 1 <= n holds P[n] implies P[n+1] proof
let n be Nat; assume 1 <= n; assume A4: a|^n in I;
a|^(n+1) = (a|^n)*(a|^1) by BINOM:11;
hence thesis by A4,Def3;
end;
for n being Nat st 1 <= n holds P[n] from Ind2(A2,A3);
hence thesis by A1;
end;
definition
let R be non empty LoopStr,
I be add-closed (non empty Subset of R);
func add|(I,R) -> BinOp of I equals :Def6:
(the add of R)|[:I,I:];
coherence proof reconsider f = (the add of R)|[:I,I:] as
Function of [:I,I:],the carrier of R by FUNCT_2:38;
A1: dom f = [:I,I:] by FUNCT_2:def 1;
for x being set st x in [:I,I:] holds f.x in I proof
let x be set; assume A2: x in [:I,I:];
then consider u,v being set such that
A3: u in I & v in I & x = [u,v] by ZFMISC_1:def 2;
reconsider u,v as Element of R by A3;
reconsider u,v as Element of R;
f.x = (the add of R).[u,v] by A1,A2,A3,FUNCT_1:70 .= u + v by RLVECT_1:def
3;
hence thesis by A3,Def1;
end;
hence thesis by A1,FUNCT_2:5;
end;
end;
definition
let R be non empty HGrStr,
I be right-ideal (non empty Subset of R);
func mult|(I,R) -> BinOp of I equals
(the mult of R)|[:I,I:];
coherence proof reconsider f = (the mult of R)|[:I,I:] as
Function of [:I,I:],the carrier of R by FUNCT_2:38;
A1: dom f = [:I,I:] by FUNCT_2:def 1;
for x being set st x in [:I,I:] holds f.x in I proof
let x be set; assume x in [:I,I:];
then consider u,v being set such that
A2: u in I & v in I & x = [u,v] by ZFMISC_1:def 2;
reconsider u,v as Element of I by A2;
f.x = (the mult of R).[u,v] by A1,A2,FUNCT_1:70
.= (the mult of R).(u,v) by BINOP_1:def 1
.= u*v by VECTSP_1:def 10;
hence thesis by Def3;
end;
hence thesis by A1,FUNCT_2:5;
end;
end;
definition
let R be non empty LoopStr,
I be add-closed (non empty Subset of R);
func Gr(I,R) -> non empty LoopStr equals :Def8:
LoopStr (#I,add|(I,R),In (0.R,I)#);
coherence;
end;
definition
let R be left_zeroed right_zeroed add-cancelable
add-associative distributive (non empty doubleLoopStr),
I be add-closed (non empty Subset of R);
cluster Gr(I,R) -> add-associative;
coherence proof set M = LoopStr (#I,add|(I,R),In (0.R,I)#);
A1: M = Gr(I,R) by Def8;
reconsider M as non empty LoopStr;
now let u be set;
assume A2: u in [:I,I:];
dom(the add of R) = [:the carrier of R,the carrier of R:] by FUNCT_2:def 1
;
hence u in dom(the add of R) by A2;
end;
then [:I,I:] c= dom(the add of R) by TARSKI:def 3;
then A3: dom((the add of R)|[:I,I:]) = [:I,I:] by RELAT_1:91;
A4: for a,b being Element of M, a',b' being Element of I
st a' = a & b' = b holds a + b = a' + b' proof
let a,b be Element of M, a',b' be Element of I;
assume a' = a & b' = b;
hence a + b = (add|(I,R)).[a',b'] by RLVECT_1:def 3
.= ((the add of R)|[:I,I:]).[a',b'] by Def6
.= (the add of R).[a',b'] by A3,FUNCT_1:70
.= a' + b' by RLVECT_1:def 3;
end;
now let a,b,c be Element of M;
reconsider a' = a, b' = b, c' = c as Element of I;
a' + b' in I by Def1;
then A5: [a'+b',c'] in dom((the add of R)|[:I,I:]) by A3,ZFMISC_1:def 2;
b' + c' in I by Def1;
then A6: [a',b'+c'] in dom((the add of R)|[:I,I:]) by A3,ZFMISC_1:def 2;
thus (a + b) + c = (the add of M).[a+b,c] by RLVECT_1:def 3
.= (add|(I,R)).[a'+b',c'] by A4
.= ((the add of R)|[:I,I:]).[a'+b',c'] by Def6
.= (the add of R).[a'+b',c'] by A5,FUNCT_1:70
.= (a'+b') + c' by RLVECT_1:def 3
.= a' + (b' + c') by RLVECT_1:def 6
.= (the add of R).[a',b'+c'] by RLVECT_1:def 3
.= ((the add of R)|[:I,I:]).[a',b'+c'] by A6,FUNCT_1:70
.= (add|(I,R)).[a',b'+c'] by Def6
.= (the add of M).[a,b+c] by A4
.= a + (b + c) by RLVECT_1:def 3;
end;
hence thesis by A1,RLVECT_1:def 6;
end;
end;
definition
let R be left_zeroed right_zeroed add-cancelable
add-associative distributive (non empty doubleLoopStr),
I be add-closed right-ideal (non empty Subset of R);
cluster Gr(I,R) -> right_zeroed;
coherence proof set M = LoopStr (#I,add|(I,R),In (0.R,I)#);
A1: M = Gr(I,R) by Def8;
reconsider M as non empty LoopStr;
now let u be set;
assume A2: u in [:I,I:];
dom(the add of R) = [:the carrier of R,the carrier of R:] by FUNCT_2:def 1
;
hence u in dom(the add of R) by A2;
end;
then [:I,I:] c= dom(the add of R) by TARSKI:def 3;
then A3: dom((the add of R)|[:I,I:]) = [:I,I:] by RELAT_1:91;
now let a be Element of M;
reconsider a' = a as Element of I;
A4: 0.R in I by Th3;
then A5: [a',0.R] in dom((the add of R)|[:I,I:]) by A3,ZFMISC_1:def 2;
thus a + 0.M = a + (the Zero of M) by RLVECT_1:def 2
.= (the add of M).[a,(In (0.R,I))] by RLVECT_1:def 3
.= (the add of M).[a,0.R] by A4,FUNCT_7:def 1
.= ((the add of R)|[:I,I:]).[a',0.R] by Def6
.= (the add of R).[a',0.R] by A5,FUNCT_1:70
.= a' + 0.R by RLVECT_1:def 3
.= a by RLVECT_1:def 7;
end;
hence thesis by A1,RLVECT_1:def 7;
end;
end;
definition
let R be Abelian (non empty doubleLoopStr),
I be add-closed (non empty Subset of R);
cluster Gr(I,R) -> Abelian;
coherence proof set M = LoopStr (#I,add|(I,R),In (0.R,I)#);
A1: M = Gr(I,R) by Def8;
reconsider M as non empty LoopStr;
now let u be set;
assume A2: u in [:I,I:];
dom(the add of R) = [:the carrier of R,the carrier of R:] by FUNCT_2:def 1
;
hence u in dom(the add of R) by A2;
end;
then [:I,I:] c= dom(the add of R) by TARSKI:def 3;
then A3: dom((the add of R)|[:I,I:]) = [:I,I:] by RELAT_1:91;
A4: for a,b being Element of M, a',b' being Element of I
st a' = a & b' = b holds a + b = a' + b' proof
let a,b be Element of M, a',b' be Element of I;
assume a' = a & b' = b;
hence a + b = (add|(I,R)).[a',b'] by RLVECT_1:def 3
.= ((the add of R)|[:I,I:]).[a',b'] by Def6
.= (the add of R).[a',b'] by A3,FUNCT_1:70
.= a' + b' by RLVECT_1:def 3;
end;
now let a,b be Element of M;
reconsider a' = a, b' = b as Element of I;
thus a + b = a' + b' by A4 .= b + a by A4;
end;
hence thesis by A1,RLVECT_1:def 5;
end;
end;
definition
let R be Abelian right_unital left_zeroed right_zeroed right_complementable
add-associative distributive (non empty doubleLoopStr),
I be add-closed right-ideal (non empty Subset of R);
cluster Gr(I,R) -> right_complementable;
coherence proof set M = LoopStr (#I,add|(I,R),In (0.R,I)#);
A1: M = Gr(I,R) by Def8;
reconsider M as non empty LoopStr;
now let u be set;
assume A2: u in [:I,I:];
dom(the add of R) = [:the carrier of R,the carrier of R:] by FUNCT_2:def 1
;
hence u in dom(the add of R) by A2;
end;
then [:I,I:] c= dom(the add of R) by TARSKI:def 3;
then A3: dom((the add of R)|[:I,I:]) = [:I,I:] by RELAT_1:91;
A4: for a,b being Element of M, a',b' being Element of I
st a' = a & b' = b holds a + b = a' + b' proof
let a,b be Element of M, a',b' be Element of I;
assume a' = a & b' = b;
hence a + b = (add|(I,R)).[a',b'] by RLVECT_1:def 3
.= ((the add of R)|[:I,I:]).[a',b'] by Def6
.= (the add of R).[a',b'] by A3,FUNCT_1:70
.= a' + b' by RLVECT_1:def 3;
end;
reconsider I as RightIdeal of R;
now let a be Element of M;
A5: 0.R in I by Th3;
reconsider a' = a as Element of I;
reconsider b = -a' as Element of M by Th14;
a + b = a' + -a' by A4 .= 0.R by RLVECT_1:16
.= the Zero of M by A5,FUNCT_7:def 1
.= 0.M by RLVECT_1:def 2;
hence ex b being Element of M st a + b = 0.M;
end;
hence thesis by A1,RLVECT_1:def 8;
end;
end;
Lm1:
for R being comRing, a being Element of R
holds {a*r where r is Element of R : not contradiction} is Ideal of R
proof let R be comRing, a be Element of R;
set M = {a*r where r is Element of R : not contradiction};
A1: now let u be set; assume u in M;
then consider r being Element of R such that A2: u = a*r;
thus u in the carrier of R by A2;
end; a*1_ R in M;
then reconsider M as non empty Subset of R by A1,TARSKI:def 3;
reconsider M as non empty Subset of R;
A3: now let b,c be Element of R; assume A4: b in M & c in M;
then consider r being Element of R such that A5: a*r = b;
consider s being Element of R such that A6: a*s = c by A4;
b + c = a*(r + s) by A5,A6,VECTSP_1:def 18;
hence b + c in M;
end;
A7: now let s,b be Element of R;
assume b in M;
then consider r being Element of R such that A8: a*r = b;
b*s = a*(r*s) by A8,VECTSP_1:def 16;
hence b*s in M;
end;
now let s,b be Element of R; assume b in M;
then consider r being Element of R such that A9: a*r = b;
s*b = (s*r)*a by A9,VECTSP_1:def 16;
hence s*b in M;
end;
hence thesis by A3,A7,Def1,Def2,Def3;
end;
theorem Th19:
for R being right_unital (non empty doubleLoopStr),
I being left-ideal (non empty Subset of R)
holds I is proper iff not(1_ R in I)
proof let R be right_unital (non empty doubleLoopStr),
I be left-ideal (non empty Subset of R);
A1: now assume A2: I is proper;
thus not(1_ R in I) proof
assume A3: 1_ R in I;
A4: for u being set holds u in I implies u in the carrier of R;
now let u be set; assume u in the carrier of R;
then reconsider u' = u as Element of R;
u'*1_ R = u' by VECTSP_1:def 13;
hence u in I by A3,Def2;
end;
then I = the carrier of R by A4,TARSKI:2;
hence thesis by A2,Def5;
end;
end;
now assume not(1_ R in I); then I <> the carrier of R;
hence I is proper by Def5;
end;
hence thesis by A1;
end;
theorem
for R being left_unital right_unital (non empty doubleLoopStr),
I being right-ideal (non empty Subset of R)
holds I is proper iff
for u being Element of R st u is unital holds not(u in I)
proof let R be left_unital right_unital (non empty doubleLoopStr),
I be right-ideal (non empty Subset of R);
A1: now assume A2: I is proper;
A3: not(1_ R in I) proof
assume A4: 1_ R in I;
A5: for u being set holds u in I implies u in the carrier of R;
now let u be set; assume u in the carrier of R;
then reconsider u' = u as Element of R;
1_ R*u' = u' by VECTSP_1:def 19;
hence u in I by A4,Def3;
end;
then I = the carrier of R by A5,TARSKI:2;
hence thesis by A2,Def5;
end;
thus for u being Element of R st u is unital holds not(u in I) proof
let u be Element of R; assume u is unital;
then u divides 1_ R by GCD_1:def 2;
then ex b being Element of R st 1_ R = u*b by GCD_1:def 1;
hence thesis by A3,Def3;
end;
end;
now assume A6: for u being Element of R st u is unital holds not(u in I);
1_ R divides 1_ R; then 1_ R is unital by GCD_1:def 2;
then I <> the carrier of R by A6;
hence I is proper by Def5;
end;
hence thesis by A1;
end;
theorem
for R being right_unital (non empty doubleLoopStr),
I being left-ideal right-ideal (non empty Subset of R)
holds I is proper iff for u being Element of R st u is unital holds not(u in
I)
proof let R be right_unital (non empty doubleLoopStr),
I be left-ideal right-ideal (non empty Subset of R);
A1: now assume A2: I is proper;
A3: not(1_ R in I) proof assume A4: 1_ R in I;
A5: for u being set holds u in I implies u in the carrier of R;
now let u be set; assume u in the carrier of R;
then reconsider u' = u as Element of R;
u'*1_ R = u' by VECTSP_1:def 13;
hence u in I by A4,Def2;
end; then I = the carrier of R by A5,TARSKI:2;
hence thesis by A2,Def5;
end;
thus for u being Element of R st u is unital holds not(u in I) proof
let u be Element of R; assume u is unital;
then u divides 1_ R by GCD_1:def 2;
then ex b being Element of R st 1_ R = u*b by GCD_1:def 1;
hence thesis by A3,Def3;
end;
end;
now assume A6: for u being Element of R st u is unital holds not(u in I);
1_ R*1_ R = 1_ R by VECTSP_1:def 13;
then 1_ R divides 1_ R by GCD_1:def 1;
then 1_ R is unital by GCD_1:def 2; then I <> the carrier of R by A6;
hence I is proper by Def5;
end;
hence thesis by A1;
end;
theorem
for R being non degenerated comRing
holds R is Field iff
for I being Ideal of R holds (I = {0.R} or I = the carrier of R)
proof let R be non degenerated comRing;
A1: now assume A2: R is Field;
thus
for I being Ideal of R holds (I = {0.R} or I = the carrier of R) proof
let I be Ideal of R; assume A3: I <> {0.R};
reconsider R as Field by A2;
ex a being Element of R st a in I & a <> 0.R proof
assume A4:
not(ex a being Element of R st a in I & a <> 0.R);
A5: now let u be set; assume u in I;
then reconsider u' = u as Element of I; u' = 0.R by A4;
hence u in {0.R} by TARSKI:def 1;
end;
now let u be set; assume A6: u in {0.R};
then reconsider u' = u as Element of R;
u' = 0.R by A6,TARSKI:def 1;
hence u in I by Th3;
end;
hence thesis by A3,A5,TARSKI:2;
end;
then consider a being Element of R such that
A7: a in I & a <> 0.R;
consider b being Element of R such that
A8: a*b = 1_ R by A7,VECTSP_1:def 20;
1_ R in I by A7,A8,Def3; then I is non proper by Th19;
hence thesis by Def5;
end;
end;
now assume A9: for I being Ideal of R holds (I= {0.R} or I = the carrier of R
)
;
now let a be Element of R;
assume A10: a <> 0.R;
reconsider a' = a as Element of R;
reconsider M = {a'*r where r is Element of R : not contradiction}
as Ideal of R by Lm1; a*1_ R = a by VECTSP_1:def 19;
then a in M; then M <> {0.R} by A10,TARSKI:def 1;
then M = the carrier of R by A9; then 1_ R in M;
then consider b being Element of R such that
A11: a*b = 1_ R;
thus ex b being Element of R st a*b = 1_ R by A11;
end;
hence R is Field by VECTSP_1:def 20;
end;
hence thesis by A1;
end;
begin :: Linear combinations
definition
let R be non empty multLoopStr,
A be non empty Subset of R;
mode LinearCombination of A -> FinSequence of the carrier of R
means :Def9:
for i being set st i in dom it
ex u,v being Element of R, a being Element of A st it/.i = u*a*v;
existence proof set p = <*>(the carrier of R);
take p; let i be set; assume i in dom p; hence thesis;
end;
mode LeftLinearCombination of A -> FinSequence of the carrier of R
means :Def10:
for i being set st i in dom it
ex u being Element of R, a being Element of A st it/.i = u*a;
existence proof consider a being Element of A;
reconsider aR = a as Element of R;
reconsider a' = a*a as Element of R; set p = <*a'*>;
take p; let i be set; assume
A1: i in dom p;
dom p = {1} by FINSEQ_1:4,55;
then A2: i = 1 by A1,TARSKI:def 1;
take aR, a;
thus p/.i = p.i by A1,FINSEQ_4:def 4 .= aR*a by A2,FINSEQ_1:57;
end;
mode RightLinearCombination of A -> FinSequence of the carrier of R
means :Def11:
for i being set st i in dom it
ex u being Element of R, a being Element of A st it/.i = a*u;
existence proof consider a being Element of A;
reconsider aR = a as Element of R;
reconsider a' = a*a as Element of R; set p = <*a'*>;
take p; let i be set; assume
A3: i in dom p;
dom p = {1} by FINSEQ_1:4,55;
then A4: i = 1 by A3,TARSKI:def 1;
take aR, a;
thus p/.i = p.i by A3,FINSEQ_4:def 4 .= a*aR by A4,FINSEQ_1:57;
end;
end;
definition
let R be non empty multLoopStr,
A be non empty Subset of R;
cluster non empty LinearCombination of A;
existence proof consider u, v being Element of R;
consider a being Element of A;
reconsider p = <*u*a*v*> as FinSequence of the carrier of R;
take p;
now let i be set; assume i in dom p; then i in {1} by FINSEQ_1:4,55
;
then A1: i = 1 by TARSKI:def 1;
take u,v, a; thus p/.i = u*a*v by A1,FINSEQ_4:25;
end; hence thesis by Def9;
end;
cluster non empty LeftLinearCombination of A;
existence proof consider u being Element of R;
consider a being Element of A;
reconsider p = <*u*a*> as FinSequence of the carrier of R;
take p;
now let i be set; assume i in dom p; then i in {1} by FINSEQ_1:4,55
;
then A2: i = 1 by TARSKI:def 1;
take u, a; thus p/.i = u*a by A2,FINSEQ_4:25;
end; hence thesis by Def10;
end;
cluster non empty RightLinearCombination of A;
existence proof consider v being Element of R;
consider a being Element of A;
reconsider p = <*a*v*> as FinSequence of the carrier of R;
take p;
now let i be set; assume i in dom p; then i in {1} by FINSEQ_1:4,55
;
then A3: i = 1 by TARSKI:def 1;
take v, a; thus p/.i = a*v by A3,FINSEQ_4:25;
end; hence thesis by Def11;
end;
end;
definition
let R be non empty multLoopStr,
A,B be non empty Subset of R,
F be LinearCombination of A,
G be LinearCombination of B;
redefine func F^G -> LinearCombination of (A \/ B);
coherence proof
set H = F^G;
thus H is LinearCombination of (A \/ B) proof
let i be set; assume
A1: i in dom H;
then A2: H/.i = H.i by FINSEQ_4:def 4;
per cases; suppose
A3: i in dom F;
then A4: F/.i = F.i by FINSEQ_4:def 4;
consider u,v being Element of R, a being Element of A such that
A5: F/.i = u*a*v by A3,Def9;
A6: F.i = H.i by A3,FINSEQ_1:def 7;
a in A \/ B by XBOOLE_0:def 2;
hence thesis by A2,A4,A5,A6;
suppose not i in dom F;
then consider n being Nat such that
A7: n in dom G & i=len F + n by A1,FINSEQ_1:38;
consider u,v being Element of R, b being Element of B such that
A8: G/.n = u*b*v by A7,Def9;
A9: G/.n = G.n by A7,FINSEQ_4:def 4;
A10: G.n = H.i by A7,FINSEQ_1:def 7;
b in A \/ B by XBOOLE_0:def 2;
hence thesis by A2,A8,A9,A10;
end;
end;
end;
theorem Th23:
for R be associative (non empty multLoopStr),
A be non empty Subset of R,
a be Element of R, F be LinearCombination of A
holds a*F is LinearCombination of A
proof let R be associative (non empty multLoopStr),
A be non empty Subset of R,
a be Element of R, F be LinearCombination of A;
let i be set; assume i in dom (a*F);
then A1: i in dom F by POLYNOM1:def 2;
then consider u, v being Element of R, b being Element of A such that
A2: F/.i = u*b*v by Def9;
take x = a*u, v, b;
thus (a*F)/.i = a*F/.i by A1,POLYNOM1:def 2
.= a*(u*b)*v by A2,VECTSP_1:def 16 .= x*b*v by VECTSP_1:def 16;
end;
theorem Th24:
for R be associative (non empty multLoopStr),
A be non empty Subset of R,
a be Element of R, F be LinearCombination of A
holds F*a is LinearCombination of A
proof let R be associative (non empty multLoopStr),
A be non empty Subset of R,
a be Element of R, F be LinearCombination of A;
let i be set; assume i in dom (F*a);
then A1: i in dom F by POLYNOM1:def 3;
then consider u, v being Element of R, b being Element of A such that
A2: F/.i = u*b*v by Def9;
take u, x = v*a, b;
thus (F*a)/.i = (F/.i)*a by A1,POLYNOM1:def 3
.= u*(b*v)*a by A2,VECTSP_1:def 16 .= u*(b*v*a) by VECTSP_1:def 16
.= u*(b*(v*a)) by VECTSP_1:def 16 .= u*b*x by VECTSP_1:def 16;
end;
theorem Th25:
for R being right_unital (non empty multLoopStr),
A being non empty Subset of R,
f being LeftLinearCombination of A
holds f is LinearCombination of A
proof let R be right_unital (non empty multLoopStr),
A be non empty Subset of R, f be LeftLinearCombination of A;
let i be set; assume i in dom f;
then consider r being Element of R, a being Element of A such that
A1: f/.i = r*a by Def10;
f/.i = r*a*1_ R by A1,VECTSP_1:def 13;
hence thesis;
end;
definition
let R be non empty multLoopStr,
A,B be non empty Subset of R,
F be LeftLinearCombination of A,
G be LeftLinearCombination of B;
redefine func F^G -> LeftLinearCombination of (A \/ B);
coherence proof set H = F^G;
thus H is LeftLinearCombination of (A \/ B) proof
let i be set; assume
A1: i in dom H;
then A2: H/.i = H.i by FINSEQ_4:def 4;
per cases; suppose
A3: i in dom F;
then A4: F/.i = F.i by FINSEQ_4:def 4;
consider u being Element of R, a being Element of A such that
A5: F/.i = u*a by A3,Def10;
A6: F.i = H.i by A3,FINSEQ_1:def 7;
a in A \/ B by XBOOLE_0:def 2;
hence thesis by A2,A4,A5,A6;
suppose not i in dom F;
then consider n being Nat such that
A7: n in dom G & i=len F + n by A1,FINSEQ_1:38;
consider u being Element of R, b being Element of B such that
A8: G/.n = u*b by A7,Def10;
A9: G/.n = G.n by A7,FINSEQ_4:def 4;
A10: G.n = H.i by A7,FINSEQ_1:def 7;
b in A \/ B by XBOOLE_0:def 2;
hence thesis by A2,A8,A9,A10;
end;
end;
end;
theorem Th26:
for R be associative (non empty multLoopStr),
A be non empty Subset of R,
a be Element of R,
F be LeftLinearCombination of A
holds a*F is LeftLinearCombination of A
proof let R be associative (non empty multLoopStr),
A be non empty Subset of R,
a be Element of R,
F be LeftLinearCombination of A;
let i be set; assume i in dom (a*F);
then A1: i in dom F by POLYNOM1:def 2;
then consider u being Element of R, b being Element of A such that
A2: F/.i = u*b by Def10;
take x = a*u, b;
thus (a*F)/.i = a*F/.i by A1,POLYNOM1:def 2
.= x*b by A2,VECTSP_1:def 16;
end;
theorem
for R be non empty multLoopStr,
A be non empty Subset of R,
a be Element of R,
F be LeftLinearCombination of A
holds F*a is LinearCombination of A
proof let R be non empty multLoopStr,
A be non empty Subset of R,
a be Element of R,
F be LeftLinearCombination of A;
let i be set; assume i in dom (F*a);
then A1: i in dom F by POLYNOM1:def 3;
then consider u being Element of R, b being Element of A such that
A2: F/.i = u*b by Def10;
reconsider c = a as Element of R;
take u, c, b;
thus (F*a)/.i = u*b*c by A1,A2,POLYNOM1:def 3;
end;
theorem Th28:
for R being left_unital (non empty multLoopStr),
A being non empty Subset of R,
f being RightLinearCombination of A
holds f is LinearCombination of A
proof
let R be left_unital (non empty multLoopStr),
A be non empty Subset of R,
f be RightLinearCombination of A;
let i be set;
assume i in dom f;
then consider r being Element of R, a being Element of A such that
A1: f/.i = a*r by Def11;
f/.i = 1_ R*a*r by A1,VECTSP_1:def 19;
hence thesis;
end;
definition
let R be non empty multLoopStr,
A,B be non empty Subset of R,
F be RightLinearCombination of A,
G be RightLinearCombination of B;
redefine func F^G -> RightLinearCombination of (A \/ B);
coherence proof set H = F^G;
thus H is RightLinearCombination of (A \/ B) proof
let i be set; assume
A1: i in dom H;
then A2: H/.i = H.i by FINSEQ_4:def 4;
per cases; suppose
A3: i in dom F;
then A4: F/.i = F.i by FINSEQ_4:def 4;
consider u being Element of R, a being Element of A such that
A5: F/.i = a*u by A3,Def11;
A6: F.i = H.i by A3,FINSEQ_1:def 7;
a in A \/ B by XBOOLE_0:def 2;
hence thesis by A2,A4,A5,A6;
suppose not i in dom F;
then consider n being Nat such that
A7: n in dom G & i=len F + n by A1,FINSEQ_1:38;
consider u being Element of R, b being Element of B such that
A8: G/.n = b*u by A7,Def11;
A9: G/.n = G.n by A7,FINSEQ_4:def 4;
A10: G.n = H.i by A7,FINSEQ_1:def 7;
b in A \/ B by XBOOLE_0:def 2;
hence thesis by A2,A8,A9,A10;
end;
end;
end;
theorem Th29:
for R be associative (non empty multLoopStr),
A be non empty Subset of R,
a be Element of R,
F be RightLinearCombination of A
holds F*a is RightLinearCombination of A
proof let R be associative (non empty multLoopStr),
A be non empty Subset of R,
a be Element of R, F be RightLinearCombination of A;
let i be set; assume i in dom (F*a);
then A1: i in dom F by POLYNOM1:def 3;
then consider u being Element of R, b being Element of A such that
A2: F/.i = b*u by Def11;
take x = u*a, b;
thus (F*a)/.i=(F/.i)*a by A1,POLYNOM1:def 3.= b*x by A2,VECTSP_1:def 16;
end;
theorem
for R be associative (non empty multLoopStr),
A be non empty Subset of R,
a be Element of R,
F be RightLinearCombination of A
holds a*F is LinearCombination of A
proof let R be associative (non empty multLoopStr),
A be non empty Subset of R,
a be Element of R, F be RightLinearCombination of A;
let i be set; assume i in dom (a*F);
then A1: i in dom F by POLYNOM1:def 2;
then consider u being Element of R, b being Element of A such that
A2: F/.i = b*u by Def11;
reconsider c = a as Element of R;
take c, u, b;
thus (a*F)/.i=a*(F/.i) by A1,POLYNOM1:def 2.= c*b*u by A2,VECTSP_1:def 16;
end;
theorem Th31:
for R being commutative associative (non empty multLoopStr),
A being non empty Subset of R,
f being LinearCombination of A
holds f is LeftLinearCombination of A & f is RightLinearCombination of A
proof let R being commutative associative (non empty multLoopStr),
A being non empty Subset of R,
f being LinearCombination of A;
hereby let i be set;
assume i in dom f;
then consider r,s being Element of R, a being Element of A such that
A1: f/.i = r*a*s by Def9;
f/.i = (r*s)*a by A1,VECTSP_1:def 16;
hence ex r being Element of R, a being Element of A st f/.i = r*a;
end;
let i be set; assume i in dom f;
then consider r,s being Element of R, a being Element of A such that
A2: f/.i = r*a*s by Def9;
f/.i = a*(r*s) by A2,VECTSP_1:def 16;
hence ex r being Element of R, a being Element of A st f/.i = a*r;
end;
theorem Th32:
for S being non empty doubleLoopStr,
F being non empty Subset of S,
lc being non empty LinearCombination of F
ex p being LinearCombination of F,
e being Element of S
st lc = p^<* e *> & <*e*> is LinearCombination of F
proof let S be non empty doubleLoopStr,
F be non empty Subset of S,
lc be non empty LinearCombination of F;
len lc <> 0 by FINSEQ_1:25;
then consider p being FinSequence of the carrier of S,
e being Element of S such that
A1: lc = p^<*e*> by FINSEQ_2:22;
now let i be set; assume
A2: i in dom p;
A3: dom p c= dom lc by A1,FINSEQ_1:39;
then consider u, v being Element of S, a being Element of F such that
A4: lc/.i = u*a*v by A2,Def9;
take u, v, a;
thus p/.i = p.i by A2,FINSEQ_4:def 4 .= lc.i by A1,A2,FINSEQ_1:def 7
.= u*a*v by A2,A3,A4,FINSEQ_4:def 4;
end;
then reconsider p as LinearCombination of F by Def9;
take p; take e; thus lc = p^<* e *> by A1;
A5: len lc = len p +1 by A1,FINSEQ_2:19;
A6: len lc in dom lc by FINSEQ_5:6;
then consider u, v being Element of S, a being Element of F such that
A7: lc/.(len lc) = u*a*v by Def9;
A8: lc/.(len lc) = lc.(len lc) by A6,FINSEQ_4:def 4;
let i be set such that
A9: i in dom <*e*>;
dom <*e*> = {1} by FINSEQ_1:4,55;
then A10: i = 1 by A9,TARSKI:def 1;
take u, v, a;
thus <*e*>/.i = <*e*>.i by A9,FINSEQ_4:def 4 .= e by A10,FINSEQ_1:57
.= u*a*v by A1,A5,A7,A8,JORDAN3:16;
end;
theorem Th33:
for S being non empty doubleLoopStr,
F being non empty Subset of S,
lc being non empty LeftLinearCombination of F
ex p being LeftLinearCombination of F,
e being Element of S
st lc = p^<* e *> & <*e*> is LeftLinearCombination of F
proof let S be non empty doubleLoopStr,
F be non empty Subset of S,
lc be non empty LeftLinearCombination of F;
len lc <> 0 by FINSEQ_1:25;
then consider p being FinSequence of the carrier of S,
e being Element of S such that
A1: lc = p^<*e*> by FINSEQ_2:22;
now let i be set; assume
A2: i in dom p;
A3: dom p c= dom lc by A1,FINSEQ_1:39;
then consider u being Element of S, a being Element of F such that
A4: lc/.i = u*a by A2,Def10;
take u, a;
thus p/.i = p.i by A2,FINSEQ_4:def 4 .= lc.i by A1,A2,FINSEQ_1:def 7
.= u*a by A2,A3,A4,FINSEQ_4:def 4;
end;
then reconsider p as LeftLinearCombination of F by Def10;
take p; take e; thus lc = p^<* e *> by A1;
A5: len lc = len p +1 by A1,FINSEQ_2:19;
A6: len lc in dom lc by FINSEQ_5:6;
then consider u being Element of S, a being Element of F such that
A7: lc/.(len lc) = u*a by Def10;
A8: lc/.(len lc) = lc.(len lc) by A6,FINSEQ_4:def 4;
let i be set such that
A9: i in dom <*e*>;
dom <*e*> = {1} by FINSEQ_1:4,55;
then A10: i = 1 by A9,TARSKI:def 1;
take u, a;
thus <*e*>/.i = <*e*>.i by A9,FINSEQ_4:def 4 .= e by A10,FINSEQ_1:57
.= u*a by A1,A5,A7,A8,JORDAN3:16;
end;
theorem Th34:
for S being non empty doubleLoopStr,
F being non empty Subset of S,
lc being non empty RightLinearCombination of F
ex p being RightLinearCombination of F,
e being Element of S
st lc = p^<* e *> & <*e*> is RightLinearCombination of F
proof let S be non empty doubleLoopStr,
F be non empty Subset of S,
lc be non empty RightLinearCombination of F;
len lc <> 0 by FINSEQ_1:25;
then consider p being FinSequence of the carrier of S,
e being Element of S such that
A1: lc = p^<*e*> by FINSEQ_2:22;
now let i be set; assume
A2: i in dom p;
A3: dom p c= dom lc by A1,FINSEQ_1:39;
then consider u being Element of S, a being Element of F such that
A4: lc/.i = a*u by A2,Def11;
take u, a;
thus p/.i = p.i by A2,FINSEQ_4:def 4 .= lc.i by A1,A2,FINSEQ_1:def 7
.= a*u by A2,A3,A4,FINSEQ_4:def 4;
end;
then reconsider p as RightLinearCombination of F by Def11;
take p; take e;
thus lc = p^<* e *> by A1;
A5: len lc = len p +1 by A1,FINSEQ_2:19;
A6: len lc in dom lc by FINSEQ_5:6;
then consider u being Element of S, a being Element of F such that
A7: lc/.(len lc) = a*u by Def11;
A8: lc/.(len lc) = lc.(len lc) by A6,FINSEQ_4:def 4;
let i be set such that
A9: i in dom <*e*>;
dom <*e*> = {1} by FINSEQ_1:4,55;
then A10: i = 1 by A9,TARSKI:def 1;
take u, a;
thus <*e*>/.i = <*e*>.i by A9,FINSEQ_4:def 4 .= e by A10,FINSEQ_1:57
.= a*u by A1,A5,A7,A8,JORDAN3:16;
end;
definition
let R be non empty multLoopStr, A be non empty Subset of R,
L be LinearCombination of A,
E be FinSequence of
[:the carrier of R, the carrier of R, the carrier of R:];
pred E represents L means :Def12
:
len E = len L &
for i being set st i in dom L
holds L.i = ((E/.i)`1)*((E/.i)`2)*((E/.i)`3) & ((E/.i)`2) in A;
end;
theorem
for R being non empty multLoopStr,
A being non empty Subset of R,
L be LinearCombination of A
ex E be FinSequence of
[:the carrier of R, the carrier of R, the carrier of R:]
st E represents L
proof let R be non empty multLoopStr,A be non empty Subset of R,
L be LinearCombination of A;
set D = [:the carrier of R, the carrier of R, the carrier of R:];
defpred P[set,set] means
ex x, y, z being Element of R
st $2 = [x, y, z] & y in A & L/.$1 = x*y*z;
A1: now let k be Nat; assume k in Seg len L; then k in dom L by FINSEQ_1:def 3;
then consider u,v being Element of R, a being Element of A such that
A2: L/.k = u*a*v by Def9;
reconsider b = a as Element of R;
reconsider d = [u, b, v] as Element of D;
take d; thus P[k, d] by A2;
end;
consider E being FinSequence of D such that
A3: dom E = Seg len L and
A4: for k be Nat st k in Seg len L holds P[k,E/.k] from SeqExD(A1);
take E;
A5: dom L = Seg len L by FINSEQ_1:def 3;
thus len E = len L by A3,FINSEQ_1:def 3;
let i being set such that
A6: i in dom L;
reconsider k = i as Nat by A6;
consider x, y, z being Element of R such that
A7: E/.k = [x, y, z] & y in A & L/.k = x*y*z by A4,A5,A6;
[x,y,z]`1 = x & [x,y,z]`2 = y & [x,y,z]`3 = z by MCART_1:def 5,def 6,def 7;
hence L.i = ((E/.i)`1)*((E/.i)`2)*((E/.i)`3) by A6,A7,FINSEQ_4:def 4;
thus ((E/.i)`2) in A by A7,MCART_1:def 6;
end;
theorem
for R, S being non empty multLoopStr,
F being non empty Subset of R,
lc being LinearCombination of F,
G being non empty Subset of S,
P being Function of the carrier of R, the carrier of S,
E being FinSequence of
[:the carrier of R, the carrier of R, the carrier of R:]
st P.:F c= G & E represents lc
holds ex LC being LinearCombination of G st len lc = len LC &
for i being set st i in dom LC
holds LC.i = (P.(E/.i)`1)*(P.(E/.i)`2)*(P.(E/.i)`3)
proof let R, S be non empty multLoopStr,
F be non empty Subset of R,
lc be LinearCombination of F,
G be non empty Subset of S,
P be Function of the carrier of R, the carrier of S,
E being FinSequence of
[:the carrier of R, the carrier of R, the carrier of R:]; assume
A1: P.:F c= G; assume
A2: E represents lc;
deffunc F(Nat)=(P.(E/.$1)`1)*(P.(E/.$1)`2)*(P.(E/.$1)`3);
consider LC being FinSequence of the carrier of S such that
A3: len LC = len lc and
A4: for k being Nat st k in Seg len lc
holds LC.k = F(k) from SeqLambdaD;
now let i be set such that
A5: i in dom LC;
A6: dom LC = Seg len lc by A3,FINSEQ_1:def 3;
reconsider u = P.(E/.i)`1, v = P.(E/.i)`3 as Element of S;
A7: dom P = the carrier of R by FUNCT_2:def 1;
dom lc = dom LC by A3,FINSEQ_3:31; then (E/.i)`2 in F by A2,A5,Def12
;
then P.((E/.i)`2) in P.:F by A7,FUNCT_1:def 12;
then reconsider a = P.(E/.i)`2 as Element of G by A1;
take u, v, a; LC.i = LC/.i by A5,FINSEQ_4:def 4;
hence LC/.i = u*a*v by A4,A5,A6;
end; then reconsider LC as LinearCombination of G by Def9;
take LC; thus len lc = len LC by A3;
let i be set such that A8: i in dom LC;
dom LC = Seg len lc by A3,FINSEQ_1:def 3;
hence thesis by A4,A8;
end;
definition
let R be non empty multLoopStr, A be non empty Subset of R,
L be LeftLinearCombination of A,
E be FinSequence of [:the carrier of R, the carrier of R:];
pred E represents L means :Def13:
len E = len L &
for i being set st i in dom L
holds L.i = ((E/.i)`1)*((E/.i)`2) & ((E/.i)`2) in A;
end;
theorem
for R being non empty multLoopStr,
A being non empty Subset of R,
L be LeftLinearCombination of A
ex E be FinSequence of [:the carrier of R, the carrier of R:]
st E represents L
proof let R be non empty multLoopStr,A be non empty Subset of R,
L be LeftLinearCombination of A;
set D = [:the carrier of R, the carrier of R:];
defpred P[set,set] means
ex x, y being Element of R
st $2 = [x, y] & y in A & L/.$1 = x*y;
A1: now let k be Nat; assume k in Seg len L; then k in dom L by FINSEQ_1:def 3;
then consider u being Element of R, a being Element of A such that
A2: L/.k = u*a by Def10;
reconsider b = a as Element of R;
reconsider d = [u, b] as Element of D;
take d; thus P[k, d] by A2;
end;
consider E being FinSequence of D such that
A3: dom E = Seg len L and
A4: for k be Nat st k in Seg len L holds P[k,E/.k] from SeqExD(A1);
take E;
A5: dom L = Seg len L by FINSEQ_1:def 3;
thus len E = len L by A3,FINSEQ_1:def 3;
let i being set such that
A6: i in dom L;
reconsider k = i as Nat by A6;
consider x, y being Element of R such that
A7: E/.k = [x, y] & y in A & L/.k = x*y by A4,A5,A6;
[x,y]`1 = x & [x,y]`2 = y by MCART_1:def 1,def 2;
hence L.i = ((E/.i)`1)*((E/.i)`2) by A6,A7,FINSEQ_4:def 4;
thus ((E/.i)`2) in A by A7,MCART_1:def 2;
end;
theorem
for R, S being non empty multLoopStr,
F being non empty Subset of R,
lc being LeftLinearCombination of F,
G being non empty Subset of S,
P being Function of the carrier of R, the carrier of S,
E being FinSequence of [:the carrier of R, the carrier of R:]
st P.:F c= G & E represents lc
holds ex LC being LeftLinearCombination of G st len lc = len LC &
for i being set st i in dom LC
holds LC.i = (P.(E/.i)`1)*(P.(E/.i)`2)
proof let R, S be non empty multLoopStr,
F be non empty Subset of R,
lc be LeftLinearCombination of F,
G be non empty Subset of S,
P be Function of the carrier of R, the carrier of S,
E being FinSequence of [:the carrier of R, the carrier of R:]; assume
A1: P.:F c= G; assume
A2: E represents lc;
deffunc F(Nat)=(P.(E/.$1)`1)*(P.(E/.$1)`2);
consider LC being FinSequence of the carrier of S such that
A3: len LC = len lc and
A4: for k being Nat st k in Seg len lc
holds LC.k = F(k) from SeqLambdaD;
now let i be set such that
A5: i in dom LC;
A6: dom LC = Seg len lc by A3,FINSEQ_1:def 3;
reconsider u = P.(E/.i)`1 as Element of S;
A7: dom P = the carrier of R by FUNCT_2:def 1;
dom lc = dom LC by A3,FINSEQ_3:31; then (E/.i)`2 in F by A2,A5,Def13
;
then P.((E/.i)`2) in P.:F by A7,FUNCT_1:def 12;
then reconsider a = P.(E/.i)`2 as Element of G by A1;
take u, a; LC.i = LC/.i by A5,FINSEQ_4:def 4;
hence LC/.i = u*a by A4,A5,A6;
end; then reconsider LC as LeftLinearCombination of G by Def10;
take LC; thus len lc = len LC by A3;
let i be set such that A8: i in dom LC;
dom LC = Seg len lc by A3,FINSEQ_1:def 3;
hence thesis by A4,A8;
end;
definition
let R be non empty multLoopStr, A be non empty Subset of R,
L be RightLinearCombination of A,
E be FinSequence of [:the carrier of R, the carrier of R:];
pred E represents L means :Def14:
len E = len L &
for i being set st i in dom L
holds L.i = ((E/.i)`1)*((E/.i)`2) & ((E/.i)`1) in A;
end;
theorem
for R being non empty multLoopStr,
A being non empty Subset of R,
L be RightLinearCombination of A
ex E be FinSequence of [:the carrier of R, the carrier of R:]
st E represents L
proof let R be non empty multLoopStr,A be non empty Subset of R,
L be RightLinearCombination of A;
set D = [:the carrier of R, the carrier of R:];
defpred P[set,set] means
ex x, y being Element of R
st $2 = [x, y] & x in A & L/.$1 = x*y;
A1: now let k be Nat; assume k in Seg len L; then k in dom L by FINSEQ_1:def 3;
then consider v being Element of R, a being Element of A such that
A2: L/.k = a*v by Def11;
reconsider b = a as Element of R;
reconsider d = [b, v] as Element of D;
take d; thus P[k, d] by A2;
end;
consider E being FinSequence of D such that
A3: dom E = Seg len L and
A4: for k be Nat st k in Seg len L holds P[k,E/.k] from SeqExD(A1);
take E;
A5: dom L = Seg len L by FINSEQ_1:def 3;
thus len E = len L by A3,FINSEQ_1:def 3;
let i being set such that
A6: i in dom L;
reconsider k = i as Nat by A6;
consider x, y being Element of R such that
A7: E/.k = [x, y] & x in A & L/.k = x*y by A4,A5,A6;
[x,y]`1 = x & [x,y]`2 = y by MCART_1:def 1,def 2;
hence L.i = ((E/.i)`1)*((E/.i)`2) by A6,A7,FINSEQ_4:def 4;
thus ((E/.i)`1) in A by A7,MCART_1:def 1;
end;
theorem
for R, S being non empty multLoopStr,
F being non empty Subset of R,
lc being RightLinearCombination of F,
G being non empty Subset of S,
P being Function of the carrier of R, the carrier of S,
E being FinSequence of [:the carrier of R, the carrier of R:]
st P.:F c= G & E represents lc
holds ex LC being RightLinearCombination of G st len lc = len LC &
for i being set st i in dom LC
holds LC.i = (P.(E/.i)`1)*(P.(E/.i)`2)
proof let R, S be non empty multLoopStr,
F be non empty Subset of R,
lc be RightLinearCombination of F,
G be non empty Subset of S,
P be Function of the carrier of R, the carrier of S,
E being FinSequence of [:the carrier of R, the carrier of R:]; assume
A1: P.:F c= G; assume
A2: E represents lc;
deffunc F(Nat)=(P.(E/.$1)`1)*(P.(E/.$1)`2);
consider LC being FinSequence of the carrier of S such that
A3: len LC = len lc and
A4: for k being Nat st k in Seg len lc
holds LC.k = F(k) from SeqLambdaD;
now let i be set such that
A5: i in dom LC;
A6: dom LC = Seg len lc by A3,FINSEQ_1:def 3;
reconsider v = P.(E/.i)`2 as Element of S;
A7: dom P = the carrier of R by FUNCT_2:def 1;
dom lc = dom LC by A3,FINSEQ_3:31; then (E/.i)`1 in F by A2,A5,Def14
;
then P.((E/.i)`1) in P.:F by A7,FUNCT_1:def 12;
then reconsider a = P.(E/.i)`1 as Element of G by A1;
take v, a; LC.i = LC/.i by A5,FINSEQ_4:def 4;
hence LC/.i = a*v by A4,A5,A6;
end; then reconsider LC as RightLinearCombination of G by Def11;
take LC; thus len lc = len LC by A3;
let i be set such that A8: i in dom LC;
dom LC = Seg len lc by A3,FINSEQ_1:def 3;
hence thesis by A4,A8;
end;
theorem
for R being non empty multLoopStr,
A being non empty Subset of R,
l being LinearCombination of A, n being Nat
holds l|Seg n is LinearCombination of A
proof let R be non empty multLoopStr,
A be non empty Subset of R,
l be LinearCombination of A, n being Nat;
reconsider ln = l|Seg n as FinSequence of the carrier of R by FINSEQ_1:23;
now let i being set such that
A1: i in dom ln;
A2: dom ln c= dom l by RELAT_1:89;
then consider u,v being Element of R, a being Element of A such that
A3: l/.i = u*a*v by A1,Def9;
take u, v, a;
thus ln/.i = ln.i by A1,FINSEQ_4:def 4 .= l.i by A1,FUNCT_1:70
.= u*a*v by A1,A2,A3,FINSEQ_4:def 4;
end;
hence l|Seg n is LinearCombination of A by Def9;
end;
theorem
for R being non empty multLoopStr,
A being non empty Subset of R,
l being LeftLinearCombination of A, n being Nat
holds l|Seg n is LeftLinearCombination of A
proof let R be non empty multLoopStr,
A be non empty Subset of R,
l be LeftLinearCombination of A, n being Nat;
reconsider ln = l|Seg n as FinSequence of the carrier of R by FINSEQ_1:23;
now let i being set such that
A1: i in dom ln;
A2: dom ln c= dom l by RELAT_1:89;
then consider u being Element of R, a being Element of A such that
A3: l/.i = u*a by A1,Def10;
take u, a;
thus ln/.i = ln.i by A1,FINSEQ_4:def 4 .= l.i by A1,FUNCT_1:70
.= u*a by A1,A2,A3,FINSEQ_4:def 4;
end;
hence l|Seg n is LeftLinearCombination of A by Def10;
end;
theorem
for R being non empty multLoopStr,
A being non empty Subset of R,
l being RightLinearCombination of A, n being Nat
holds l|Seg n is RightLinearCombination of A
proof let R be non empty multLoopStr,
A be non empty Subset of R,
l be RightLinearCombination of A, n being Nat;
reconsider ln = l|Seg n as FinSequence of the carrier of R by FINSEQ_1:23;
now let i being set such that
A1: i in dom ln;
A2: dom ln c= dom l by RELAT_1:89;
then consider v being Element of R, a being Element of A such that
A3: l/.i = a*v by A1,Def11;
take v, a;
thus ln/.i = ln.i by A1,FINSEQ_4:def 4 .= l.i by A1,FUNCT_1:70
.= a*v by A1,A2,A3,FINSEQ_4:def 4;
end;
hence l|Seg n is RightLinearCombination of A by Def11;
end;
begin :: Generated ideals
definition
let L be non empty doubleLoopStr,
F be Subset of L;
assume A1: F is non empty;
func F-Ideal -> Ideal of L means :Def15:
F c= it & for I being Ideal of L st F c= I holds it c= I;
existence proof
set Id = { I where I is Element of bool the carrier of L:
F c= I & I is Ideal of L };
set I = meet Id;
the carrier of L is Ideal of L by Th10;
then A2: the carrier of L in Id;
then A3: I c= the carrier of L by SETFAM_1:4;
A4: now let X be set; assume X in Id;
then ex X' being Element of bool the carrier of L st
X'=X & F c= X' & X' is Ideal of L;
hence F c= X;
end;
then A5: F c= I by A2,SETFAM_1:6;
consider x being set such that
A6: x in F by A1,XBOOLE_0:def 1;
reconsider I as non empty Subset of L by A3,A5,A6;
A7: I is add-closed proof let x, y being Element of L; assume
A8: x in I & y in I;
now let X be set; assume
A9: X in Id;
then A10: x in X by A8,SETFAM_1:def 1;
A11: y in X by A8,A9,SETFAM_1:def 1;
consider X' being Element of bool the carrier of L such that
A12: X'=X & F c= X' & X' is Ideal of L by A9;
x+y in X' by A10,A11,A12,Def1;
hence {x+y} c= X by A12,ZFMISC_1:37;
end; then {x+y} c= I by A2,SETFAM_1:6;
hence x+y in I by ZFMISC_1:37;
end;
A13: I is left-ideal proof let p, x being Element of L;
assume
A14: x in I;
now let X be set; assume
A15: X in Id;
then A16: x in X by A14,SETFAM_1:def 1;
consider X' being Element of bool the carrier of L such that
A17: X'=X & F c= X' & X' is Ideal of L by A15;
p*x in X' by A16,A17,Def2;
hence {p*x} c= X by A17,ZFMISC_1:37;
end; then {p*x} c= I by A2,SETFAM_1:6;
hence p*x in I by ZFMISC_1:37;
end;
I is right-ideal proof
let p, x being Element of L; assume
A18: x in I;
now let X be set; assume
A19: X in Id;
then A20: x in X by A18,SETFAM_1:def 1;
consider X' being Element of bool the carrier of L such that
A21: X'=X & F c= X' & X' is Ideal of L by A19;
x*p in X' by A20,A21,Def3;
hence {x*p} c= X by A21,ZFMISC_1:37;
end; then {x*p} c= I by A2,SETFAM_1:6;
hence x*p in I by ZFMISC_1:37;
end;
then reconsider I as Ideal of L by A7,A13;
take I;
now let X be Ideal of L; assume
F c= X; then X in Id;
hence I c= X by SETFAM_1:4;
end;
hence thesis by A2,A4,SETFAM_1:6;
end;
uniqueness proof
let X,Y be Ideal of L such that
A22: F c= X & for I being Ideal of L st F c= I holds X c= I and
A23: F c= Y & for I being Ideal of L st F c= I holds Y c= I;
A24: X c= Y by A22,A23; Y c= X by A22,A23;
hence X=Y by A24,XBOOLE_0:def 10;
end;
func F-LeftIdeal -> LeftIdeal of L means :Def16
:
F c= it & for I being LeftIdeal of L st F c= I holds it c= I;
existence proof set Id = { I where I is Element of bool the carrier of L:
F c= I & I is LeftIdeal of L };
set I = meet Id; the carrier of L is LeftIdeal of L by Th11;
then A25: the carrier of L in Id;
then A26: I c= the carrier of L by SETFAM_1:4;
A27: now let X be set; assume X in Id;
then consider X' being Element of bool the carrier of L such that
A28: X'=X & F c= X' & X' is LeftIdeal of L;
thus F c= X by A28;
end;
then A29: F c= I by A25,SETFAM_1:6; consider x being set such that
A30: x in F by A1,XBOOLE_0:def 1;
reconsider I as non empty Subset of L by A26,A29,A30;
A31: I is add-closed proof let x, y being Element of L;
assume
A32: x in I & y in I;
now let X be set; assume
A33: X in Id;
then A34: x in X by A32,SETFAM_1:def 1;
A35: y in X by A32,A33,SETFAM_1:def 1;
consider X' being Element of bool the carrier of L such that
A36: X'=X & F c= X' & X' is LeftIdeal of L by A33;
x+y in X' by A34,A35,A36,Def1;
hence {x+y} c= X by A36,ZFMISC_1:37;
end; then {x+y} c= I by A25,SETFAM_1:6;
hence x+y in I by ZFMISC_1:37;
end;
I is left-ideal proof let p, x being Element of L; assume
A37: x in I;
now let X be set; assume
A38: X in Id;
then A39: x in X by A37,SETFAM_1:def 1;
consider X' being Element of bool the carrier of L such that
A40: X'=X & F c= X' & X' is LeftIdeal of L by A38;
p*x in X' by A39,A40,Def2;
hence {p*x} c= X by A40,ZFMISC_1:37;
end; then {p*x} c= I by A25,SETFAM_1:6;
hence p*x in I by ZFMISC_1:37;
end; then reconsider I as LeftIdeal of L by A31;
take I;
now let X be LeftIdeal of L; assume
F c= X; then X in Id;
hence I c= X by SETFAM_1:4;
end;
hence thesis by A25,A27,SETFAM_1:6;
end;
uniqueness proof let X,Y be LeftIdeal of L such that
A41: F c= X & for I being LeftIdeal of L st F c= I holds X c= I and
A42: F c= Y & for I being LeftIdeal of L st F c= I holds Y c= I;
A43: X c= Y by A41,A42; Y c= X by A41,A42;
hence X=Y by A43,XBOOLE_0:def 10;
end;
func F-RightIdeal -> RightIdeal of L means :Def17
:
F c= it & for I being RightIdeal of L st F c= I holds it c= I;
existence proof set Id = { I where I is Element of bool the carrier of L:
F c= I & I is RightIdeal of L };
set I = meet Id;
the carrier of L is RightIdeal of L by Th12;
then A44: the carrier of L in Id;
then A45: I c= the carrier of L by SETFAM_1:4;
A46: now let X be set; assume X in Id;
then consider X' being Element of bool the carrier of L such that
A47: X'=X & F c= X' & X' is RightIdeal of L;
thus F c= X by A47;
end;
then A48: F c= I by A44,SETFAM_1:6;
consider x being set such that
A49: x in F by A1,XBOOLE_0:def 1;
reconsider I as non empty Subset of L by A45,A48,A49;
A50: I is add-closed proof let x, y being Element of L;
assume
A51: x in I & y in I;
now let X be set; assume
A52: X in Id;
then A53: x in X by A51,SETFAM_1:def 1;
A54: y in X by A51,A52,SETFAM_1:def 1;
consider X' being Element of bool the carrier of L such that
A55: X'=X & F c= X' & X' is RightIdeal of L by A52;
x+y in X' by A53,A54,A55,Def1;
hence {x+y} c= X by A55,ZFMISC_1:37;
end; then {x+y} c= I by A44,SETFAM_1:6;
hence x+y in I by ZFMISC_1:37;
end;
I is right-ideal proof let p, x being Element of L; assume
A56: x in I;
now let X be set; assume
A57: X in Id;
then A58: x in X by A56,SETFAM_1:def 1;
consider X' being Element of bool the carrier of L such that
A59: X'=X & F c= X' & X' is RightIdeal of L by A57;
x*p in X' by A58,A59,Def3;
hence {x*p} c= X by A59,ZFMISC_1:37;
end; then {x*p} c= I by A44,SETFAM_1:6;
hence x*p in I by ZFMISC_1:37;
end;
then reconsider I as RightIdeal of L by A50;
take I;
now let X be RightIdeal of L; assume F c= X; then X in Id;
hence I c= X by SETFAM_1:4;
end;
hence thesis by A44,A46,SETFAM_1:6;
end;
uniqueness proof let X,Y be RightIdeal of L such that
A60: F c= X & for I being RightIdeal of L st F c= I holds X c= I and
A61: F c= Y & for I being RightIdeal of L st F c= I holds Y c= I;
A62: X c= Y by A60,A61; Y c= X by A60,A61;
hence X=Y by A62,XBOOLE_0:def 10;
end;
end;
theorem Th44:
for L being non empty doubleLoopStr, I being Ideal of L holds I-Ideal = I
proof let L be non empty doubleLoopStr, I be Ideal of L;
I c= I-Ideal & I-Ideal c= I by Def15; hence thesis by XBOOLE_0:def 10;
end;
theorem Th45:
for L being non empty doubleLoopStr, I being LeftIdeal of L
holds I-LeftIdeal = I
proof let L be non empty doubleLoopStr, I be LeftIdeal of L;
I c= I-LeftIdeal & I-LeftIdeal c= I by Def16; hence thesis by XBOOLE_0:def
10
;
end;
theorem Th46:
for L being non empty doubleLoopStr, I being RightIdeal of L
holds I-RightIdeal = I
proof let L be non empty doubleLoopStr, I be RightIdeal of L;
I c= I-RightIdeal & I-RightIdeal c= I by Def17; hence thesis by XBOOLE_0:
def 10;
end;
definition
let L be non empty doubleLoopStr,
I be Ideal of L;
mode Basis of I -> non empty Subset of L means
it-Ideal = I;
existence proof take I; thus thesis by Th44; end;
end;
theorem Th47:
for L being add-associative right_zeroed right_complementable
distributive (non empty doubleLoopStr)
holds {0.L}-Ideal = {0.L}
proof let L be add-associative right_zeroed right_complementable
distributive (non empty doubleLoopStr);
{0.L} is Ideal of L by Th7; hence thesis by Th44;
end;
theorem
for L being left_zeroed right_zeroed add-cancelable
distributive (non empty doubleLoopStr)
holds {0.L}-Ideal = {0.L}
proof let L be left_zeroed right_zeroed add-cancelable
distributive (non empty doubleLoopStr);
{0.L} is Ideal of L by Th4,Th5,Th6; hence thesis by Th44;
end;
theorem
for L being left_zeroed right_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr)
holds {0.L}-LeftIdeal = {0.L}
proof let L be left_zeroed right_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr);
{0.L} is LeftIdeal of L by Th4,Th5; hence thesis by Th45;
end;
theorem
for L being right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr)
holds {0.L}-RightIdeal = {0.L}
proof let L be right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr);
{0.L} is RightIdeal of L by Th4,Th6; hence thesis by Th46;
end;
theorem
for L being well-unital (non empty doubleLoopStr)
holds {1_ L}-Ideal = the carrier of L
proof let L be well-unital (non empty doubleLoopStr);
the carrier of L c= {1_ L}-Ideal proof let x be set;
assume x in the carrier of L;
then reconsider x'=x as Element of L;
A1: 1_ L in {1_ L} by TARSKI:def 1;
{1_ L} c= {1_ L}-Ideal by Def15;
then x'*1_ L in {1_ L}-Ideal by A1,Def2;
hence thesis by VECTSP_2:def 2;
end;
hence thesis by XBOOLE_0:def 10;
end;
theorem
for L being right_unital (non empty doubleLoopStr)
holds {1_ L}-LeftIdeal = the carrier of L
proof let L be right_unital (non empty doubleLoopStr);
the carrier of L c= {1_ L}-LeftIdeal proof let x be set;
assume x in the carrier of L;
then reconsider x'=x as Element of L;
A1: 1_ L in {1_ L} by TARSKI:def 1;
{1_ L} c= {1_ L}-LeftIdeal by Def16;
then x'*1_ L in {1_ L}-LeftIdeal by A1,Def2;
hence thesis by VECTSP_1:def 13;
end;
hence thesis by XBOOLE_0:def 10;
end;
theorem
for L being left_unital (non empty doubleLoopStr)
holds {1_ L}-RightIdeal = the carrier of L
proof let L be left_unital (non empty doubleLoopStr);
the carrier of L c= {1_ L}-RightIdeal proof let x be set;
assume x in the carrier of L;
then reconsider x'=x as Element of L;
A1: 1_ L in {1_ L} by TARSKI:def 1;
{1_ L} c= {1_ L}-RightIdeal by Def17;
then (1_ L)*x' in {1_ L}-RightIdeal by A1,Def3;
hence thesis by VECTSP_1:def 19;
end;
hence thesis by XBOOLE_0:def 10;
end;
theorem
for L being non empty doubleLoopStr holds ([#] L)-Ideal = the carrier of L
proof let L be non empty doubleLoopStr;
A1: [#] L = the carrier of L by PRE_TOPC:def 3;
[#] L c= ([#] L)-Ideal by Def15;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
for L being non empty doubleLoopStr holds ([#] L)-LeftIdeal = the carrier of
L
proof let L be non empty doubleLoopStr;
A1: [#] L = the carrier of L by PRE_TOPC:def 3;
[#] L c= ([#] L)-LeftIdeal by Def16;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
for L being non empty doubleLoopStr holds ([#]
L)-RightIdeal = the carrier of L
proof let L be non empty doubleLoopStr;
A1: [#] L = the carrier of L by PRE_TOPC:def 3;
[#] L c= ([#] L)-RightIdeal by Def17;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th57:
for L being non empty doubleLoopStr,
A, B being non empty Subset of L
st A c= B holds A-Ideal c= B-Ideal
proof let L be non empty doubleLoopStr,
A,B be non empty Subset of L;
assume A1: A c= B; B c= B-Ideal by Def15; then A c= B-Ideal by A1,XBOOLE_1:1
;
hence thesis by Def15;
end;
theorem
for L being non empty doubleLoopStr,
A, B being non empty Subset of L
st A c= B holds A-LeftIdeal c= B-LeftIdeal
proof let L be non empty doubleLoopStr,
A,B be non empty Subset of L;
assume A1: A c= B; B c= B-LeftIdeal by Def16;
then A c= B-LeftIdeal by A1,XBOOLE_1:1;
hence thesis by Def16;
end;
theorem
for L being non empty doubleLoopStr,
A, B being non empty Subset of L
st A c= B holds A-RightIdeal c= B-RightIdeal
proof let L be non empty doubleLoopStr,
A,B be non empty Subset of L;
assume A1: A c= B; B c= B-RightIdeal by Def17;
then A c= B-RightIdeal by A1,XBOOLE_1:1;
hence thesis by Def17;
end;
theorem Th60:
for L being add-associative left_zeroed right_zeroed add-cancelable
associative distributive well-unital (non empty doubleLoopStr),
F being non empty Subset of L, x being set
holds x in F-Ideal iff ex f being LinearCombination of F st x = Sum f
proof let L be add-associative right_zeroed add-cancelable left_zeroed
associative distributive well-unital (non empty doubleLoopStr),
F be non empty Subset of L;
set I = { x where x is Element of L:
ex lc being LinearCombination of F st Sum lc = x };
A1: I c= F-Ideal proof let x be set;
defpred P[Nat] means
for lc being LinearCombination of F st len lc <= $1
holds Sum lc in F-Ideal;
A2: P[0] proof let lc be LinearCombination of F; assume
len lc <= 0;
then len lc = 0 by NAT_1:18;
then lc = <*>(the carrier of L) by FINSEQ_1:25;
then A3: Sum lc = 0.L by RLVECT_1:60; consider y being Element of F;
F c= F-Ideal by Def15;
then A4: y in F-Ideal by TARSKI:def 3;
0.L*y = 0.L by BINOM:1;
hence thesis by A3,A4,Def2;
end;
A5: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume
A6: P[k];
thus P[k+1] proof let lc be LinearCombination of F; assume
A7: len lc <= k+1;
per cases by A7,NAT_1:26; suppose
len lc <= k;
hence thesis by A6;
suppose
A8: len lc = k+1;
then lc is non empty by FINSEQ_1:25;
then consider q being LinearCombination of F,
r being Element of L such that
A9: lc=q^<*r*> & <*r*> is LinearCombination of F by Th32;
k+1 = len q + len <*r*> by A8,A9,FINSEQ_1:35
.= len q + 1 by FINSEQ_1:56;
then len q = k by XCMPLX_1:2;
then A10: Sum q in F-Ideal by A6;
dom <*r*> = {1} by FINSEQ_1:4,55;
then A11: 1 in dom <*r*> by TARSKI:def 1;
then consider u,v being Element of L, a being Element of F such
that
A12: <* r *>/.1 = u*a*v by A9,Def9;
A13: <*r*>/.1 = <*r*>.1 by A11,FINSEQ_4:def 4;
A14: Sum <* r *> = r by BINOM:3
.= u*a*v by A12,A13,FINSEQ_1:57;
F c= F-Ideal by Def15
; then a in F-Ideal by TARSKI:def 3;
then u*a in F-Ideal by Def2;
then A15: Sum <* r *> in F-Ideal by A14,Def3;
Sum lc = Sum q + Sum <* r *> by A9,RLVECT_1:58;
hence thesis by A10,A15,Def1;
end;
end;
A16: for k being Nat holds P[k] from Ind(A2,A5);
assume x in I;
then consider x' being Element of L such that
A17: x'=x & ex lc being LinearCombination of F st Sum lc = x';
consider lc being LinearCombination of F such that
A18: Sum lc = x' by A17; P[len lc] by A16;
hence x in F-Ideal by A17,A18;
end;
A19: F c= I proof let x be set; assume
A20: x in F; then reconsider x as Element of L;
set lc = <* x *>;
now let i be set; assume
A21: i in dom lc;
then A22: lc/.i = lc.i by FINSEQ_4:def 4;
dom lc = {1} by FINSEQ_1:4,55;
then i = 1 by A21,TARSKI:def 1;
then lc.i = x by FINSEQ_1:57 .= 1_ L*x by VECTSP_2:def 2
.= 1_ L*x*1_ L by VECTSP_2:def 2;
hence ex u,v being Element of L, a being Element of F st
lc/.i = u*a*v by A20,A22;
end; then reconsider lc as LinearCombination of F by Def9;
Sum lc = x by BINOM:3;
hence thesis;
end;
A23: I c= the carrier of L proof let x be set; assume x in I;
then consider x' being Element of L such that
A24: x'=x & ex lc being LinearCombination of F st Sum lc = x';
thus thesis by A24;
end;
consider x being set such that
A25: x in F by XBOOLE_0:def 1;
reconsider I as non empty Subset of L by A19,A23,A25;
reconsider I'=I as non empty Subset of L;
A26: I' is add-closed proof let x, y be Element of L; assume
A27: x in I' & y in I';
then consider x' being Element of L such that
A28: x'=x & ex lc being LinearCombination of F st Sum lc = x';
consider y' being Element of L such that
A29: y'=y & ex lc being LinearCombination of F st Sum lc = y' by A27;
consider lcx being LinearCombination of F such that
A30: Sum lcx = x' by A28;
consider lcy being LinearCombination of F such that
A31: Sum lcy = y' by A29;
Sum (lcx^lcy) = x' + y' by A30,A31,RLVECT_1:58;
hence x+y in I' by A28,A29;
end;
A32: I' is left-ideal proof
let p, x be Element of L; assume x in I';
then consider x' being Element of L such that
A33: x'=x & ex lc being LinearCombination of F st Sum lc = x';
consider lcx being LinearCombination of F such that
A34: Sum lcx = x' by A33;
reconsider plcx = p*lcx as LinearCombination of F by Th23;
p*x = Sum plcx by A33,A34,BINOM:4;
hence p*x in I';
end;
I' is right-ideal proof
let p, x be Element of L; assume x in I';
then consider x' being Element of L such that
A35: x'=x & ex lc being LinearCombination of F st Sum lc = x';
consider lcx being LinearCombination of F such that
A36: Sum lcx = x' by A35;
reconsider lcxp = lcx*p as LinearCombination of F by Th24;
x*p = Sum lcxp by A35,A36,BINOM:5;
hence x*p in I';
end;
then F-Ideal c= I by A19,A26,A32,Def15;
then A37: I = F-Ideal by A1,XBOOLE_0:def 10;
let x be set;
hereby assume x in F-Ideal;
then consider x' being Element of L such that
A38: x'=x & ex lc being LinearCombination of F st Sum lc = x' by A37;
thus ex f being LinearCombination of F st x = Sum f by A38;
end;
assume ex f being LinearCombination of F st x = Sum f;
hence x in F-Ideal by A37;
end;
theorem Th61:
for L being add-associative left_zeroed right_zeroed add-cancelable
associative distributive well-unital (non empty doubleLoopStr),
F being non empty Subset of L, x being set
holds x in F-LeftIdeal iff ex f being LeftLinearCombination of F st x = Sum f
proof let L be add-associative right_zeroed add-cancelable left_zeroed
associative distributive well-unital (non empty doubleLoopStr),
F be non empty Subset of L;
set I = { x where x is Element of L:
ex lc being LeftLinearCombination of F st Sum lc = x };
A1: I c= F-LeftIdeal proof let x be set;
defpred P[Nat] means
for lc being LeftLinearCombination of F st len lc <= $1
holds Sum lc in F-LeftIdeal;
A2: P[0] proof let lc be LeftLinearCombination of F; assume
len lc <= 0;
then len lc = 0 by NAT_1:18;
then lc = <*>(the carrier of L) by FINSEQ_1:25;
then A3: Sum lc = 0.L by RLVECT_1:60; consider y being Element
of F;
F c= F-LeftIdeal by Def16;
then A4: y in F-LeftIdeal by TARSKI:def 3;
0.L*y = 0.L by BINOM:1;
hence thesis by A3,A4,Def2;
end;
A5: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume
A6: P[k];
thus P[k+1] proof let lc be LeftLinearCombination of F; assume
A7: len lc <= k+1;
per cases by A7,NAT_1:26; suppose
len lc <= k;
hence thesis by A6;
suppose
A8: len lc = k+1;
then lc is non empty by FINSEQ_1:25;
then consider q being LeftLinearCombination of F,
r being Element of L such that
A9: lc=q^<*r*> & <*r*> is LeftLinearCombination of F by Th33;
k+1 = len q + len <*r*> by A8,A9,FINSEQ_1:35
.= len q + 1 by FINSEQ_1:56;
then len q = k by XCMPLX_1:2;
then A10: Sum q in F-LeftIdeal by A6;
dom <*r*> = {1} by FINSEQ_1:4,55;
then A11: 1 in dom <*r*> by TARSKI:def 1;
then consider u being Element of L, a being Element of F such
that
A12: <* r *>/.1 = u*a by A9,Def10;
A13: <*r*>/.1 = <*r*>.1 by A11,FINSEQ_4:def 4;
A14: Sum <* r *> = r by BINOM:3 .= u*a by A12,A13,FINSEQ_1:57;
F c= F-LeftIdeal by Def16;
then a in F-LeftIdeal by TARSKI:def 3;
then A15: Sum <* r *> in F-LeftIdeal by A14,Def2;
Sum lc = Sum q + Sum <* r *> by A9,RLVECT_1:58;
hence thesis by A10,A15,Def1;
end;
end;
A16: for k being Nat holds P[k] from Ind(A2,A5);
assume x in I;
then consider x' being Element of L such that
A17: x'=x & ex lc being LeftLinearCombination of F st Sum lc = x';
consider lc being LeftLinearCombination of F such that
A18: Sum lc = x' by A17; P[len lc] by A16;
hence x in F-LeftIdeal by A17,A18;
end;
A19: F c= I proof let x be set; assume
A20: x in F; then reconsider x as Element of L;
set lc = <* x *>;
now let i be set; assume
A21: i in dom lc;
then A22: lc/.i = lc.i by FINSEQ_4:def 4;
dom lc = {1} by FINSEQ_1:4,55;
then i = 1 by A21,TARSKI:def 1;
then lc.i = x by FINSEQ_1:57 .= 1_ L*x by VECTSP_2:def 2;
hence ex u being Element of L, a being Element of F st
lc/.i = u*a by A20,A22;
end; then reconsider lc as LeftLinearCombination of F by Def10;
Sum lc = x by BINOM:3;
hence thesis;
end;
A23: I c= the carrier of L proof let x be set; assume x in I;
then consider x' being Element of L such that
A24: x'=x & ex lc being LeftLinearCombination of F st Sum lc = x';
thus thesis by A24;
end;
consider x being set such that
A25: x in F by XBOOLE_0:def 1;
reconsider I as non empty Subset of L by A19,A23,A25;
reconsider I'=I as non empty Subset of L;
A26: I' is add-closed proof let x, y be Element of L; assume
A27: x in I' & y in I';
then consider x' being Element of L such that
A28: x'=x & ex lc being LeftLinearCombination of F st Sum lc = x';
consider y' being Element of L such that
A29: y'=y & ex lc being LeftLinearCombination of F st Sum lc = y' by A27;
consider lcx being LeftLinearCombination of F such that
A30: Sum lcx = x' by A28;
consider lcy being LeftLinearCombination of F such that
A31: Sum lcy = y' by A29;
Sum (lcx^lcy) = x' + y' by A30,A31,RLVECT_1:58;
hence x+y in I' by A28,A29;
end;
I' is left-ideal proof
let p, x be Element of L; assume x in I';
then consider x' being Element of L such that
A32: x'=x & ex lc being LeftLinearCombination of F st Sum lc = x';
consider lcx being LeftLinearCombination of F such that
A33: Sum lcx = x' by A32;
reconsider plcx = p*lcx as LeftLinearCombination of F by Th26;
p*x = Sum plcx by A32,A33,BINOM:4;
hence p*x in I';
end;
then F-LeftIdeal c= I by A19,A26,Def16;
then A34: I = F-LeftIdeal by A1,XBOOLE_0:def 10;
let x be set;
hereby assume x in F-LeftIdeal;
then consider x' being Element of L such that
A35: x'=x & ex lc being LeftLinearCombination of F st Sum lc = x' by A34;
thus ex f being LeftLinearCombination of F st x = Sum f by A35;
end;
assume ex f being LeftLinearCombination of F st x = Sum f;
hence x in F-LeftIdeal by A34;
end;
theorem Th62:
for L being add-associative left_zeroed right_zeroed add-cancelable
associative distributive well-unital (non empty doubleLoopStr),
F being non empty Subset of L, x being set
holds x in F-RightIdeal iff ex f being RightLinearCombination of F st x = Sum
f
proof let L be add-associative left_zeroed right_zeroed add-cancelable
associative distributive well-unital (non empty doubleLoopStr),
F be non empty Subset of L;
set I = { x where x is Element of L:
ex lc being RightLinearCombination of F st Sum lc = x };
A1: I c= F-RightIdeal proof let x be set;
defpred P[Nat] means
for lc being RightLinearCombination of F st len lc <= $1
holds Sum lc in F-RightIdeal;
A2: P[0] proof let lc be RightLinearCombination of F; assume
len lc <= 0;
then len lc = 0 by NAT_1:18;
then lc = <*>(the carrier of L) by FINSEQ_1:25;
then A3: Sum lc = 0.L by RLVECT_1:60;
consider y being Element of F; F c= F-RightIdeal by Def17;
then A4: y in F-RightIdeal by TARSKI:def 3;
y*0.L = 0.L by BINOM:2;
hence thesis by A3,A4,Def3;
end;
A5: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume
A6: P[k];
thus P[k+1] proof let lc be RightLinearCombination of F;
assume
A7: len lc <= k+1;
per cases by A7,NAT_1:26; suppose
len lc <= k;
hence thesis by A6;
suppose
A8: len lc = k+1;
then lc is non empty by FINSEQ_1:25;
then consider q being RightLinearCombination of F,
r being Element of L such that
A9: lc=q^<*r*> & <*r*> is RightLinearCombination of F by Th34;
k+1 = len q + len <*r*> by A8,A9,FINSEQ_1:35
.= len q + 1 by FINSEQ_1:56;
then len q = k by XCMPLX_1:2;
then A10: Sum q in F-RightIdeal by A6;
dom <*r*> = {1} by FINSEQ_1:4,55;
then A11: 1 in dom <*r*> by TARSKI:def 1;
then consider v being Element of L, a being Element of F such
that
A12: <* r *>/.1 = a*v by A9,Def11;
A13: <*r*>/.1 = <*r*>.1 by A11,FINSEQ_4:def 4;
A14: Sum <* r *> = r by BINOM:3
.= a*v by A12,A13,FINSEQ_1:57;
F c= F-RightIdeal by Def17;
then a in F-RightIdeal by TARSKI:def 3;
then A15: Sum <* r *> in F-RightIdeal by A14,Def3;
Sum lc = Sum q + Sum <* r *> by A9,RLVECT_1:58;
hence thesis by A10,A15,Def1;
end;
end;
A16: for k being Nat holds P[k] from Ind(A2,A5);
assume x in I;
then consider x' being Element of L such that
A17: x'=x & ex lc being RightLinearCombination of F st Sum lc = x';
consider lc being RightLinearCombination of F such that
A18: Sum lc = x' by A17; P[len lc] by A16;
hence x in F-RightIdeal by A17,A18;
end;
A19: F c= I proof let x be set; assume
A20: x in F; then reconsider x as Element of L;
set lc = <* x *>;
now let i be set; assume
A21: i in dom lc;
then A22: lc/.i = lc.i by FINSEQ_4:def 4;
dom lc = {1} by FINSEQ_1:4,55;
then i = 1 by A21,TARSKI:def 1;
then lc.i = x by FINSEQ_1:57 .= x*1_ L by VECTSP_2:def 2;
hence ex v being Element of L, a being Element of F st
lc/.i = a*v by A20,A22;
end; then reconsider lc as RightLinearCombination of F by Def11;
Sum lc = x by BINOM:3;
hence thesis;
end;
A23: I c= the carrier of L proof let x be set; assume x in I;
then consider x' being Element of L such that
A24: x'=x & ex lc being RightLinearCombination of F st Sum lc = x';
thus thesis by A24;
end;
consider x being set such that
A25: x in F by XBOOLE_0:def 1;
reconsider I as non empty Subset of L by A19,A23,A25;
reconsider I'=I as non empty Subset of L;
A26: I' is add-closed proof let x, y be Element of L; assume
A27: x in I' & y in I';
then consider x' being Element of L such that
A28: x'=x & ex lc being RightLinearCombination of F st Sum lc = x';
consider y' being Element of L such that
A29: y'=y & ex lc being RightLinearCombination of F st Sum lc = y' by A27;
consider lcx being RightLinearCombination of F such that
A30: Sum lcx = x' by A28;
consider lcy being RightLinearCombination of F such that
A31: Sum lcy = y' by A29;
Sum (lcx^lcy) = x' + y' by A30,A31,RLVECT_1:58;
hence x+y in I' by A28,A29;
end;
I' is right-ideal proof
let p, x be Element of L; assume x in I';
then consider x' being Element of L such that
A32: x'=x & ex lc being RightLinearCombination of F st Sum lc = x';
consider lcx being RightLinearCombination of F such that
A33: Sum lcx = x' by A32;
reconsider lcxp = lcx*p as RightLinearCombination of F by Th29;
x*p = Sum lcxp by A32,A33,BINOM:5;
hence x*p in I';
end;
then F-RightIdeal c= I by A19,A26,Def17;
then A34: I = F-RightIdeal by A1,XBOOLE_0:def 10;
let x be set;
hereby assume x in F-RightIdeal;
then consider x' being Element of L such that
A35: x'=x & ex lc being RightLinearCombination of F st Sum lc = x' by A34;
thus ex f being RightLinearCombination of F st x = Sum f by A35;
end;
assume ex f being RightLinearCombination of F st x = Sum f;
hence x in F-RightIdeal by A34;
end;
theorem Th63:
for R being add-associative left_zeroed right_zeroed add-cancelable well-unital
associative commutative distributive (non empty doubleLoopStr),
F being non empty Subset of R
holds F-Ideal = F-LeftIdeal & F-Ideal = F-RightIdeal
proof let R be add-associative left_zeroed right_zeroed add-cancelable
well-unital associative commutative distributive (non empty doubleLoopStr),
F be non empty Subset of R;
now let x be set;
hereby assume x in F-Ideal;
then consider lc being LinearCombination of F such that
A1: x = Sum lc by Th60; lc is LeftLinearCombination of F by Th31;
hence x in F-LeftIdeal by A1,Th61;
end;
assume x in F-LeftIdeal;
then consider lc being LeftLinearCombination of F such that
A2: x = Sum lc by Th61; lc is LinearCombination of F by Th25;
hence x in F-Ideal by A2,Th60;
end;
hence F-Ideal = F-LeftIdeal by TARSKI:2;
now let x be set;
hereby assume x in F-Ideal;
then consider lc being LinearCombination of F such that
A3: x = Sum lc by Th60; lc is RightLinearCombination of F by Th31;
hence x in F-RightIdeal by A3,Th62;
end;
assume x in F-RightIdeal;
then consider lc being RightLinearCombination of F such that
A4: x = Sum lc by Th62; lc is LinearCombination of F by Th28;
hence x in F-Ideal by A4,Th60;
end;
hence F-Ideal = F-RightIdeal by TARSKI:2;
end;
theorem Th64:
for R being add-associative left_zeroed right_zeroed add-cancelable well-unital
associative commutative distributive (non empty doubleLoopStr),
a being Element of R
holds {a}-Ideal = {a*r where r is Element of R : not contradiction}
proof let R be add-associative left_zeroed right_zeroed add-cancelable
well-unital commutative associative distributive (non empty doubleLoopStr),
a be Element of R;
set A = {a};
reconsider a as Element of A by TARSKI:def 1;
set M = {Sum s where s is LinearCombination of A : not contradiction};
set N = {a*r where r is Element of R : not contradiction};
A1: for u being set holds u in M implies u in N
proof let u be set; assume u in M;
then consider s being LinearCombination of A such that A2: u = Sum s;
A3: 0 <= len s by NAT_1:18;
consider f being Function of NAT,the carrier of R such that
A4: Sum s = f.(len s) and
A5: f.0 = 0.R and
A6: for j being Nat,v being Element of R
st j < len s & v = s.(j + 1) holds f.(j + 1) = f.j + v
by RLVECT_1:def 12;
defpred P[Nat] means ex r being Element of R st f.($1) = a*r;
f.0 = a*0.R by A5,BINOM:2;
then A7: P[0];
A8: now let j be Nat;
assume A9: 0 <= j & j < len s;
thus P[j] implies P[j+1]
proof assume ex r being Element of R st f.j = a*r;
then consider r1 being Element of R such that A10: f.j = a*r1;
A11: 0 + 1 <= j + 1 by A9,AXIOMS:24;
j + 1 <= len s by A9,NAT_1:38;
then j + 1 in Seg(len s) by A11,FINSEQ_1:3;
then A12: j + 1 in dom s by FINSEQ_1:def 3;
then s.(j+1) = s/.(j+1) by FINSEQ_4:def 4;
then A13: f.(j+1) = f.j + s/.(j+1) by A6,A9;
consider r2,r3 being Element of R, a' being Element of A such that
A14: s/.(j+1) = r2*a'*r3 by A12,Def9;
f.(j+1) = a*r1 + r2*a*r3 by A10,A13,A14,TARSKI:def 1
.= a*r1 + a*(r2*r3) by VECTSP_1:def 16
.= a*(r1 + r2*r3) by VECTSP_1:def 18;
hence thesis;
end;
end;
for k being Nat st 0 <= k & k <= len s holds P[k] from FinInd(A7,A8);
then ex r being Element of R st Sum s = a*r by A3,A4;
hence thesis by A2;
end;
for u being set holds u in N implies u in M
proof let u be set; assume u in N;
then consider r being Element of R such that
A15: u = a*r;
set s = <* a*r *>;
for i being set st i in dom s
ex r,t being Element of R, a being Element of A st s/.i = r*a*t
proof let i be set; assume
A16: i in dom s;
len s = 1 by FINSEQ_1:57; then i in {1} by A16,FINSEQ_1:4,def 3;
then i = 1 by TARSKI:def 1;
then s/.i = a*r by FINSEQ_4:25 .= (r*a)*1_ R by VECTSP_1:def 13;
hence thesis;
end; then reconsider s as LinearCombination of A by Def9;
Sum s = a*r by BINOM:3;
hence u in M by A15;
end;
then A17: M = N by A1,TARSKI:2;
now let x be set;
hereby assume x in {a}-Ideal; then x in {a}-RightIdeal by Th63;
then consider f being RightLinearCombination of A such that
A18: x = Sum f by Th62; f is LinearCombination of A by Th28;
hence x in M by A18;
end;
assume x in M; then consider s being LinearCombination of A such that
A19: x = Sum s;
thus x in {a}-Ideal by A19,Th60;
end;
hence thesis by A17,TARSKI:2;
end;
theorem Th65:
for R being Abelian left_zeroed right_zeroed
add-cancelable well-unital add-associative
associative commutative distributive (non empty doubleLoopStr),
a,b being Element of R
holds {a,b}-Ideal = {a*r + b*s where r,s is Element of R : not contradiction}
proof let R be Abelian left_zeroed right_zeroed add-cancelable associative
well-unital add-associative commutative
distributive (non empty doubleLoopStr), a,b be Element of R;
set A = {a,b};
reconsider a,b as Element of A by TARSKI:def 2;
set M = {Sum s where s is LinearCombination of A : not contradiction};
set N = {a*r + b*s where r,s is Element of R : not contradiction};
A1: for u being set holds u in M implies u in N
proof let u be set; assume u in M;
then consider s being LinearCombination of A such that A2: u = Sum s;
A3: 0 <= len s by NAT_1:18;
consider f being Function of NAT,the carrier of R such that
A4: Sum s = f.(len s) and
A5: f.0 = 0.R and
A6: for j being Nat,v being Element of R
st j < len s & v = s.(j + 1) holds f.(j + 1) = f.j + v
by RLVECT_1:def 12;
defpred P[Nat] means
ex r,s being Element of R st f.($1) = a*r + b*s;
f.0 = a*0.R by A5,BINOM:2
.= a*0.R + 0.R by RLVECT_1:def 7 .= a*0.R + b*0.R by BINOM:2;
then A7: P[0];
A8: now let j be Nat; assume A9: 0 <= j & j < len s;
thus P[j] implies P[j+1]
proof assume ex r,s being Element of R st f.j = a*r + b*s;
then consider r1,s1 being Element of R such that
A10: f.j = a*r1 + b*s1;
A11: 0 + 1 <= j + 1 by A9,AXIOMS:24;
j + 1 <= len s by A9,NAT_1:38;
then j + 1 in Seg(len s) by A11,FINSEQ_1:3;
then A12: j + 1 in dom s by FINSEQ_1:def 3;
then consider r2,r3 being Element of R, a' being Element of A such
that
A13: s/.(j+1) = r2*a'*r3 by Def9;
A14: s/.(j+1) = s.(j+1) by A12,FINSEQ_4:def 4;
per cases by TARSKI:def 2;
suppose a' = a;
then f.(j+1) = (a*r1 + b*s1) + r2*a*r3 by A6,A9,A10,A13,A14
.= (a*r1 + a*r2*r3) + b*s1 by RLVECT_1:def 6
.= (a*r1 + a*(r2*r3)) + b*s1 by VECTSP_1:def 16
.= a*(r1 + r2*r3) + b*s1 by VECTSP_1:def 18;
hence thesis;
suppose a' = b;
then f.(j+1) = (a*r1 + b*s1) + r2*b*r3 by A6,A9,A10,A13,A14
.= a*r1 + (b*s1 + b*r2*r3) by RLVECT_1:def 6
.= a*r1 + (b*s1 + b*(r2*r3)) by VECTSP_1:def 16
.= a*r1 + b*(s1 + r2*r3) by VECTSP_1:def 18;
hence thesis;
end;
end;
for k being Nat st 0 <= k & k <= len s holds P[k] from FinInd(A7,A8);
then ex r,t being Element of R st Sum s = a*r + b*t by A3,A4;
hence thesis by A2;
end;
for u being set holds u in N implies u in M proof
let u be set; assume u in N; then consider r,t being Element of R such that
A15: u = a*r + b*t;
set s = <* a*r, b*t *>;
for i being set st i in dom s
ex r,t being Element of R, a being Element of A st s/.i = r*a*t
proof let i be set; assume
A16: i in dom s; then i in Seg(len s) by FINSEQ_1:def 3;
then A17: i in {1,2} by FINSEQ_1:4,61;
per cases by A17,TARSKI:def 2;
suppose i = 1;
then s/.i = s.1 by A16,FINSEQ_4:def 4 .= a*r by FINSEQ_1:61
.= 1_ R*a*r by VECTSP_1:def 19;
hence thesis;
suppose i = 2;
then s/.i = s.2 by A16,FINSEQ_4:def 4 .= b*t by FINSEQ_1:61
.= 1_ R*b*t by VECTSP_1:def 19;
hence thesis;
end;
then reconsider s as LinearCombination of A by Def9;
Sum s = a*r + b*t by Th1;
hence u in M by A15;
end;
then A18: M = N by A1,TARSKI:2;
now let x be set;
hereby assume x in {a,b}-Ideal; then x in {a,b}-RightIdeal by Th63;
then consider f being RightLinearCombination of A such that
A19: x = Sum f by Th62;
f is LinearCombination of A by Th28;
hence x in M by A19;
end;
assume x in M; then consider s being LinearCombination of A such that
A20: x = Sum s;
thus x in {a,b}-Ideal by A20,Th60;
end;
hence thesis by A18,TARSKI:2;
end;
theorem Th66:
for R being non empty doubleLoopStr, a being Element of R
holds a in {a}-Ideal
proof let R be non empty doubleLoopStr, a be Element of R;
a in {a} & {a} c= {a}-Ideal by Def15,TARSKI:def 1;
hence thesis;
end;
theorem
for R being Abelian left_zeroed right_zeroed right_complementable
add-associative associative commutative
distributive well-unital (non empty doubleLoopStr),
A being non empty Subset of R, a being Element of R
holds a in A-Ideal implies {a}-Ideal c= A-Ideal
proof let R be left_zeroed right_zeroed right_complementable add-associative
associative distributive well-unital
commutative Abelian (non empty doubleLoopStr),
A be non empty Subset of R, a be Element of R;
assume a in A-Ideal;
then consider s being LinearCombination of A such that A1: a = Sum s by Th60;
now let u be set;
assume u in {a}-Ideal;
then u in {a*r where r is Element of R : not contradiction} by Th64;
then consider r being Element of R such that A2: u = a*r; set t = s*r;
A3: dom s = dom t by POLYNOM1:def 3;
for i being set st i in dom t
ex u,v being Element of R, a being Element of A st t/.i = u*a*v
proof let i be set; assume A4: i in dom t;
then consider u,v being Element of R, b being Element of A such that
A5: s/.i = u*b*v by A3,Def9;
t/.i = (u*b*v)*r by A3,A4,A5,POLYNOM1:def 3
.= u*b*(v*r) by VECTSP_1:def 16;
hence thesis;
end;
then A6: t is LinearCombination of A by Def9;
Sum t = u by A1,A2,BINOM:5;
hence u in A-Ideal by A6,Th60;
end;
hence thesis by TARSKI:def 3;
end;
Lm2:
for a,b being set holds {a} c= {a,b}
proof let a,b be set;
now let u be set; assume u in {a}; then u = a by TARSKI:def 1;
hence u in {a,b} by TARSKI:def 2;
end;
hence thesis by TARSKI:def 3;
end;
theorem
for R being non empty doubleLoopStr, a,b being Element of R
holds a in {a,b}-Ideal & b in {a,b}-Ideal
proof let R be non empty doubleLoopStr, a,b be Element of R;
{a} c= {a,b} by Lm2; then A1: {a}-Ideal c= {a,b}-Ideal by Th57;
a in {a}-Ideal by Th66;
hence a in {a,b}-Ideal by A1; {b} c= {a,b} by Lm2;
then A2: {b}-Ideal c= {a,b}-Ideal by Th57;
b in {b}-Ideal by Th66;
hence b in {a,b}-Ideal by A2;
end;
theorem
for R being non empty doubleLoopStr, a,b being Element of R
holds {a}-Ideal c= {a,b}-Ideal & {b}-Ideal c= {a,b}-Ideal
proof let R be non empty doubleLoopStr, a,b be Element of R;
{a} c= {a,b} & {b} c= {a,b} by Lm2;
hence thesis by Th57;
end;
begin :: Some Operations on Ideals
definition
let R be non empty HGrStr, I be Subset of R, a be Element of R;
func a*I -> Subset of R equals :Def19:
{a*i where i is Element of R : i in I};
coherence proof set M = {a*i where i is Element of R : i in I};
M is Subset of R proof
per cases;
suppose A1: I is empty;
M is empty proof assume M is non empty;
then reconsider M as non empty set; consider b being Element of M;
b in {a*i where i is Element of R : i in I};
then consider i being Element of R such that
A2: b = a*i & i in I;
thus thesis by A1,A2;
end;
then for u being set holds u in M implies u in the carrier of R;
hence thesis by TARSKI:def 3;
suppose I is non empty;
then reconsider I as non empty set;
consider j' being Element of I;
j' in I;
then reconsider j = j' as Element of R;
a*j in {a*i where i is Element of R : i in I};
then reconsider M as non empty set;
for x being set holds x in M implies x in the carrier of R proof
let x be set; assume x in M;
then consider i being Element of R such that A3: x = a*i & i in I;
thus thesis by A3;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis;
end;
end;
definition
let R be non empty multLoopStr, I be non empty Subset of R, a be Element of R;
cluster a*I -> non empty;
coherence proof
consider j being Element of I; a*j in {a*i where i is Element of R : i in I}
;
hence thesis by Def19;
end;
end;
definition
let R be distributive (non empty doubleLoopStr),
I be add-closed Subset of R, a be Element of R;
cluster a*I -> add-closed;
coherence proof set M = {a*i where i is Element of R : i in I};
A1: M = a*I by Def19;
for x,y being Element of R st x in M & y in M holds x+y in
M proof
let x,y be Element of R; assume A2: x in M & y in M;
then consider i being Element of R such that A3: x = a*i & i in I;
consider j being Element of R such that A4: y = a*j & j in I by A2;
reconsider k = i + j as Element of R;
A5: k in I by A3,A4,Def1;
x + y = a*k by A3,A4,VECTSP_1:def 18;
hence thesis by A5;
end;
hence thesis by A1,Def1;
end;
end;
definition
let R be associative (non empty doubleLoopStr),
I be right-ideal Subset of R, a be Element of R;
cluster a*I -> right-ideal;
coherence proof set M = {a*i where i is Element of R : i in I};
A1: M = a*I by Def19;
for y,x being Element of R st x in M holds x*y in M proof
let y,x be Element of R; assume x in M;
then consider i being Element of R such that A2: x = a*i & i in I;
A3: x*y = a*(i*y) by A2,VECTSP_1:def 16; i*y in
I by A2,Def3;
hence thesis by A3;
end;
hence thesis by A1,Def3;
end;
end;
theorem Th70:
for R being right_zeroed add-left-cancelable left-distributive
(non empty doubleLoopStr), I being non empty Subset of R
holds 0.R*I = {0.R}
proof let R be right_zeroed add-left-cancelable left-distributive
(non empty doubleLoopStr),
I be non empty Subset of R;
A1: now let u be set; assume u in {0.R}; then A2: u = 0.R by TARSKI:def 1;
consider j being Element of I;
0.R*j = 0.R by BINOM:1; then 0.R in {0.R*i where i is Element of R : i in
I};
hence u in 0.R*I by A2,Def19;
end;
now let u be set; assume u in 0.R*I;
then u in {0.R*i where i is Element of R : i in I} by Def19;
then consider i being Element of R such that A3: u = 0.R*i & i in I;
u = 0.R by A3,BINOM:1;
hence u in {0.R} by TARSKI:def 1;
end;
hence 0.R*I = {0.R} by A1,TARSKI:2;
end;
theorem
for R being left_unital (non empty doubleLoopStr), I being Subset of R
holds 1_ R*I = I
proof let R be left_unital (non empty doubleLoopStr), I be Subset of R;
A1: now let u be set; assume A2: u in I;
then reconsider u' = u as Element of R;
1_ R*u' = u' by VECTSP_1:def 19;
then u' in {1_ R*i where i is Element of R : i in I} by A2;
hence u in 1_ R*I by Def19;
end;
now let u be set; assume u in 1_ R*I;
then u in {1_ R*i where i is Element of R : i in I } by Def19;
then ex i being Element of R st u = 1_ R*i & i in I;
hence u in I by VECTSP_1:def 19;
end;
hence thesis by A1,TARSKI:2;
end;
definition
let R be non empty LoopStr, I,J be Subset of R;
func I + J -> Subset of R equals :Def20:
{a + b where a,b is Element of R : a in I & b in J};
coherence proof set M = {a + b where a,b is Element of R : a in I & b in J};
M is Subset of R proof
per cases;
suppose A1: (I is empty) or (J is empty);
now per cases by A1;
case A2: I is empty;
M is empty proof assume M is non empty;
then reconsider M as non empty set;
consider x being Element of M;
x in {a + b where a,b is Element of R : a in I & b in J};
then consider a,b being Element of R such that
A3: x = a + b & a in I & b in J;
thus thesis by A2,A3;
end;
then for u being set holds u in M implies u in the carrier of R;
hence thesis by TARSKI:def 3;
case A4: J is empty;
M is empty proof assume M is non empty;
then reconsider M as non empty set;
consider x being Element of M;
x in {a + b where a,b is Element of R : a in I & b in J};
then consider a,b being Element of R such that
A5: x = a + b & a in I & b in J;
thus thesis by A4,A5;
end;
then for u being set holds u in M implies u in the carrier of R;
hence thesis by TARSKI:def 3;
end;
hence thesis;
suppose A6: I is non empty & J is non empty;
then reconsider I as non empty set;
reconsider J as non empty set by A6;
consider x' being Element of I;
consider y' being Element of J;
x' in I & y' in J;
then reconsider x = x',y = y' as Element of R;
x+y in {a + b where a,b is Element of R : a in I & b in J};
then reconsider M as non empty set;
for x being set holds x in M implies x in the carrier of R proof
let x be set; assume x in M; then consider a,b being Element of R
such that A7: x = a + b & a in I & b in J;
thus thesis by A7;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis;
end;
end;
definition
let R be non empty LoopStr, I,J be non empty Subset of R;
cluster I + J -> non empty;
coherence proof
{x + y where x,y is Element of R : x in I & y in J} is non empty
proof
consider x being Element of I;
consider y being Element of J;
x+y in {a + b where a,b is Element of R : a in I & b in J};
hence thesis;
end;
hence thesis by Def20;
end;
end;
definition
let R be Abelian (non empty LoopStr), I,J be Subset of R;
redefine func I + J;
commutativity proof
now let I,J be Subset of R;
A1: I+J = {a + b where a,b is Element of R : a in I & b in J} by Def20;
A2: J+I = {a + b where a,b is Element of R : a in J & b in I} by Def20;
A3: now let u be set; assume u in I+J;
then consider a,b being Element of R such that
A4: u = a + b & a in I & b in J by A1;
thus u in J+I by A2,A4;
end;
now let u be set; assume u in J+I;
then consider a,b being Element of R such that
A5: u = a + b & a in J & b in I by A2;
thus u in I+J by A1,A5;
end;
hence I + J = J + I by A3,TARSKI:2;
end;
hence thesis;
end;
end;
definition
let R be Abelian add-associative (non empty LoopStr),
I,J be add-closed Subset of R;
cluster I + J -> add-closed;
coherence proof set M = {a + b where a,b is Element of R : a in I & b in J};
A1: M = I + J by Def20;
for x,y being Element of R st x in M & y in M holds x+y in
M proof
let x,y be Element of R;
assume A2: x in M & y in M; then consider a',b' being Element of R such
that
A3: x = a' + b' & a' in I & b' in J;
consider c,d being Element of R such that
A4: y = c + d & c in I & d in J by A2;
A5: a' + c in I & b' + d in J by A3,A4,Def1;
(a' + c) + (b' + d) = ((a' + c) + b') + d by RLVECT_1:def 6
.= (c + x) + d by A3,RLVECT_1:def 6
.= x + y by A4,RLVECT_1:def 6;
hence thesis by A5;
end;
hence thesis by A1,Def1;
end;
end;
definition
let R be left-distributive (non empty doubleLoopStr),
I,J be right-ideal Subset of R;
cluster I + J -> right-ideal;
coherence proof set M = {a + b where a,b is Element of R : a in I & b in J};
A1: M = I + J by Def20;
for y,x being Element of R st x in M holds x*y in M proof
let y,x be Element of R; assume x in M;
then consider a',b' being Element of R such that
A2: x = a' + b' & a' in I & b' in J;
A3: a'*y in I & b'*y in J by A2,Def3;
(a'*y) + (b'*y) = x*y by A2,VECTSP_1:def 12;
hence thesis by A3;
end;
hence thesis by A1,Def3;
end;
end;
definition
let R be right-distributive (non empty doubleLoopStr),
I,J be left-ideal Subset of R;
cluster I + J -> left-ideal;
coherence proof set M = {a + b where a,b is Element of R : a in I & b in J};
A1: M = I + J by Def20;
for y,x being Element of R st x in M holds y*x in M proof
let y,x be Element of R; assume x in M;
then consider a',b' being Element of R such that
A2: x = a' + b' & a' in I & b' in J;
A3: y*a' in I & y*b' in J by A2,Def2;
(y*a') + (y*b') = y*x by A2,VECTSP_1:def 11;
hence thesis by A3;
end;
hence thesis by A1,Def2;
end;
end;
theorem
for R being add-associative (non empty LoopStr), I,J,K being Subset of R
holds I + (J + K) = (I + J) + K
proof let R be add-associative (non empty LoopStr), I,J,K be Subset of R;
A1: now let u be set; assume u in I + (J + K);
then u in {a + b where a,b is Element of R : a in I & b in J+K} by Def20;
then consider a,b being Element of R such that
A2: u = a + b & a in I & b in J+K;
b in {a' + b' where a',b' is Element of R : a' in J & b' in K} by A2,Def20
;
then consider c,d being Element of R such that
A3: b = c + d & c in J & d in K;
a + c in {a' + b' where a',b' is Element of R : a' in I & b' in J} by A2,
A3
;
then a + c in I + J by Def20;
then (a+ c) + d in {a' + b' where a',b' is Element of R : a' in I+J & b' in
K}by A3;
then (a + c) + d in (I + J) + K by Def20;
hence u in (I + J) + K by A2,A3,RLVECT_1:def 6;
end;
now let u be set; assume u in (I + J) + K;
then u in {a + b where a,b is Element of R : a in I+J & b in K} by Def20;
then consider a,b being Element of R such that
A4: u = a + b & a in I+J & b in K;
a in {a' + b' where a',b' is Element of R : a' in I & b' in J} by A4,Def20
;
then consider c,d being Element of R such that
A5: a = c + d & c in I & d in J;
d + b in {a' + b' where a',b' is Element of R : a' in J & b' in K} by A4,
A5
;
then d + b in J + K by Def20;
then c+(d + b) in {a' + b' where a',b' is Element of R : a' in I & b' in
J+K} by A5;
then c + (d + b) in I + (J + K) by Def20;
hence u in I + (J + K) by A4,A5,RLVECT_1:def 6;
end;
hence thesis by A1,TARSKI:2;
end;
theorem Th73:
for R being left_zeroed right_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
I,J being right-ideal (non empty Subset of R)
holds I c= I + J
proof let R be left_zeroed add-right-cancelable right_zeroed
right-distributive (non empty doubleLoopStr),
I,J be right-ideal (non empty Subset of R);
now let u be set; assume u in I; then reconsider u' = u as Element of I;
0.R is Element of J by Th3; then A1: u' + 0.R in
{a + b where a,b is Element of R : a in I & b in J};
u' + 0.R = u' by RLVECT_1:def 7;
hence u in I + J by A1,Def20;
end;
hence I c= I + J by TARSKI:def 3;
end;
theorem Th74:
for R being left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
I,J being right-ideal (non empty Subset of R)
holds J c= I + J
proof let R be left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
I,J be right-ideal (non empty Subset of R);
now let u be set; assume u in J; then reconsider u' = u as Element of J;
0.R is Element of I by Th3;
then A1: 0.R + u' in {a + b where a,b is Element of R : a in I & b in J};
0.R + u' = u' by ALGSTR_1:def 5;
hence u in I + J by A1,Def20;
end;
hence thesis by TARSKI:def 3;
end;
theorem
for R being non empty LoopStr, I,J being Subset of R,
K being add-closed Subset of R
st I c= K & J c= K holds I + J c= K
proof let R be (non empty LoopStr), I,J be Subset of R,
K being add-closed ( Subset of R);
assume A1: I c= K & J c= K;
now let u be set; assume u in I + J;
then u in {x + y where x,y is Element of R : x in I & y in J} by Def20;
then consider i,j being Element of R such that
A2: u = i + j & i in I & j in J;
thus u in K by A1,A2,Def1;
end;
hence thesis by TARSKI:def 3;
end;
theorem
for R being Abelian left_zeroed right_zeroed add-cancelable
well-unital add-associative associative
commutative distributive (non empty doubleLoopStr),
a,b being Element of R
holds {a,b}-Ideal = {a}-Ideal + {b}-Ideal
proof let R be Abelian left_zeroed right_zeroed
add-cancelable well-unital add-associative
associative commutative distributive (non empty doubleLoopStr),
a,b be Element of R;
A1: now let u be set; assume u in {a,b}-Ideal;
then u in {a*r + b*s where r,s is Element of R : not contradiction} by Th65
;
then consider r,s being Element of R such that
A2: u = a*r + b*s; a*r in {a*v where v is Element of R : not contradiction
}
;
then reconsider a' = a*r as Element of {a}-Ideal by Th64;
b*s in {b*v where v is Element of R : not contradiction};
then reconsider b' = b*s as Element of {b}-Ideal by Th64;
a' + b' in {x + y where x,y is Element of R : x in {a}-Ideal & y in
{b}-Ideal};
hence u in {a}-Ideal + {b}-Ideal by A2,Def20;
end;
now let u be set; assume u in {a}-Ideal + {b}-Ideal;
then u in {x + y where x,y is Element of R :
x in {a}-Ideal & y in {b}-Ideal} by Def20;
then consider x,y being Element of R such that
A3: u = x + y & x in {a}-Ideal & y in {b}-Ideal;
x in {a*v where v is Element of R : not contradiction} by A3,Th64;
then consider r being Element of R such that
A4: x = a*r;
y in {b*v where v is Element of R : not contradiction} by A3,Th64;
then consider s being Element of R such that A5: y = b*s;
u in {a*v + b*d where v,d is Element of R : not contradiction} by A3,A4,A5
;
hence u in {a,b}-Ideal by Th65;
end;
hence thesis by A1,TARSKI:2;
end;
definition
let R be non empty 1-sorted, I,J be Subset of R;
func I /\ J -> Subset of R equals :Def21:
{ x where x is Element of R : x in I & x in J };
coherence proof set M = { x where x is Element of R : x in I & x in J };
now let u be set; assume u in M; then consider x being Element of R such
that
A1: u = x & x in I & x in J;
thus u in the carrier of R by A1;
end;
then reconsider M as Subset of R by TARSKI:def 3;
M is Subset of R;
hence thesis;
end;
end;
definition
let R be right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr),
I,J be left-ideal (non empty Subset of R);
cluster I /\ J -> non empty;
coherence proof 0.R in I & 0.R in J by Th2;
then 0.R in { x where x is Element of R : x in I & x in J };
hence thesis by Def21;
end;
end;
definition
let R be non empty LoopStr, I,J be add-closed Subset of R;
cluster I /\ J -> add-closed;
coherence proof set M = { x where x is Element of R : x in I & x in J };
A1: M = I /\ J by Def21;
then reconsider M as Subset of R;
for x,y being Element of R st x in M & y in M holds x+y in
M proof
let x,y be Element of R; assume A2: x in M & y in M;
then consider a being Element of R such that A3: x = a & a in I & a in J;
consider c being Element of R such that A4: c = y & c in I & c in J by A2;
a + c in I & a + c in J by A3,A4,Def1;
hence thesis by A3,A4;
end;
hence thesis by A1,Def1;
end;
end;
definition
let R be non empty multLoopStr, I,J be left-ideal Subset of R;
cluster I /\ J -> left-ideal;
coherence proof set M = { x where x is Element of R : x in I & x in J };
A1: M = I /\ J by Def21;
then reconsider M as Subset of R;
for y,x being Element of R st x in M holds y*x in M proof
let y,x be Element of R; assume x in M;
then consider a being Element of R such that
A2: x = a & a in I & a in J; y*a in I & y*a in J by A2,Def2;
hence thesis by A2;
end;
hence thesis by A1,Def2;
end;
end;
definition
let R be non empty multLoopStr, I,J be right-ideal Subset of R;
cluster I /\ J -> right-ideal;
coherence proof set M = { x where x is Element of R : x in I & x in J };
A1: M = I /\ J by Def21; then reconsider M as Subset of R;
for y,x being Element of R st x in M holds x*y in M proof
let y,x be Element of R; assume x in M;
then consider a being Element of R such that
A2: x = a & a in I & a in J; a*y in I & a*y in J by A2,Def3;
hence thesis by A2;
end;
hence thesis by A1,Def3;
end;
end;
theorem Th77:
for R being non empty 1-sorted, I,J being Subset of R
holds I /\ J c= I & I /\ J c= J
proof let R be non empty 1-sorted, I,J be Subset of R;
now let u be set; assume u in I /\ J;
then u in {x where x is Element of R : x in I & x in J} by Def21;
then consider a being Element of R such that
A1: u = a & a in I & a in J;
thus u in I by A1;
end;
hence I /\ J c= I by TARSKI:def 3;
now let u be set; assume u in I /\ J;
then u in {x where x is Element of R : x in I & x in J} by Def21;
then consider a being Element of R such that
A2: u = a & a in I & a in J;
thus u in J by A2;
end;
hence I /\ J c= J by TARSKI:def 3;
end;
theorem
for R being non empty 1-sorted, I,J,K being Subset of R
holds I /\ (J /\ K) = (I /\ J) /\ K
proof let R be non empty 1-sorted, I,J,K be Subset of R;
A1: now let u be set; assume u in I /\ (J /\ K);
then u in {x where x is Element of R : x in I & x in (J /\ K)} by Def21;
then consider a being Element of R such that
A2: u = a & a in I & a in J/\K;
a in {x where x is Element of R : x in J & x in K} by A2,Def21;
then consider b being Element of R such that
A3: b = a & b in J & b in K;
a in {x where x is Element of R : x in I & x in J} by A2,A3;
then a in (I /\ J) by Def21;
then a in {x where x is Element of R : x in (I /\ J) & x in K} by A3;
hence u in (I /\ J) /\ K by A2,Def21;
end;
now let u be set; assume u in (I /\ J) /\ K;
then u in {x where x is Element of R : x in (I /\ J) & x in K} by Def21;
then consider a being Element of R such that
A4: u = a & a in (I /\ J) & a in K;
a in {x where x is Element of R : x in I & x in J} by A4,Def21;
then consider b being Element of R such that
A5: b = a & b in I & b in J;
a in {x where x is Element of R : x in J & x in K} by A4,A5;
then a in (J /\ K) by Def21;
then a in {x where x is Element of R : x in I & x in (J /\ K)} by A5;
hence u in I /\ (J /\ K) by A4,Def21;
end;
hence thesis by A1,TARSKI:2;
end;
theorem
for R being non empty 1-sorted, I,J,K being Subset of R
st K c= I & K c= J holds K c= I /\ J
proof let R be non empty 1-sorted, I,J,K be Subset of R;
assume A1: K c= I & K c= J;
now let u be set; assume
A2: u in K;
then reconsider u' = u as Element of R;
u' in {x where x is Element of R : x in I & x in J} by A1,A2;
hence u in (I /\ J) by Def21;
end;
hence thesis by TARSKI:def 3;
end;
theorem
for R being Abelian left_zeroed right_zeroed right_complementable left_unital
add-associative left-distributive (non empty doubleLoopStr),
I being add-closed left-ideal (non empty Subset of R),
J being Subset of R, K being non empty Subset of R
st J c= I holds I /\ (J + K) = J + (I /\ K)
proof
let R be Abelian left_zeroed right_zeroed right_complementable left_unital
add-associative left-distributive (non empty doubleLoopStr),
I be add-closed left-ideal (non empty Subset of R),
J be Subset of R, K be non empty Subset of R;
assume A1: J c= I;
A2: now let u be set; assume u in I /\ (J + K);
then u in {x where x is Element of R : x in I & x in J+K} by Def21;
then consider v being Element of R such that
A3: u = v & v in I & v in J + K;
v in {x + y where x,y is Element of R : x in J & y in K} by A3,Def20;
then consider j,k being Element of R such that
A4: v = j + k & j in J & k in K; reconsider j' = j as Element of I by A1,A4;
-j' in I by Th13; then (j' + k) + -j' in I by A3,A4,Def1;
then (j' + -j') + k in I by RLVECT_1:def 6; then 0.R + k in
I by RLVECT_1:16;
then k in I by ALGSTR_1:def 5;
then k in {x where x is Element of R : x in I & x in K} by A4;
then k in (I /\ K) by Def21;
then u in {x+y where x,y is Element of R : x in J & y in (I /\ K)} by A3,A4
;
hence u in J + (I /\ K) by Def20;
end;
now let u be set; assume u in J + (I /\ K);
then u in {x + y where x,y is Element of R: x in J & y in (I /\
K)} by Def20;
then consider j,ik being Element of R
such that A5: u = j + ik & j in J & ik in (I /\ K);
ik in {x where x is Element of R : x in I & x in K} by A5,Def21;
then consider z being Element of R such that A6: z = ik & z in I & z in K;
reconsider i' = ik as Element of I by A6;
reconsider k' = ik as Element of K by A6;
reconsider j' = j as Element of I by A1,A5; u = j' + i' by A5;
then A7: u in I by Def1; u = j + k' by A5;
then u in {x + y where x,y is Element of R: x in J & y in K} by A5;
then u in J + K by Def20;
then u in {x where x is Element of R : x in I & x in J+K} by A7;
hence u in I /\ (J + K) by Def21;
end;
hence thesis by A2,TARSKI:2;
end;
definition
let R be non empty doubleLoopStr, I,J be Subset of R;
func I *' J -> Subset of R equals :Def22:
{ Sum s where s is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J};
coherence proof set M = {Sum s where s is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J};
now let u be set; assume u in M;
then consider s being FinSequence of the carrier of R such that
A1: u = Sum s &
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J;
thus u in the carrier of R by A1;
end;
then reconsider M as Subset of R by TARSKI:def 3;
M is Subset of R;
hence thesis;
end;
end;
definition
let R be non empty doubleLoopStr, I,J be Subset of R;
cluster I *' J -> non empty;
coherence proof set M = {Sum s where s is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J};
M is non empty proof set p = <*>(the carrier of R);
for i being Nat st 1 <= i & i <= len p
ex a,b being Element of R st p.i = a*b & a in I & b in J proof
let i be Nat; assume A1: 1 <= i & i <= len p; len p = 0 by FINSEQ_1:32;
hence thesis by A1,AXIOMS:22;
end; then Sum p in M;
hence thesis;
end;
hence thesis by Def22;
end;
end;
definition
let R be commutative (non empty doubleLoopStr), I,J be Subset of R;
redefine func I *' J;
commutativity proof
now let I,J be Subset of R;
A1: I*'J = {Sum s where s is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J} by Def22;
A2: J*'I = {Sum s where s is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in J & b in I} by Def22;
A3: now let u be set; assume u in I*'J;
then consider s being FinSequence of the carrier of R such that
A4: u = Sum s &
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J by A1;
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in J & b in I proof
let i be Nat; assume 1 <= i & i <= len s;
then consider a,b being Element of R such that
A5: s.i = a*b & a in I & b in J by A4;
thus thesis by A5;
end;
hence u in J*'I by A2,A4;
end;
now let u be set; assume u in J*'I;
then consider s being FinSequence of the carrier of R such that
A6: u = Sum s & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in J & b in I by A2;
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J proof
let i be Nat; assume 1 <= i & i <= len s;
then consider a,b being Element of R such that
A7: s.i = a*b & a in J & b in I by A6;
thus thesis by A7;
end;
hence u in I*'J by A1,A6;
end;
hence I *' J = J *' I by A3,TARSKI:2;
end;
hence thesis;
end;
end;
definition
let R be right_zeroed add-associative (non empty doubleLoopStr),
I,J be Subset of R;
cluster I *' J -> add-closed;
coherence proof set M = {Sum s where s is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J};
A1: M = I *' J by Def22;
then reconsider M as non empty Subset of R;
for x,y being Element of R st x in M & y in M holds x+y in
M proof
let x,y be Element of R; assume A2: x in M & y in M;
then consider s being FinSequence of the carrier of R such that
A3: x = Sum s & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J;
consider t being FinSequence of the carrier of R such that
A4: y = Sum t & for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I & b in J by A2;
set q = s^t;
A5: Sum q = x + y by A3,A4,RLVECT_1:58;
now let i be Nat; assume A6: 1 <= i & i <= len q;
thus ex a,r being Element of R st q.i = a*r & a in I & r in J proof
per cases;
suppose A7: i <= len s;
then i in Seg(len s) by A6,FINSEQ_1:3;
then i in dom s by FINSEQ_1:def 3;
then q.i = s.i by FINSEQ_1:def 7;
hence thesis by A3,A6,A7;
suppose A8: len s < i;
then reconsider j = i - len s as Nat by INT_1:18;
len s - len s < j by A8,REAL_1:54
; then 0 < j by XCMPLX_1:14;
then A9: 1 <= j by RLVECT_1:99;
i <= len s + len t by A6,FINSEQ_1:35;
then j <= (len s + len t) - len s by REAL_1:49;
then j <= (len s + len t) + -len s by XCMPLX_0:def 8;
then j <= len t + (len s + -len s) by XCMPLX_1:1;
then j <= len t + (len s - len s) by XCMPLX_0:def 8;
then A10: j <= len t + 0 by XCMPLX_1:14;
t.j = q.i by A6,A8,FINSEQ_1:37;
hence thesis by A4,A9,A10;
end;
end;
hence thesis by A5;
end;
hence thesis by A1,Def1;
end;
end;
definition
let R be right_zeroed add-left-cancelable associative
left-distributive (non empty doubleLoopStr),
I,J be right-ideal Subset of R;
cluster I *' J -> right-ideal;
coherence proof set M = {Sum s where s is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J};
A1: M = I *' J by Def22; then reconsider M as non empty Subset of R;
for y,x being Element of R st x in M holds x*y in M proof
let y,x be Element of R; assume x in M;
then consider s being FinSequence of the carrier of R such that
A2: x = Sum s & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J;
set q = s*y;
A3: Sum q = Sum s*y by BINOM:5;
A4: Seg(len q) = dom q by FINSEQ_1:def 3 .= dom s by POLYNOM1:def 3
.= Seg(len s) by FINSEQ_1:def 3;
then A5: len q = len s by FINSEQ_1:8;
now let i be Nat; assume A6: 1 <= i & i <= len q;
then consider c,r' being Element of R such that
A7: s.i = c*r' & c in I & r' in J by A2,A5;
i in Seg(len s) & i in Seg(len q) by A4,A6,FINSEQ_1:3;
then A8: i in dom s & i in dom q by FINSEQ_1:def 3;
then A9: s/.i = c*r' by A7,FINSEQ_4:def 4;
A10: q.i = q/.i by A8,FINSEQ_4:def 4 .= (c*r')*y by A8,A9,POLYNOM1:def
3 .= c*(r'*y) by VECTSP_1:def 16;
thus ex b,r being Element of R st q.i = b*r & b in I & r in J proof
take c,r'*y;
thus thesis by A7,A10,Def3;
end;
end;
hence thesis by A2,A3;
end;
hence thesis by A1,Def3;
end;
end;
definition
let R be left_zeroed add-right-cancelable associative
right-distributive (non empty doubleLoopStr),
I,J be left-ideal Subset of R;
cluster I *' J -> left-ideal;
coherence proof set M = {Sum s where s is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J};
A1: M = I *' J by Def22;
then reconsider M as non empty Subset of R;
for y,x being Element of R st x in M holds y*x in M proof
let y,x be Element of R; assume x in M;
then consider s being FinSequence of the carrier of R such that
A2: x = Sum s & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J;
set q = y*s;
A3: Sum q = y*Sum s by BINOM:4;
A4: Seg(len q) = dom q by FINSEQ_1:def 3 .= dom s by POLYNOM1:def 2
.= Seg(len s) by FINSEQ_1:def 3;
then A5: len q = len s by FINSEQ_1:8;
now let i be Nat; assume A6: 1 <= i & i <= len q;
then consider c,r' being Element of R such that
A7: s.i = c*r' & c in I & r' in J by A2,A5;
i in Seg(len s) & i in Seg(len q) by A4,A6,FINSEQ_1:3;
then A8: i in dom s & i in dom q by FINSEQ_1:def 3;
then A9: s/.i = c*r' by A7,FINSEQ_4:def 4;
A10: q.i = q/.i by A8,FINSEQ_4:def 4 .= y*(c*r') by A8,A9,POLYNOM1:def
2 .= (y*c)*r' by VECTSP_1:def 16;
thus ex b,r being Element of R st q.i = b*r & b in I & r in J proof
take y*c,r';
thus thesis by A7,A10,Def2;
end;
end;
hence thesis by A2,A3;
end;
hence thesis by A1,Def2;
end;
end;
theorem
for R being left_zeroed right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr),
I being non empty Subset of R
holds {0.R} *' I = {0.R}
proof let R be left_zeroed right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr), I be non empty Subset of R;
A1: now let u be set; assume A2: u in {0.R}; consider a being Element of I;
set q = <* 0.R*a *>;
A3: Sum q = 0.R*a by BINOM:3 .= 0.R by BINOM:1 .= u by A2,TARSKI:def 1;
A4: len q = 1 & q.1 = 0.R*a by FINSEQ_1:57;
reconsider o = 0.R as Element of {0.R} by TARSKI:def 1;
for i being Nat st 1 <= i & i <= len q holds
ex b,r being Element of R st q.i = b*r & b in {0.R} & r in I proof
let i be Nat; assume 1 <= i & i <= len q;
then q.i = o*a by A4,AXIOMS:21;
hence thesis;
end;
then u in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in {0.R} & b in I} by A3;
hence u in {0.R} *' I by Def22;
end;
now let u be set; assume u in ({0.R}) *' I;
then u in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in {0.R} & b in
I} by Def22;
then consider s being FinSequence of the carrier of R such that
A5: Sum s = u & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in {0.R} & b in I;
now per cases;
case len s = 0; then s = <*>(the carrier of R) by FINSEQ_1:32;
hence Sum s = 0.R by RLVECT_1:60;
case len s <> 0; then 1 <= len s by RLVECT_1:99;
then 1 in Seg(len s) by FINSEQ_1:3;
then A6: 1 in dom s by FINSEQ_1:def 3;
A7: for i being Nat st i in dom s holds s/.i = 0.R proof
let i be Nat; assume A8: i in dom s;
then i in Seg(len s) by FINSEQ_1:def 3;
then 1 <= i & i <= len s by FINSEQ_1:3;
then consider a ,b being Element of R such that
A9: s.i = a*b & a in {0.R} & b in I by A5;
A10: s/.i = a*b by A8,A9,FINSEQ_4:def 4;
a = 0.R by A9,TARSKI:def 1;
hence thesis by A10,BINOM:1;
end;
then for i being Nat st i in dom s & i <> 1 holds s/.i = 0.R;
hence Sum s = s/.1 by A6,POLYNOM2:5 .= 0.R by A6,A7;
end;
hence u in {0.R} by A5,TARSKI:def 1;
end;
hence ({0.R}) *' I = {0.R} by A1,TARSKI:2;
end;
theorem Th82:
for R being left_zeroed right_zeroed add-cancelable
distributive (non empty doubleLoopStr),
I being add-closed right-ideal (non empty Subset of R),
J being add-closed left-ideal (non empty Subset of R)
holds I *' J c= I /\ J
proof let R be left_zeroed right_zeroed add-cancelable
distributive (non empty doubleLoopStr),
I be add-closed right-ideal (non empty Subset of R),
J be add-closed left-ideal (non empty Subset of R);
now let u be set; assume u in I *' J;
then u in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I & b in J} by Def22;
then consider s being FinSequence of the carrier of R such that
A1: Sum s = u & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J;
consider f being Function of NAT,the carrier of R such that
A2: Sum s = f.(len s) & f.0 = 0.R &
for j being Nat, v being Element of R
st j < len s & v = s.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
defpred P[Nat] means f.$1 in I & f.$1 in J;
A3: P[0] by A2,Th2,Th3;
A4: now let j be Nat; assume A5: 0 <= j & j < len s;
thus P[j] implies P[j+1] proof
assume A6: f.j in I & f.j in J;
A7: j + 1 <= len s by A5,NAT_1:38;
A8: 0 + 1 <= j + 1 by A5,AXIOMS:24;
then j + 1 in Seg(len s) by A7,FINSEQ_1:3;
then j + 1 in dom s by FINSEQ_1:def 3;
then A9: s.(j+1) = s/.(j+1) by FINSEQ_4:def 4;
then A10: f.(j+1) = f.j + s/.(j+1) by A2,A5;
consider a,b being Element of R such that
A11: s.(j+1) = a*b & a in I & b in J by A1,A7,A8;
s/.(j+1) in I & s/.(j+1) in J by A9,A11,Def2,Def3;
hence thesis by A6,A10,Def1;
end;
end;
A12: for j being Nat st 0 <= j & j <= len s holds P[j]
from FinInd(A3,A4); 0 <= len s by NAT_1:18;
then Sum s in I & Sum s in J by A2,A12;
then Sum s in {z where z is Element of R : z in I & z in J};
hence u in I /\ J by A1,Def21;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th83:
for R being Abelian left_zeroed right_zeroed add-cancelable add-associative
associative distributive (non empty doubleLoopStr),
I,J,K being right-ideal (non empty Subset of R)
holds I *' (J + K) = (I *' J) + (I *' K)
proof let R be Abelian left_zeroed right_zeroed add-cancelable add-associative
associative distributive (non empty doubleLoopStr),
I,J,K be right-ideal (non empty Subset of R);
A1: now let u be set; assume u in I *' (J + K);
then u in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I & b in
J+K} by Def22;
then consider s being FinSequence of the carrier of R such that
A2: Sum s = u & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J+K;
consider f being Function of NAT,the carrier of R such that
A3: Sum s = f.(len s) & f.0 = 0.R &
for j being Nat,v being Element of R
st j < len s & v = s.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
defpred P[Nat] means
ex x,y being Element of R st f.$1=x+y & x in I*'J & y in I*'K;
A4: P[0] proof
take 0.R,0.R;
thus thesis by A3,Th3,RLVECT_1:def 7;
end;
A5: now let n be Nat; assume A6: 0 <= n & n < len s;
thus P[n] implies P[n+1]
proof
assume ex x,y being Element of R st f.n = x+y & x in I*'J & y in I*'K;
then consider x,y being Element of R such that
A7: f.n = x+y & x in I*'J & y in I*'K;
x in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I & b in
J} by A7,Def22
;
then consider q being FinSequence of the carrier of R such that
A8: Sum q = x & for i being Nat st 1 <= i & i <= len q
ex a,b being Element of R st q.i = a*b & a in I & b in J;
y in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I & b in K} by A7,
Def22;
then consider p being FinSequence of the carrier of R such that
A9: Sum p = y & for i being Nat st 1 <= i & i <= len p
ex a,b being Element of R st p.i = a*b & a in I & b in K;
A10: 0 + 1 <= n + 1 by A6,AXIOMS:24;
A11: n + 1 <= len s by A6,NAT_1:38;
then n + 1 in Seg(len s) by A10,FINSEQ_1:3;
then A12: n + 1 in dom s by FINSEQ_1:def 3;
then A13: s.(n+1) = s/.(n+1) by FINSEQ_4:def 4;
consider a,b being Element of R such that
A14: s.(n+1) = a*b & a in I & b in J+K by A2,A10,A11;
b in {a'+b' where a',b' is Element of R : a' in J & b' in
K} by A14,Def20;
then consider c,d being Element of R such that
A15: b = c + d & c in J & d in K;
A16: s/.(n+1) = a*(c + d) by A12,A14,A15,FINSEQ_4:def 4 .= a*c + a*d
by VECTSP_1:def 18;
set q1 = q^<*a*c*>, p1 = p^<*a*d*>;
A17: len q1 = len q + len(<*a*c*>) by FINSEQ_1:35
.= len q + 1 by FINSEQ_1:57;
for i being Nat st 1 <= i & i <= len q1
ex a,b being Element of R st q1.i = a*b & a in I & b in J proof
let i be Nat; assume A18: 1 <= i & i <= len q1;
per cases;
suppose i = len q1; then q1.i = a*c by A17,FINSEQ_1:59;
hence thesis by A14,A15;
suppose i <> len q1; then i < len q1 by A18,REAL_1:def 5;
then A19: i <= len q by A17,NAT_1:38;
then i in Seg(len q) by A18,FINSEQ_1:3;
then A20: i in dom q by FINSEQ_1:def 3;
consider a,b being Element of R such that
A21: q.i = a*b & a in I & b in J by A8,A18,A19;
q1.i = a*b by A20,A21,FINSEQ_1:def 7;
hence thesis by A21;
end;
then Sum q1 in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I & b in J};
then A22: Sum q1 in I *' J by Def22;
A23: len p1 = len p + len(<*a*d*>) by FINSEQ_1:35
.= len p + 1 by FINSEQ_1:57;
for i being Nat st 1 <= i & i <= len p1
ex a,b being Element of R st p1.i = a*b & a in I & b in K proof
let i be Nat; assume A24: 1 <= i & i <= len p1;
per cases;
suppose i = len p1; then p1.i = a*d by A23,FINSEQ_1:59;
hence thesis by A14,A15;
suppose i <> len p1; then i < len p1 by A24,REAL_1:def 5;
then A25: i <= len p by A23,NAT_1:38;
then i in Seg(len p) by A24,FINSEQ_1:3;
then A26: i in dom p by FINSEQ_1:def 3;
consider a,b being Element of R such that
A27: p.i = a*b & a in I & b in K by A9,A24,A25;
p1.i = a*b by A26,A27,FINSEQ_1:def 7;
hence thesis by A27;
end;
then Sum p1 in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I & b in K};
then A28: Sum p1 in I *' K by Def22;
Sum q1 + Sum p1 = (Sum q + Sum <*a*c*>) + Sum p1 by RLVECT_1:58
.= (Sum q + a*c) + Sum p1 by BINOM:3
.= (Sum q + a*c) + (Sum p + Sum <*a*d*>) by RLVECT_1:58
.= (Sum q + a*c) + (Sum p + a*d) by BINOM:3
.= ((Sum q + a*c) + Sum p) + a*d by RLVECT_1:def 6
.= (a*c + (Sum q + Sum p)) + a*d by RLVECT_1:def 6
.= f.n + (a*c + a*d) by A7,A8,A9,RLVECT_1:def 6
.= f.(n+1) by A3,A6,A13,A16;
hence thesis by A22,A28;
end;
end;
A29: for n being Nat st 0 <= n &n <= len s holds P[n]
from FinInd(A4,A5);
0 <= len s by NAT_1:18;
then ex x,y being Element of R st Sum s = x+y & x in I*'J & y in I*'K by A3,
A29;
then u in {a+b where a,b is Element of R : a in I*'J & b in I*'K} by A2;
hence u in (I *' J) + (I *' K) by Def20;
end;
now let u be set; assume u in (I *' J) + (I *' K);
then u in {a+b where a,b is Element of R: a in I*'J & b in I*'K} by Def20;
then consider a,b being Element of R such that
A30: u = a + b & a in I*'J & b in I*'K;
a in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I & b in J} by A30,Def22;
then consider q being FinSequence of the carrier of R such that
A31: a = Sum q & for i being Nat st 1 <= i & i <= len q
ex a,b being Element of R st q.i = a*b & a in I & b in J;
b in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I & b in K} by A30,Def22;
then consider p being FinSequence of the carrier of R such that
A32: b = Sum p & for i being Nat st 1 <= i & i <= len p
ex a,b being Element of R st p.i = a*b & a in I & b in K;
set s = p^q;
A33: for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J+K proof
let i be Nat; assume A34: 1 <= i & i <= len s;
then i in Seg(len s) by FINSEQ_1:3; then A35: i in dom s by FINSEQ_1:def 3
;
now per cases;
case A36: i <= len p; then i in Seg(len p) by A34,FINSEQ_1:3;
then A37: i in dom p by FINSEQ_1:def 3;
consider a,b being Element of R such that
A38: p.i = a*b & a in I & b in K by A32,A34,A36;
0.R in J by Th3;
then 0.R + b in {a'+b' where a',b' is Element of R:a' in J & b' in
K} by A38
;
then A39: 0.R + b in J + K by Def20;
s.i=a*b by A37,A38,FINSEQ_1:def 7
.=a*(0.R + b) by ALGSTR_1:def 5;
hence thesis by A38,A39;
case i > len p; then not(i in Seg(len p)) by FINSEQ_1:3;
then not(i in dom p) by FINSEQ_1:def 3;
then consider n being Nat such that
A40: n in dom q & i = len p + n by A35,FINSEQ_1:38;
n in Seg(len q) by A40,FINSEQ_1:def 3;
then 1 <= n & n <= len q by FINSEQ_1:3;
then consider a,b being Element of R such that
A41: q.n = a*b & a in I & b in J by A31;
0.R in K by Th3;
then b + 0.R in {a'+b' where a',b' is Element of R:a' in J & b' in
K} by A41
;
then A42: b + 0.R in J + K by Def20;
s.i = q.n by A40,FINSEQ_1:def 7 .= a*(b + 0.R) by A41,RLVECT_1:def 7;
hence thesis by A41,A42;
end;
hence thesis;
end;
Sum s = u by A30,A31,A32,RLVECT_1:58;
then u in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I & b in J+K} by A33;
hence u in I *' (J + K) by Def22;
end;
hence thesis by A1,TARSKI:2;
end;
theorem Th84:
for R being Abelian left_zeroed right_zeroed add-cancelable add-associative
commutative associative distributive (non empty doubleLoopStr),
I,J being right-ideal (non empty Subset of R)
holds (I + J) *' (I /\ J) c= I *' J
proof let R be Abelian left_zeroed right_zeroed add-cancelable add-associative
commutative associative distributive (non empty doubleLoopStr),
I,J be right-ideal (non empty Subset of R);
A1: (I + J) *' (I /\ J) = (I *' (I /\ J)) + (J *' (I /\ J)) by Th83;
now let u be set; assume u in (I *' (I /\ J)) + (J *' (I /\ J));
then u in {a + b where a,b is Element of R :
a in (I *' (I /\ J)) & b in (J *' (I /\ J))} by Def20;
then consider a,b being Element of R such that
A2: u = a + b & a in (I *' (I /\ J)) & b in (J *' (I /\ J));
a in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I & b in (I /\ J)} by A2,
Def22;
then consider q being FinSequence of the carrier of R such that
A3: a = Sum q & for i being Nat st 1 <= i & i <= len q
ex a,b being Element of R st q.i = a*b & a in I & b in (I /\ J);
for i being Nat st 1 <= i & i <= len q
ex x,y being Element of R st q.i = x*y & x in I & y in J proof
let i be Nat; assume 1 <= i & i <= len q;
then consider x,y being Element of R such that
A4: q.i = x*y & x in I & y in (I /\ J) by A3; I /\ J c= J by Th77;
hence thesis by A4;
end;
then A5: Sum q in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R
st t.i = a*b & a in I & b in J};
b in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in J & b in (I /\ J)} by A2,
Def22;
then consider s being FinSequence of the carrier of R such that
A6: b = Sum s & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in J & b in (I /\
J);
for i being Nat st 1 <= i & i <= len s
ex x,y being Element of R st s.i = x*y & x in I & y in J proof
let i be Nat; assume 1 <= i & i <= len s;
then consider x,y being Element of R such that
A7: s.i = x*y & x in J & y in (I /\ J) by A6; I /\ J c= I by Th77;
hence thesis by A7;
end;
then Sum s in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I & b in J};
then a in I *' J & b in I *' J by A3,A5,A6,Def22;
hence u in I *' J by A2,Def1;
end;
hence thesis by A1,TARSKI:def 3;
end;
theorem
for R being right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr),
I,J being add-closed left-ideal (non empty Subset of R)
holds (I + J) *' (I /\ J) c= I /\ J
proof let R be right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr),
I,J be add-closed left-ideal (non empty Subset of R);
now let u be set; assume u in (I + J) *' (I /\ J);
then u in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I+J & b in I/\J} by Def22;
then consider s being FinSequence of the carrier of R such that
A1: u = Sum s & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I+J & b in I/\J;
consider f being Function of NAT,the carrier of R such that
A2: Sum s = f.(len s) & f.0 = 0.R &
for j being Nat,v being Element of R
st j < len s & v = s.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
defpred P[Nat] means f.$1 in I/\J; f.0 in I & f.0 in J by A2,Th2;
then f.0 in {t where t is Element of R : t in I & t in J};
then A3: P[0] by Def21;
A4: now let n be Nat; assume A5: 0 <= n & n < len s;
thus P[n] implies P[n+1] proof
assume A6: f.n in I /\ J;
A7: 0 + 1 <= n + 1 by A5,AXIOMS:24;
A8: n + 1 <= len s by A5,NAT_1:38;
then n + 1 in Seg(len s) by A7,FINSEQ_1:3;
then A9: n + 1 in dom s by FINSEQ_1:def 3;
consider x,y being Element of R such that
A10: s.(n+1) = x*y & x in I+J & y in I/\J by A1,A7,A8;
A11: s.(n+1) = s/.(n+1) by A9,FINSEQ_4:def 4;
then s/.(n+1) in I /\ J by A10,Def2;
then f.n + s/.(n+1) in I /\ J by A6,Def1;
hence thesis by A2,A5,A11;
end;
end;
A12: for n being Nat st 0 <= n &n <= len s holds P[n] from FinInd(A3,A4);
0 <= len s by NAT_1:18;
hence u in I /\ J by A1,A2,A12;
end;
hence thesis by TARSKI:def 3;
end;
definition
let R be non empty LoopStr, I,J be Subset of R;
pred I,J are_co-prime means :Def23:
I + J = the carrier of R;
end;
theorem Th86:
for R being left_zeroed left_unital (non empty doubleLoopStr),
I,J being non empty Subset of R
st I,J are_co-prime holds I /\ J c= (I + J) *' (I /\ J)
proof let R be left_zeroed left_unital (non empty doubleLoopStr),
I,J be non empty Subset of R;
assume I,J are_co-prime; then A1: I + J = the carrier of R by Def23;
now let u be set; assume A2: u in I /\ J;
then u in {g where g is Element of R : g in I & g in J} by Def21;
then consider g being Element of R such that
A3: u = g & g in I & g in J;
reconsider u' = u as Element of R by A3; set q = <*1_ R*u'*>;
A4: len q = 1 by FINSEQ_1:56;
A5: for i being Nat st 1 <= i & i <= len q
ex x,y being Element of R st q.i = x*y & x in I+J & y in I/\J
proof
let i be Nat; assume 1 <= i & i <= len q;
then A6: i = 1 by A4,AXIOMS:21;
take 1_ R,u';
thus thesis by A1,A2,A6,FINSEQ_1:57;
end;
Sum q = 1_ R*u' by BINOM:3 .= u' by VECTSP_1:def 19;
then u' in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I+J & b in I/\J} by A5;
hence u in (I + J) *' (I /\ J) by Def22;
end;
hence thesis by TARSKI:def 3;
end;
theorem
for R being Abelian left_zeroed right_zeroed add-cancelable
add-associative left_unital commutative associative
distributive (non empty doubleLoopStr),
I being add-closed left-ideal right-ideal (non empty Subset of R),
J being add-closed left-ideal (non empty Subset of R)
st I,J are_co-prime holds I *' J = I /\ J
proof let R be left_zeroed right_zeroed add-cancelable add-associative
Abelian commutative associative distributive
left_unital (non empty doubleLoopStr),
I be add-closed left-ideal right-ideal (non empty Subset of R),
J be add-closed left-ideal (non empty Subset of R);
assume A1: I,J are_co-prime;
A2: (I + J) *' (I /\ J) c= I *' J by Th84; I /\ J c= (I + J) *' (I /\
J) by A1,Th86;
then A3: I /\ J c= I *' J by A2,XBOOLE_1:1; I *' J c= I /\ J by Th82;
hence thesis by A3,XBOOLE_0:def 10;
end;
definition
let R be non empty HGrStr, I,J be Subset of R;
func I % J -> Subset of R equals :Def24:
{a where a is Element of R: a*J c= I};
coherence proof set M = {a where a is Element of R: a*J c= I};
M is Subset of R proof
for x being set holds x in M implies x in the carrier of R proof
let x be set; assume x in M;
then consider a being Element of R such that A1: x = a & a*J c= I;
thus thesis by A1;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis;
end;
end;
definition
let R be right_zeroed add-left-cancelable left-distributive
(non empty doubleLoopStr),
I,J be left-ideal (non empty Subset of R);
cluster I % J -> non empty;
coherence proof set M = {a where a is Element of R: a*J c= I};
M is non empty Subset of R proof
A1: 0.R*J = {0.R} by Th70; 0.R in I & 0.R in J by Th2;
then for u being set holds u in {0.R} implies u in I by TARSKI:def 1;
then {0.R} c= I by TARSKI:def 3; then A2: 0.R in M by A1;
for x being set holds x in M implies x in the carrier of R proof
let x be set; assume x in M;
then consider a being Element of R such that A3: x = a & a*J c= I;
thus thesis by A3;
end;
hence thesis by A2,TARSKI:def 3;
end;
hence thesis by Def24;
end;
end;
definition
let R be right_zeroed add-left-cancelable left-distributive
(non empty doubleLoopStr),
I,J be add-closed left-ideal (non empty Subset of R);
cluster I % J -> add-closed;
coherence proof set M = {a where a is Element of R: a*J c= I};
A1: M = I % J by Def24;
then reconsider M as non empty Subset of R;
for x,y being Element of R st x in M & y in M holds x+y in
M proof
let x,y be Element of R;
assume A2: x in M & y in M;
then consider a being Element of R such that A3: x = a & a*J c= I;
consider b being Element of R such that A4: y = b & b*J c= I by A2;
now let u be set; assume u in (a+b)*J;
then u in {(a+b)*i where i is Element of R : i in J} by Def19;
then consider c being Element of R such that
A5: u = (a + b)*c & c in J;
A6: u = a*c + b*c by A5,VECTSP_1:def 12;
a*c in {a*i where i is Element of R : i in J} by A5;
then A7: a*c in a*J by Def19;
b*c in {b*i where i is Element of R : i in J} by A5;
then b*c in b*J by Def19;
hence u in I by A3,A4,A6,A7,Def1;
end;
then (a+b)*J c= I by TARSKI:def 3;
hence thesis by A3,A4;
end;
hence thesis by A1,Def1;
end;
end;
definition
let R be right_zeroed add-left-cancelable left-distributive
associative commutative (non empty doubleLoopStr),
I,J be left-ideal (non empty Subset of R);
cluster I % J -> left-ideal;
coherence proof set M = {a where a is Element of R: a*J c= I};
A1: M = I % J by Def24; then reconsider M as non empty Subset of R;
for y,x being Element of R st x in M holds y*x in M proof
let y,x be Element of R;
assume x in M;
then consider a being Element of R such that A2: x = a & a*J c= I;
now let u be set; assume u in (y*a)*J;
then u in {(y*a)*i where i is Element of R : i in J} by Def19;
then consider c being Element of R such that
A3: u = (y*a)*c & c in J;
A4: u = a*(y*c) by A3,VECTSP_1:def 16;
y*c in J by A3,Def2
; then a*(y*c) in {a*i where i is Element of R : i in J};
then u in a*J by A4,Def19;
hence u in I by A2;
end; then (y*a)*J c= I by TARSKI:def 3;
hence thesis by A2;
end;
hence thesis by A1,Def2;
end;
cluster I % J -> right-ideal;
coherence proof set M = {a where a is Element of R: a*J c= I};
A5: M = I % J by Def24;
then reconsider M as non empty Subset of R;
for y,x being Element of R st x in M holds x*y in M proof
let y,x be Element of R;
assume x in M;
then consider a being Element of R such that A6: x = a & a*J c= I;
now let u be set; assume u in (a*y)*J;
then u in {(a*y)*i where i is Element of R : i in J} by Def19;
then consider c being Element of R such that
A7: u = (a*y)*c & c in J;
A8: u = y*(a*c) by A7,VECTSP_1:def 16;
a*c in {a*i where i is Element of R : i in J} by A7; then a*c in a*J
by Def19;
hence u in I by A6,A8,Def2;
end;
then (a*y)*J c= I by TARSKI:def 3;
hence thesis by A6;
end;
hence thesis by A5,Def3;
end;
end;
theorem
for R being (non empty multLoopStr),
I being right-ideal (non empty Subset of R),
J being Subset of R
holds I c= I % J
proof let R be (non empty multLoopStr),
I be right-ideal (non empty Subset of R), J be Subset of R;
now let u be set; assume A1: u in I;
then reconsider u' = u as Element of R;
now let v be set; assume v in u'*J;
then v in {u'*j where j is Element of R : j in J} by Def19;
then consider j being Element of R such that
A2: v = u'*j & j in J;
thus v in I by A1,A2,Def3;
end; then u'*J c= I by TARSKI:def 3;
then u' in {a where a is Element of R: a*J c= I};
hence u in (I % J) by Def24;
end;
hence thesis by TARSKI:def 3;
end;
theorem
for R being right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr),
I being add-closed left-ideal (non empty Subset of R),
J being Subset of R
holds (I % J) *' J c= I
proof let R be right_zeroed add-left-cancelable
left-distributive (non empty doubleLoopStr),
I be add-closed left-ideal (non empty Subset of R), J be Subset of R;
now let u be set; assume u in (I % J) *' J;
then u in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I%J & b in
J} by Def22;
then consider s being FinSequence of the carrier of R such that
A1: Sum s = u & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I%J & b in J;
consider f being Function of NAT,the carrier of R such that
A2: Sum s = f.(len s) & f.0 = 0.R &
for j being Nat, v being Element of R
st j < len s & v = s.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
defpred P[Nat] means f.$1 in I;
A3: P[0] by A2,Th2;
A4: now let j be Nat;
assume A5: 0 <= j & j < len s;
thus P[j] implies P[j+1] proof
assume A6: f.j in I;
A7: j + 1 <= len s by A5,NAT_1:38;
A8: 0 + 1 <= j + 1 by A5,AXIOMS:24;
then j + 1 in Seg(len s) by A7,FINSEQ_1:3;
then j + 1 in dom s by FINSEQ_1:def 3;
then A9: s.(j+1) = s/.(j+1) by FINSEQ_4:def 4;
then A10: f.(j+1) = f.j + s/.(j+1) by A2,A5;
consider a,b being Element of R such that
A11: s.(j+1) = a*b & a in I%J & b in J by A1,A7,A8;
a in {d where d is Element of R: d*J c= I} by A11,Def24;
then consider d being Element of R such that
A12: a = d & d*J c= I;
a*b in {d*i where i is Element of R : i in J} by A11,A12;
then s.(j+1) in d*J by A11,Def19;
hence thesis by A6,A9,A10,A12,Def1;
end;
end;
A13: for j being Nat st 0 <= j & j <= len s holds P[j]
from FinInd(A3,A4);
0 <= len s by NAT_1:18;
hence u in I by A1,A2,A13;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th90:
for R being left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
I being add-closed right-ideal (non empty Subset of R),
J being Subset of R
holds (I % J) *' J c= I
proof let R be left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
I be add-closed right-ideal (non empty Subset of R), J be Subset of R;
now let u be set; assume u in (I % J) *' J;
then u in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I%J & b in
J} by Def22;
then consider s being FinSequence of the carrier of R such that
A1: Sum s = u & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I%J & b in J;
consider f being Function of NAT,the carrier of R such that
A2: Sum s = f.(len s) & f.0 = 0.R &
for j being Nat, v being Element of R
st j < len s & v = s.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
defpred P[Nat] means f.$1 in I;
A3: P[0] by A2,Th3;
A4: now let j be Nat;
assume A5: 0 <= j & j < len s;
thus P[j] implies P[j+1] proof
assume A6: f.j in I;
A7: j + 1 <= len s by A5,NAT_1:38;
A8: 0 + 1 <= j + 1 by A5,AXIOMS:24;
then j + 1 in Seg(len s) by A7,FINSEQ_1:3;
then j + 1 in dom s by FINSEQ_1:def 3;
then A9: s.(j+1) = s/.(j+1) by FINSEQ_4:def 4;
then A10: f.(j+1) = f.j + s/.(j+1) by A2,A5;
consider a,b being Element of R such that
A11: s.(j+1) = a*b & a in I%J & b in J by A1,A7,A8;
a in {d where d is Element of R: d*J c= I} by A11,Def24;
then consider d being Element of R such that
A12: a = d & d*J c= I;
a*b in {d*i where i is Element of R : i in J} by A11,A12;
then s.(j+1) in d*J by A11,Def19;
hence thesis by A6,A9,A10,A12,Def1;
end;
end;
A13: for j being Nat st 0 <= j & j <= len s holds P[j] from FinInd(A3,A4);
0 <= len s by NAT_1:18;
hence u in I by A1,A2,A13;
end;
hence thesis by TARSKI:def 3;
end;
theorem
for R being left_zeroed add-right-cancelable right-distributive
commutative associative (non empty doubleLoopStr),
I being add-closed right-ideal (non empty Subset of R),
J,K being Subset of R
holds (I % J) % K = I % (J *' K)
proof let R be left_zeroed add-right-cancelable right-distributive
commutative associative (non empty doubleLoopStr),
I be add-closed right-ideal (non empty Subset of R), J,K be Subset of R;
A1: now let u be set; assume u in (I % J) % K;
then u in {a where a is Element of R: a*K c= I%J} by Def24;
then consider a being Element of R such that
A2: u = a & a*K c= I % J;
now let v be set; assume v in a*(J *' K);
then v in {a*b where b is Element of R : b in J*'K} by Def19;
then consider b being Element of R such that
A3: v = a*b & b in J *' K;
b in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in J & b in
K} by A3,Def22;
then consider s being FinSequence of the carrier of R such that
A4: Sum s = b & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in J & b in K;
set q = a*s;
A5: dom q = dom s by POLYNOM1:def 2;
A6: Seg(len q) = dom q by FINSEQ_1:def 3 .= dom s by POLYNOM1:def 2
.= Seg(len s) by FINSEQ_1:def 3;
then A7: len q = len s by FINSEQ_1:8;
A8: for j being Nat st 1 <= j & j <= len q holds
ex c,d being Element of R st q.j = c*d & c in I%J & d in J proof
let j be Nat;
assume A9: 1 <= j & j <= len q;
then consider c,d being Element of R such that
A10: s.j = c*d & c in J & d in K by A4,A7;
j in Seg(len s) by A6,A9,FINSEQ_1:3;
then A11: j in dom s by FINSEQ_1:def 3;
then A12: s/.j = c*d by A10,FINSEQ_4:def 4;
A13: q.j = q/.j by A5,A11,FINSEQ_4:def 4
.= a*(c*d) by A11,A12,POLYNOM1:def 2
.= (a*d)*c by VECTSP_1:def 16;
a*d in {a*b' where b' is Element of R : b' in K} by A10;
then a*d in a*K by Def19;
hence thesis by A2,A10,A13;
end;
A14: Sum q = v by A3,A4,BINOM:4;
Sum q in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in I%J & b in J} by A8;
then A15: v in (I % J) *' J by A14,Def22; (I % J) *' J c= I by Th90;
hence v in I by A15;
end;
then a*(J*'K) c= I by TARSKI:def 3;
then u in {f where f is Element of R: f*(J*'K) c= I} by A2;
hence u in I % (J *' K) by Def24;
end;
now let u be set; assume u in I % (J *' K);
then u in {f where f is Element of R: f*(J*'K) c= I} by Def24;
then consider a being Element of R such that
A16: u = a & a*(J *' K) c= I;
now let v be set; assume v in a*K;
then v in {a*b where b is Element of R : b in K} by Def19;
then consider b being Element of R such that A17: v = a*b & b in K;
now let z be set; assume z in (a*b)*J;
then z in {(a*b)*c where c is Element of R : c in J} by Def19;
then consider c being Element of R such that
A18: z = (a*b)*c & c in J;
A19: z = a*(c*b) by A18,VECTSP_1:def 16; set q = <*c*b*>;
A20: len q = 1 by FINSEQ_1:57;
A21: for i being Nat st 1 <= i & i <= len q
ex x,y being Element of R st q.i = x*y & x in J & y in
K proof
let i be Nat; assume 1 <= i & i <= len q;
then q.i = q.1 by A20,AXIOMS:21 .= c*b by FINSEQ_1:57;
hence thesis by A17,A18;
end;
Sum q = c*b by BINOM:3;
then c*b in {Sum t where t is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len t
ex a,b being Element of R st t.i = a*b & a in J & b in K} by A21;
then c*b in J *' K by Def22;
then z in {a*f where f is Element of R : f in J*'K} by A19;
then z in a*(J *' K) by Def19;
hence z in I by A16;
end; then (a*b)*J c= I by TARSKI:def 3;
then v in {f where f is Element of R: f*J c= I} by A17;
hence v in I % J by Def24;
end; then a*K c= I % J by TARSKI:def 3;
then u in {f where f is Element of R: f*K c= I % J} by A16;
hence u in (I % J) % K by Def24;
end;
hence thesis by A1,TARSKI:2;
end;
theorem
for R being non empty multLoopStr, I,J,K being Subset of R
holds (J /\ K) % I = (J % I) /\ (K % I)
proof let R be (non empty multLoopStr), I,J,K be Subset of R;
A1: now let u be set; assume u in (J /\ K) % I;
then u in {a where a is Element of R: a*I c= (J /\ K)} by Def24;
then consider a being Element of R such that
A2: u = a & a*I c= (J /\ K);
now let v be set; assume v in a*I; then v in J /\ K by A2;
then v in { x where x is Element of R : x in J & x in K} by Def21;
then consider x being Element of R such that
A3: v = x & x in J & x in K;
thus v in J by A3;
end; then a*I c= J by TARSKI:def 3;
then u in {a' where a' is Element of R: a'*I c= J} by A2;
then A4: u in (J % I) by Def24;
now let v be set; assume v in a*I; then v in J /\ K by A2;
then v in { x where x is Element of R : x in J & x in K} by Def21;
then consider x being Element of R such that
A5: v = x & x in J & x in K;
thus v in K by A5;
end;
then a*I c= K by TARSKI:def 3;
then u in {a' where a' is Element of R: a'*I c= K} by A2;
then u in (K % I) by Def24;
then u in { x where x is Element of R : x in J%I & x in K%I } by A4;
hence u in (J % I) /\ (K % I) by Def21;
end;
now let u be set; assume u in (J % I) /\ (K % I);
then u in { x where x is Element of R : x in J%I & x in K%I} by Def21;
then consider x being Element of R such that
A6: x = u & x in (J % I) & x in (K % I);
A7: u in {a' where a' is Element of R: a'*I c= J} &
u in {a' where a' is Element of R: a'*I c= K} by A6,Def24;
then consider a being Element of R such that
A8: u = a & a*I c= J;
consider b being Element of R such that
A9: u = b & b*I c= K by A7;
now let v be set; assume A10: v in a*I;
v in { x' where x' is Element of R : x' in J & x' in K}
by A8,A9,A10;
hence v in J /\ K by Def21;
end;
then a*I c= J /\ K by TARSKI:def 3;
then u in {a' where a' is Element of R: a'*I c= (J /\ K)} by A8;
hence u in (J /\ K) % I by Def24;
end;
hence thesis by A1,TARSKI:2;
end;
theorem
for R being left_zeroed right_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
I being add-closed Subset of R,
J,K being right-ideal (non empty Subset of R)
holds I % (J + K) = (I % J) /\ (I % K)
proof let R be left_zeroed right_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
I be add-closed Subset of R, J,K be right-ideal (non empty Subset of R);
A1: now let u be set; assume u in I % (J + K);
then u in {a' where a' is Element of R: a'*(J+K) c= I} by Def24;
then consider a being Element of R such that
A2: u = a & a*(J+K) c= I;
now let u be set; assume u in a*K;
then u in {a*j where j is Element of R : j in K} by Def19;
then consider j being Element of R such that
A3: u = a*j & j in K; K c= J+K by Th74;
then u in {a*j' where j' is Element of R : j' in J+K} by A3;
then u in a*(J+K) by Def19;
hence u in I by A2;
end;
then a*K c= I by TARSKI:def 3;
then u in {a' where a' is Element of R: a'*K c= I} by A2;
then A4: u in (I % K) by Def24;
now let u be set; assume u in a*J;
then u in {a*j where j is Element of R : j in J} by Def19;
then consider j being Element of R such that
A5: u = a*j & j in J;
J c= J+K by Th73;
then u in {a*j' where j' is Element of R : j' in J+K} by A5;
then u in a*(J+K) by Def19;
hence u in I by A2;
end; then a*J c= I by TARSKI:def 3;
then u in {a' where a' is Element of R: a'*J c= I} by A2;
then u in (I % J) by Def24;
then u in {x where x is Element of R: x in (I % J) & x in (I % K)} by A4
;
hence u in (I % J) /\ (I % K) by Def21;
end;
now let u be set; assume u in (I % J) /\ (I % K);
then u in {x where x is Element of R: x in (I % J) & x in (I % K)} by Def21
;
then consider x being Element of R such that
A6: u = x & x in (I % J) & x in (I % K);
A7: u in {a where a is Element of R: a*J c= I} &
u in {a where a is Element of R: a*K c= I} by A6,Def24;
then consider a being Element of R such that
A8: u = a & a*J c= I;
consider b being Element of R such that
A9: u = b & b*K c= I by A7;
now let v be set; assume v in a*(J+K);
then v in {a*j where j is Element of R : j in J+K} by Def19;
then consider j being Element of R such that
A10: v = a*j & j in J+K;
j in {x'+y where x',y is Element of R : x' in J & y in K} by A10,Def20;
then consider x',y being Element of R such that
A11: j = x' + y & x' in J & y in K;
A12: v = a*x' + b*y by A8,A9,A10,A11,VECTSP_1:def 11;
a*x' in {a*j' where j' is Element of R : j' in J} by A11;
then A13: a*x' in a*J by Def19;
b*y in {b*j' where j' is Element of R : j' in K} by A11;
then b*y in b*K by Def19;
hence v in I by A8,A9,A12,A13,Def1;
end;
then a*(J+K) c= I by TARSKI:def 3;
then u in {a' where a' is Element of R: a'*(J+K) c= I} by A8;
hence u in I % (J + K) by Def24;
end;
hence thesis by A1,TARSKI:2;
end;
definition
let R be unital (non empty doubleLoopStr),
I be Subset of R;
func sqrt I -> Subset of R equals :Def25:
{a where a is Element of R: ex n being Nat st a|^n in I};
coherence proof set M = {a where a is Element of R:ex n being Nat st a|^n in
I};
M is Subset of R proof
for x being set holds x in M implies x in the carrier of R proof
let x be set; assume x in M;
then consider a being Element of R such that
A1: a = x & ex n being Nat st a|^n in I;
thus thesis by A1;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis;
end;
end;
definition
let R be unital (non empty doubleLoopStr), I be non empty Subset of R;
cluster sqrt I -> non empty;
coherence proof set M ={a where a is Element of R: ex n being Nat st a|^n in
I};
M is non empty proof consider a being Element of I; a|^1 = a by BINOM:8;
then a in M;
hence thesis;
end;
hence thesis by Def25;
end;
end;
definition
let R be Abelian add-associative left_zeroed right_zeroed
commutative associative add-cancelable distributive
unital (non empty doubleLoopStr),
I be add-closed right-ideal (non empty Subset of R);
cluster sqrt I -> add-closed;
coherence proof set M ={a where a is Element of R: ex n being Nat st a|^n in
I};
A1: M = sqrt I by Def25;
then reconsider M as non empty Subset of R;
for x,y being Element of R st x in M & y in M holds x+y in
M proof
let x,y be Element of R;
assume A2: x in M & y in M; then consider a being Element of R such
that
A3: x = a & ex n being Nat st a|^n in I;
consider n being Nat such that A4: a|^n in I by A3;
consider b being Element of R such that
A5: y = b & ex m being Nat st b|^m in I by A2;
consider m being Nat such that A6: b|^m in I by A5;
A7: (a+b)|^(n+m) = Sum((a,b) In_Power (n+m)) by BINOM:26;
set p = ((a,b) In_Power (n+m));
consider f being Function of NAT,the carrier of R such that
A8: 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;
A9: 0 <= len p by NAT_1:18;
A10: for i being Nat st 1 <= i & i <= len p holds p.i in I proof
let i be Nat;
assume A11: 1 <= i & i <= len p; then i in Seg(len p) by FINSEQ_1:3;
then A12: i in dom p by FINSEQ_1:def 3;
set r = i - 1; set l = (n+m) - r;
1 - 1 <= i - 1 by A11,REAL_1:49;
then reconsider r as Nat by INT_1:16;
i <= (n+m) + 1 by A11,BINOM:def 10;
then r <= ((n+m) + 1) - 1 by REAL_1:49;
then r <= ((n+m) + 1) + -1 by XCMPLX_0:def 8;
then r <= (n+m) + (1 + -1) by XCMPLX_1:1;
then r - r <= (n+m) - r by REAL_1:49;
then 0 <= l by XCMPLX_1:14;
then reconsider l as Nat by INT_1:16;
A13: p.i = p/.i by A12,FINSEQ_4:def 4
.= ((n+m) choose r)*a|^l*b|^r by A12,BINOM:def 10;
per cases;
suppose n <= l;
then consider k being Nat such that
A14: l = n + k by NAT_1:28;
a|^l = (a|^n)*(a|^k) by A14,BINOM:11;
then a|^l in I by A4,Def3; then ((n+m) choose r)*a|^l in I by Th17;
hence thesis by A13,Def3;
suppose l < n; then ((n+m) + -r) < n by XCMPLX_0:def 8;
then ((n+m) + -r) + r < n + r by REAL_1:53;
then (n+m) + (-r + r) < n + r by XCMPLX_1:1;
then (n+m) + (r - r) < n + r by XCMPLX_0:def 8;
then (n+m) + 0 < n + r by XCMPLX_1:14;
then -n + (n+m) < -n + (n + r) by REAL_1:53;
then (-n + n) + m < -n + (n + r) by XCMPLX_1:1;
then (-n + n) + m < (-n + n) + r by XCMPLX_1:1;
then (-n + n) + m < (n - n) + r by XCMPLX_0:def 8;
then (-n + n) + m < 0 + r by XCMPLX_1:14;
then (n - n) + m < 0 + r by XCMPLX_0:def 8;
then 0 + m < r by XCMPLX_1:14; then consider k being Nat such that
A15: r = m + k by NAT_1:28;
b|^r = (b|^m)*(b|^k) by A15,BINOM:11;
then b|^r in I by A6,Def3;
hence thesis by A13,Def3;
end;
defpred P[Nat] means f.$1 in I;
A16: P[0] by A8,Th2;
A17: now let j be Nat;
assume A18: 0 <= j & j < len p;
thus P[j] implies P[j+1] proof
assume A19: f.j in I;
A20: 1 <= j + 1 by NAT_1:29;
A21: j + 1 <= len p by A18,NAT_1:38;
then j + 1 in Seg(len p) by A20,FINSEQ_1:3;
then j + 1 in dom p by FINSEQ_1:def 3;
then A22: p/.(j+1) = p.(j+1) by FINSEQ_4:def 4;
then A23: f.(j + 1) = f.j + p/.(j+1) by A8,A18;
p/.(j+1) in I by A10,A20,A21,A22;
hence thesis by A19,A23,Def1;
end;
end;
for i being Nat st 0 <= i & i <= len p holds P[i]
from FinInd(A16,A17);
then (a+b)|^(n+m) in I by A7,A8,A9;
hence thesis by A3,A5;
end;
hence thesis by A1,Def1;
end;
end;
definition
let R be unital commutative associative (non empty doubleLoopStr),
I be left-ideal (non empty Subset of R);
cluster sqrt I -> left-ideal;
coherence proof set M ={a where a is Element of R: ex n being Nat st a|^n in
I};
A1: M = sqrt I by Def25;
then reconsider M as non empty Subset of R;
for y,x being Element of R st x in M holds y*x in M proof
let y',x' be Element of R;
assume A2: x' in M;
reconsider x = x',y = y' as Element of R;
consider a being Element of R such that
A3: x = a & ex n being Nat st a|^n in I by A2;
consider n being Nat such that A4: a|^n in I by A3;
A5: (y|^n)*(a|^n) in I by A4,Def2; (y*a)|^n = (y|^n)*(a|^n) by BINOM:10
;
hence thesis by A3,A5;
end;
hence thesis by A1,Def2;
end;
cluster sqrt I -> right-ideal;
coherence proof set M ={a where a is Element of R: ex n being Nat st a|^n in
I};
A6: M = sqrt I by Def25;
then reconsider M as non empty Subset of R;
for y,x being Element of R st x in M holds x*y in M proof
let y',x' be Element of R;
assume A7: x' in M;
reconsider x = x',y = y' as Element of R;
consider a being Element of R such that
A8: x = a & ex n being Nat st a|^n in I by A7;
consider n being Nat such that A9: a|^n in I by A8;
A10: (y|^n)*(a|^n) in I by A9,Def2;
(y*a)|^n = (y|^n)*(a|^n) by BINOM:10;
hence thesis by A8,A10;
end;
hence thesis by A6,Def3;
end;
end;
theorem
for R being unital associative (non empty doubleLoopStr),
I being non empty Subset of R, a being Element of R
holds a in sqrt I iff ex n being Nat st a|^n in sqrt I
proof let R be unital associative (non empty doubleLoopStr),
I be non empty Subset of R, a be Element of R;
A1: now assume A2: a in sqrt I; a|^1 = a by BINOM:8;
hence ex n being Nat st a|^n in sqrt I by A2;
end;
now assume ex n being Nat st a|^n in sqrt I;
then consider n being Nat such that A3: a|^n in sqrt I;
a|^n in {d where d is Element of R: ex m being Nat st d|^m in
I} by A3,Def25;
then consider d being Element of R such that
A4: a|^n = d & ex m being Nat st d|^m in I;
consider m being Nat such that A5: d|^m in I by A4;
a|^(n*m) = d|^m by A4,BINOM:12;
then a in {g where g is Element of R: ex l being Nat st g|^l in I} by A5;
hence a in sqrt I by Def25;
end;
hence thesis by A1;
end;
theorem
for R being left_zeroed right_zeroed add-cancelable distributive
unital associative (non empty doubleLoopStr),
I being add-closed right-ideal (non empty Subset of R),
J being add-closed left-ideal (non empty Subset of R)
holds sqrt (I *' J) = sqrt (I /\ J)
proof let R be left_zeroed right_zeroed associative
add-cancelable distributive unital (non empty doubleLoopStr),
I be add-closed right-ideal (non empty Subset of R),
J be add-closed left-ideal(non empty Subset of R);
A1: now let u be set; assume u in sqrt (I *' J);
then u in {d where d is Element of R: ex m being Nat st d|^m in I*'J} by
Def25;
then consider d being Element of R such that
A2: u = d & ex m being Nat st d|^m in I *' J;
consider m being Nat such that A3: d|^m in I *' J by A2;
d|^m in {Sum s where s is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J} by A3,Def22;
then consider s being FinSequence of the carrier of R such that
A4: d|^m = Sum s & for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J;
consider f being Function of NAT,the carrier of R such that
A5: Sum s = f.(len s) & f.0 = 0.R &
for j being Nat, v being Element of R
st j < len s & v = s.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
defpred P[Nat] means f.$1 in I /\ J;
f.0 in I & f.0 in J by A5,Th2,Th3;
then f.0 in {g where g is Element of R: g in I & g in J};
then A6: P[0] by Def21;
A7: now let j be Nat;
assume A8: 0 <= j & j < len s;
thus P[j] implies P[j+1] proof
assume f.j in I /\ J;
then f.j in {g where g is Element of R: g in I & g in J} by Def21;
then consider g being Element of R such that
A9: g = f.j & g in I & g in J;
A10: j + 1 <= len s by A8,NAT_1:38;
A11: 0 + 1 <= j + 1 by A8,AXIOMS:24;
then j + 1 in Seg(len s) by A10,FINSEQ_1:3;
then j + 1 in dom s by FINSEQ_1:def 3;
then A12: s.(j+1) = s/.(j+1) by FINSEQ_4:def 4;
then A13: f.(j+1) = f.j + s/.(j+1) by A5,A8;
consider a,b being Element of R such that
A14: s.(j+1) = a*b & a in I & b in J by A4,A10,A11;
s/.(j+1) in I & s/.(j+1) in J by A12,A14,Def2,Def3;
then A15: f.(j+1) in I & f.(j+1) in J by A9,A13,Def1;
f.(j+1) in {g' where g' is Element of R: g' in I & g' in
J} by A15;
hence thesis by Def21;
end;
end;
A16: for j being Nat st 0 <= j&j<=len s holds P[j]
from FinInd(A6,A7);
0 <= len s by NAT_1:18;
then Sum s in I /\ J by A5,A16;
then u in {d' where d' is Element of R: ex m being Nat st d'|^m in
I /\ J} by A2,A4;
hence u in sqrt (I /\ J) by Def25;
end;
now let u be set; assume u in sqrt (I /\ J);
then u in {d where d is Element of R: ex m being Nat st d|^m in I/\J} by
Def25;
then consider d being Element of R such that
A17: u = d & ex m being Nat st d|^m in I /\ J;
consider m being Nat such that A18: d|^m in I /\ J by A17;
d|^m in {g where g is Element of R: g in I & g in J} by A18,Def21;
then consider g being Element of R such that
A19: d|^m = g & g in I & g in J;
set q = <*d|^m*d|^m*>;
A20: len q = 1 by FINSEQ_1:57;
A21: for i being Nat st 1 <= i & i <= len q
ex x,y being Element of R st q.i = x*y & x in I & y in J proof
let i be Nat;
assume A22: 1 <= i & i <= len q; then i in Seg(len q) by FINSEQ_1:3;
then i in dom q by FINSEQ_1:def 3;
then A23: q.i = q/.i by FINSEQ_4:def 4;
then q/.i = q.1 by A20,A22,AXIOMS:21 .= d|^m*d|^m by FINSEQ_1:57;
hence thesis by A19,A23;
end;
d|^(m+m) = d|^m*d|^m by BINOM:11 .= Sum q by BINOM:3;
then d|^(m+m) in {Sum s where s is FinSequence of the carrier of R :
for i being Nat st 1 <= i & i <= len s
ex a,b being Element of R st s.i = a*b & a in I & b in J} by A21;
then d|^(m+m) in I *' J by Def22;
then u in {d' where d' is Element of R: ex m being Nat st d'|^m in I *'
J} by A17;
hence u in sqrt (I *' J) by Def25;
end;
hence thesis by A1,TARSKI:2;
end;
begin :: Noetherian ideals
definition
let L be non empty doubleLoopStr, I be Ideal of L;
attr I is finitely_generated means :
Def26:
ex F being non empty finite Subset of L st I = F-Ideal;
end;
definition
let L be non empty doubleLoopStr;
cluster finitely_generated Ideal of L;
existence proof consider x being set such that
A1: x in the carrier of L by XBOOLE_0:def 1;
reconsider x as Element of L by A1;
take {x}-Ideal; thus thesis by Def26;
end;
end;
definition
let L be non empty doubleLoopStr,
F be non empty finite Subset of L;
cluster F-Ideal -> finitely_generated;
coherence by Def26;
end;
definition
let L be non empty doubleLoopStr;
attr L is Noetherian means :Def27:
for I being Ideal of L holds I is finitely_generated;
end;
definition
cluster Euclidian Abelian add-associative right_zeroed right_complementable
well-unital distributive commutative associative non degenerated
(non empty doubleLoopStr);
existence proof take INT.Ring; thus thesis; end;
end;
definition
let L be non empty doubleLoopStr;
let I be Ideal of L;
attr I is principal means :Def28:
ex e being Element of L st I = {e}-Ideal;
end;
definition
let L be non empty doubleLoopStr;
attr L is PID means :Def29
:
for I being Ideal of L holds I is principal;
end;
theorem Th96:
for L being non empty doubleLoopStr,
F being non empty Subset of L st F <> {0.L}
ex x being Element of L st x <> 0.L & x in F
proof let L be non empty doubleLoopStr,
F be non empty Subset of L;
assume A1: F <> {0.L};
now assume A2: for x being set st x in F holds x = 0.L;
for x being set holds x in F iff x = 0.L proof let e be set;
thus e in F implies e = 0.L by A2;
assume A3: e = 0.L;
ex a being set st a in F by XBOOLE_0:def 1;
hence e in F by A2,A3;
end;
hence contradiction by A1,TARSKI:def 1;
end;
hence thesis;
end;
theorem Th97:
for R being add-associative left_zeroed right_zeroed right_complementable
distributive left_unital Euclidian (non empty doubleLoopStr)
holds R is PID
proof let R be add-associative left_zeroed right_zeroed right_complementable
distributive left_unital Euclidian (non empty doubleLoopStr);
let I be Ideal of R;
per cases;
suppose A1: I = {0.R}; set e = 0.R;
take e;
thus I = {e}-Ideal by A1,Th47;
suppose I <> {0.R}; then consider x being Element of R such
that
A2: x <> 0.R & x in I by Th96;
set I' = { y where y is Element of I : y <> 0.R };
A3: x in I' by A2;
I' c= the carrier of R proof let x be set;
assume x in I'; then consider y being Element of I such that
A4: x=y & y <> 0.R;
thus x in the carrier of R by A4;
end; then reconsider I' as non empty Subset of R by A3;
consider f being Function of the carrier of R, NAT such that
A5: for a,b being Element of R st b <> 0.R holds
(ex q,r being Element of R st
(a = q*b + r & (r = 0.R or (f.r qua Nat) < (f.b qua Nat))))
by INT_3:def 9;
set K = { f.i where i is Element of I' : not contradiction };
consider i being Element of I';
A6: f.i in K;
K c= NAT proof let x be set;
assume x in K; then consider e being Element of I' such that
A7: f.e = x;
thus x in NAT by A7;
end;
then reconsider K as non empty Subset of NAT by A6;
set k=min K;
k in K by CQC_SIM1:def 8; then consider e being Element of I' such that
A8: f.e = k; e in I'; then consider e' being Element of I such that
A9: e'=e & e' <> 0.R;
take e;
now let x be set;
hereby assume A10: x in I;
then reconsider x'=x as Element of R;
consider q,r being Element of R such that
A11: x' = q*e + r and
A12: r = 0.R or (f.r qua Nat) < k by A5,A8,A9;
now
A13: -(q*e) + x' = -(q*e) + q*e + r by A11,RLVECT_1:def 6 .= 0.R + r
by RLVECT_1:16
.= r by ALGSTR_1:def 5; q*e in I by A9,Def2;
then -(q*e) in I by Th13;
then A14: r in I by A10,A13,Def1;
assume A15: r <> 0.R; then r in I' by A14;
then f.r in K;
hence contradiction by A12,A15,CQC_SIM1:def 8;
end;
then A16: x' = q*e by A11,RLVECT_1:def 7;
A17: e in {e} by TARSKI:def 1; {e} c= {e}-Ideal by Def15;
hence x in {e}-Ideal by A16,A17,Def2;
end;
assume A18: x in {e}-Ideal;
{e} c= I by A9,ZFMISC_1:37;
then {e}-Ideal c= I by Def15;
hence x in I by A18;
end;
hence I={e}-Ideal by TARSKI:2;
end;
theorem Th98:
for L being non empty doubleLoopStr st L is PID holds L is Noetherian
proof let L be non empty doubleLoopStr; assume
A1: L is PID;
let I being Ideal of L; I is principal by A1,Def29;
then consider e being Element of L such that
A2: I = {e}-Ideal by Def28;
take F={e}; thus F-Ideal=I by A2;
end;
definition
cluster INT.Ring -> Noetherian;
coherence proof INT.Ring is PID by Th97;
hence thesis by Th98;
end;
end;
definition
cluster Noetherian Abelian add-associative right_zeroed right_complementable
well-unital distributive commutative associative non degenerated
(non empty doubleLoopStr);
existence proof take INT.Ring; thus thesis; end;
end;
theorem :: Lemma_4_5_i_ii:
for R being Noetherian add-associative left_zeroed right_zeroed
add-cancelable
associative distributive well-unital (non empty doubleLoopStr)
for B being non empty Subset of R
ex C being non empty finite Subset of R
st C c= B & C-Ideal = B-Ideal
proof
let R be Noetherian add-associative left_zeroed right_zeroed add-cancelable
associative distributive well-unital (non empty doubleLoopStr);
let B be non empty Subset of R;
B-Ideal is finitely_generated by Def27;
then consider D being non empty finite Subset of R such that
A1: D-Ideal = B-Ideal by Def26;
A2: D c= B-Ideal by A1,Def15;
defpred P[set,set] means
ex cL being non empty LinearCombination of B st $1 = Sum cL &
ex fsB being FinSequence of B st dom fsB = dom cL & $2 = rng fsB &
for i being Nat st i in dom cL ex u, v being Element of R st
cL/.i = u*((fsB/.i qua Element of B)
qua Element of R)*v;
A3: for e being set st e in D ex u being set st u in bool B & P[e,u] proof
let e be set; assume e in D;
then consider cL being LinearCombination of B such that
A4: e = Sum cL by A2,Th60;
per cases;
suppose A5: cL is non empty;
defpred P1[set,Element of B] means
ex u, v being Element of R st
cL/.$1 = u*(($2 qua Element of B)
qua Element of R)*v;
A6: now let k be Nat; assume k in Seg len cL;
then k in dom cL by FINSEQ_1:def 3;
then consider u, v being Element of R, a being Element of B such that
A7: cL/.k = u*a*v by Def9;
take d = a;
thus P1[k,d] by A7;
end;
consider fsB being FinSequence of B such that
A8: dom fsB = Seg len cL and
A9: for k being Nat st k in Seg len cL holds
P1[k,fsB/.k] from SeqExD(A6);
take u = rng fsB; thus u in bool B; dom cL = Seg len cL by FINSEQ_1:def 3
;
hence P[e,u] by A4,A5,A8,A9;
suppose A10: cL is empty;
consider b being Element of B;
set kL = <*0.R*b*0.R*>;
now let i be set; assume i in dom kL;
then i in Seg len kL by FINSEQ_1:def 3;
then i in {1} by FINSEQ_1:4,57;
then A11: i = 1 by TARSKI:def 1;
take u = 0.R, v = 0.R, b; thus kL/.i = u*b*v by A11,FINSEQ_4:25;
end;
then reconsider kL as non empty LinearCombination of B by Def9;
cL = <*>the carrier of R by A10;
then A12: e = 0.R by A4,RLVECT_1:60 .= 0.R*b*0.R by BINOM:2
.= Sum kL by BINOM:3;
defpred P2[Nat,Element of B] means ex u, v being Element of R st
kL/.$1 = u*(($2 qua Element of B)
qua Element of R)*v;
A13: now let k be Nat; assume k in Seg len kL;
then k in {1} by FINSEQ_1:4,57;
then A14: k = 1 by TARSKI:def 1;
take b;
thus P2[k,b]
proof
take u=0.R, v=0.R;
thus thesis by A14,FINSEQ_4:25;
end;
end;
consider fsB being FinSequence of B such that
A15: dom fsB = Seg len kL and
A16: for k being Nat st k in Seg len kL holds
P2[k,fsB/.k] from SeqExD(A13);
take u = rng fsB;
thus u in bool B; dom kL = Seg len kL by FINSEQ_1:def 3;
hence P[e,u] by A12,A15,A16;
end;
consider f being Function of D, bool B such that
A17: for e being set st e in D holds P[e,f.e] from FuncEx1(A3);
reconsider rf = rng f as Subset-Family of B by SETFAM_1:def 7;
reconsider C = union rf as Subset of B;
consider r being set such that
A18: r in rng f by XBOOLE_0:def 1;
consider x being set such that
A19: x in dom f & r = f.x by A18,FUNCT_1:def 5;
A20: dom f = D by FUNCT_2:def 1;
consider cL being non empty LinearCombination of B such that
x = Sum cL and
A21: ex fsB being FinSequence of B st dom fsB = dom cL & r = rng fsB &
for i being Nat st i in dom cL ex u, v being Element of R st
cL/.i = u*((fsB/.i qua Element of B)
qua Element of R)*v by A17,A19;
consider fsB being FinSequence of B such that
A22: dom fsB = dom cL and
A23: r = rng fsB and
for i being Nat st i in dom cL ex u, v being Element of R st
cL/.i = u*((fsB/.i qua Element of B)
qua Element of R)*v by A21;
r is non empty by A22,A23,RELAT_1:65;
then consider x being set such that
A24: x in r by XBOOLE_0:def 1;
A25: rng f is finite by A20,FINSET_1:26;
A26: now let r be set; assume r in rng f;
then consider x being set such that
A27: x in dom f & r = f.x by FUNCT_1:def 5;
consider cL being non empty LinearCombination of B such that
x = Sum cL and
A28: ex fsB being FinSequence of B st dom fsB = dom cL & r = rng fsB &
for i being Nat st i in dom cL ex u, v being Element of R st
cL/.i = u*((fsB/.i qua Element of B)
qua Element of R)*v by A17,A27;
consider fsB being FinSequence of B such that
dom fsB = dom cL and
A29: r = rng fsB and
for i being Nat st i in dom cL ex u, v being Element of R st
cL/.i = u*((fsB/.i qua Element of B)
qua Element of R)*v by A28;
thus r is finite by A29;
end;
C c= the carrier of R by XBOOLE_1:1;
then reconsider C as non empty finite Subset of R by A18,A24,A25,A26,
FINSET_1:25,TARSKI:def 4;
now let d be set; assume
A30: d in D;
then d in dom f by FUNCT_2:def 1; then f.d in rng f by FUNCT_1:def 5;
then A31: f.d c= C by ZFMISC_1:92;
consider cL being non empty LinearCombination of B such that
A32: d = Sum cL and
A33: ex fsB being FinSequence of B st dom fsB = dom cL & f.d = rng fsB &
for i being Nat st i in dom cL ex u, v being Element of R st
cL/.i = u*((fsB/.i qua Element of B)
qua Element of R)*v by A17,A30;
now let i be set; assume
A34: i in dom cL;
consider fsB being FinSequence of B such that
A35: dom fsB = dom cL and
A36: f.d = rng fsB and
A37: for i being Nat st i in dom cL ex u, v being Element of R st
cL/.i = u*((fsB/.i qua Element of B)
qua Element of R)*v by A33;
consider u, v being Element of R such that
A38: cL/.i = u*((fsB/.i qua Element of B)
qua Element of R)*v by A34,A37;
fsB/.i = fsB.i by A34,A35,FINSEQ_4:def 4;
then fsB/.i in f.d by A34,A35,A36,FUNCT_1:def 5;
hence ex u,v being Element of R, a being Element of C st cL/.i = u*a*v
by A31,A38;
end;
then reconsider cL'= cL as LinearCombination of C by Def9;
d = Sum cL' by A32;
hence d in C-Ideal by Th60;
end;
then D c= C-Ideal by TARSKI:def 3; then D-Ideal c= (C-Ideal)-Ideal by Th57
;
then A39: B-Ideal c= C-Ideal by A1,Th44;
take C;
C-Ideal c= B-Ideal by Th57;
hence thesis by A39,XBOOLE_0:def 10;
end;
theorem :: Lemma_4_5_ii_iii:
for R being (non empty doubleLoopStr)
st for B being non empty Subset of R
ex C being non empty finite Subset of R
st C c= B & C-Ideal = B-Ideal
for a being sequence of R
ex m being Nat st a.(m+1) in (rng (a|Segm(m+1)))-Ideal
proof let R be (non empty doubleLoopStr);
assume A1: for B being non empty Subset of R
ex C being non empty finite Subset of R
st C c= B & C-Ideal = B-Ideal;
let a being sequence of R;
reconsider B = rng a as non empty Subset of R;
consider C being non empty finite Subset of R such that
A2: C c= B & C-Ideal = B-Ideal by A1;
defpred P[set,set] means $1 = a.$2;
A3: dom a = NAT by FUNCT_2:def 1;
A4: for e being set st e in C ex u being set st u in NAT & P[e,u] proof
let e be set; assume e in C;
then consider u being set such that
A5: u in dom a & e = a.u by A2,FUNCT_1:def 5;
take u; thus u in NAT by A5; thus P[e,u] by A5;
end;
consider f being Function of C, NAT such that
A6: for e being set st e in C holds P[e,f.e] from FuncEx1(A4);
set Rf = rng f;
A7: dom f = C by FUNCT_2:def 1;
then reconsider Rf as non empty finite Subset of NAT by FINSET_1:26;
reconsider m = max Rf as Nat by ORDINAL2:def 21;
take m; set D = rng (a | Segm(m+1));
A8: C c= D proof let X be set; assume
A9: X in C;
then A10: f.X in Rf by A7,FUNCT_1:def 5;
reconsider fx=f.X as Nat;
fx <= m by A10,PRE_CIRC:def 1;
then A11: fx < m+1 by NAT_1:38;
m + 1 > 0 by NAT_1:19; then fx in Segm(m+1) by A11,GR_CY_1:10;
then a.fx in rng (a | Segm(m+1)) by A3,FUNCT_1:73;
hence X in D by A6,A9;
end; then reconsider D as non empty Subset of R by XBOOLE_1:3
;
A12: B-Ideal c= D-Ideal by A2,A8,Th57; D c= B by RELAT_1:99;
then D-Ideal c= B-Ideal by Th57;
then A13: D-Ideal = B-Ideal by A12,XBOOLE_0:def 10;
A14: B c= B-Ideal by Def15;
a.(m+1) in B by FUNCT_2:6;
hence a.(m+1) in (rng (a|Segm(m+1)))-Ideal by A13,A14;
end;
definition
let X, Y be non empty set, f be Function of X, Y, A be non empty Subset of X;
cluster f|A -> non empty;
coherence proof dom f = X by FUNCT_2:def 1;
then (dom f) /\ A is non empty by XBOOLE_1:28;
then (dom f) meets A by XBOOLE_0:def 7;
hence f|A is non empty by RELAT_1:95;
end;
end;
theorem :: Lemma_4_5_iii_iv:
for R being (non empty doubleLoopStr)
st for a being sequence of R
ex m being Nat st a.(m+1) in (rng (a|Segm(m+1)))-Ideal
holds not ex F being Function of NAT, bool (the carrier of R)
st (for i being Nat holds F.i is Ideal of R) &
(for j,k being Nat st j < k holds F.j c< F.k)
proof let R being (non empty doubleLoopStr);
assume A1: for a being sequence of R
ex m being Nat st a.(m+1) in (rng (a|Segm(m+1)))-Ideal;
given F being Function of NAT, bool (the carrier of R) such that
A2: for i being Nat holds F.i is Ideal of R and
A3: for j,k being Nat st j < k holds F.j c< F.k;
defpred P[set,set] means
ex n being Nat st n = $1 &
(n = 0 implies $2 in F.0) &
(n > 0 implies ex k being Nat st n = k+1 & $2 in F.n \ F.k);
A4: for e being set st e in NAT
ex u being set st u in the carrier of R & P[e,u] proof
let e be set such that
A5: e in NAT; reconsider n=e as Nat by A5;
per cases by NAT_1:19;
suppose A6: n = 0; F.0 is Ideal of R by A2;
then consider u being set such that
A7: u in F.0 by XBOOLE_0:def 1;
take u; thus u in the carrier of R by A7; take n; thus n=e;
thus thesis by A6,A7;
suppose n > 0; then consider k being Nat such that
A8: n=k+1 by NAT_1:22;
n > k by A8,NAT_1:38; then F.k c< F.n by A3;
then not (F.n c= F.k) by XBOOLE_1:60;
then F.n \ F.k is non empty by XBOOLE_1:37;
then consider u being set such that
A9: u in F.n \ F.k by XBOOLE_0:def 1;
take u;
thus u in the carrier of R by A9; take n; thus n=e;
thus thesis by A8,A9;
end;
consider f being Function of NAT, the carrier of R such that
A10: for e being set st e in NAT holds P[e, f.e] from FuncEx1(A4);
reconsider f as sequence of R by NORMSP_1:def 3;
defpred P[Nat] means rng (f|Segm($1+1)) c= F.$1;
A11: P[0] proof
let y be set; assume y in rng (f|Segm(0+1));
then consider x being set such that
A12: x in dom (f|Segm(1)) and
A13: y = (f|Segm(1)).x by FUNCT_1:def 5;
A14: x in Segm(1) & x in dom f by A12,RELAT_1:86;
ex n being Nat st n = x & (n = 0 implies f.x in F.0) &
(n > 0 implies ex k being Nat st n = k+1 & f.x in F.n \ F.k) by A10,A12;
hence thesis by A13,A14,FUNCT_1:72,GR_CY_1:13,TARSKI:def 1;
end;
A15: for k being Nat st P[k] holds P[k+1] proof
let k be Nat such that
A16: rng (f|Segm(k+1)) c= F.k;
let y be set such that
A17: y in rng (f|Segm((k+1)+1)); consider x being set such that
A18: x in dom (f|Segm((k+1)+1)) and
A19: y = (f|Segm((k+1)+1)).x by A17,FUNCT_1:def 5;
A20: x in Segm((k+1)+1) & x in dom f by A18,RELAT_1:86;
reconsider nx = x as Nat by A18;
0 < (k+1)+1 by NAT_1:19;
then nx < (k+1)+1 by A20,GR_CY_1:10;
then A21: nx <= k+1 by NAT_1:38;
per cases by A21,AXIOMS:21;
suppose A22: nx < k+1; 0 < k+1 by NAT_1:19;
then A23: nx in Segm(k+1) by A22,GR_CY_1:10;
y = f.nx by A18,A19,FUNCT_1:70;
then y in rng(f|Segm(k+1)) by A20,A23,FUNCT_1:73;
then A24: y in F.k by A16; k < k+1 by NAT_1:38;
then F.k c< F.(k+1) by A3;
then F.k c= F.(k+1) by XBOOLE_0:def 8;
hence y in F.(k+1) by A24;
suppose A25: nx = k+1;
A26: y = f.nx by A18,A19,FUNCT_1:70;
consider n being Nat such that
A27: n = nx and
(n = 0 implies f.nx in F.0) and
A28: (n > 0 implies ex k being Nat st n = k+1 & f.nx in F.n \ F.k) by A10;
consider m being Nat such that
A29: n = m+1 & f.nx in F.n \ F.m by A25,A27,A28,NAT_1:19;
thus y in F.(k+1) by A25,A26,A27,A29,XBOOLE_0:def 4;
end;
A30: for m being Nat holds P[m] from Ind(A11,A15);
consider m being Nat such that
A31: f.(m+1) in (rng (f|Segm(m+1)))-Ideal by A1;
F.m is Ideal of R by A2;
then A32: F.m = (F.m)-Ideal by Th44; (rng (f|Segm(m+1))) c= F.m by A30;
then (rng (f|Segm(m+1)))-Ideal c= F.m by A32,Th57;
then A33: f.(m+1) in F.m by A31; consider n being Nat such that
A34: n = m+1 and n = 0 implies f.(m+1) in F.0 and
A35: n > 0 implies ex k being Nat st n = k+1 & f.(m+1) in F.n \ F.k by A10;
consider k being Nat such that
A36: n = k+1 and
A37: f.(m+1) in F.n \ F.k by A34,A35,NAT_1:19;
not f.(m+1) in F.k by A37,XBOOLE_0:def 4;
hence contradiction by A33,A34,A36,XCMPLX_1:2;
end;
theorem :: Lemma_4_5_iv_i:
for R being (non empty doubleLoopStr)
st not ex F being Function of NAT, bool (the carrier of R)
st (for i being Nat holds F.i is Ideal of R) &
(for j,k being Nat st j < k holds F.j c< F.k)
holds R is Noetherian
proof let R being (non empty doubleLoopStr) such that
A1: not ex F being Function of NAT, bool (the carrier of R)
st (for i being Nat holds F.i is Ideal of R) &
(for j,k being Nat st j < k holds F.j c< F.k) and
A2: not R is Noetherian;
consider I being Ideal of R such that
A3: I is not finitely_generated by A2,Def27;
consider e being set such that
A4: e in I by XBOOLE_0:def 1;
reconsider e as Element of R by A4;
set D = { S where S is Element of bool the carrier of R :
S is non empty finite Subset of I };
{e} c= I by A4,ZFMISC_1:37;
then A5: {e} in D;
D c= bool the carrier of R proof
let x be set; assume x in D;
then ex s being Element of bool the carrier of R st
x = s & s is non empty finite Subset of I;
hence x in bool the carrier of R;
end; then reconsider D as non empty Subset of bool the carrier of R by A5;
reconsider e'={e} as Element of D by A5;
defpred P[Nat,Element of D,Element of D] means
ex r being Element of R st
r in I \ $2-Ideal & $3 = $2 \/ {r};
A6: for n be Nat for x be Element of D
ex y be Element of D st P[n,x,y] proof let n be Nat, x be Element of D;
x in D; then consider x' being Subset of R such that
A7: x' = x and
A8: x' is non empty finite Subset of I;
A9: I <> x'-Ideal by A3,A8,Def26;
x'-Ideal c= I-Ideal by A8,Th57; then x'-Ideal c= I by Th44;
then not I c= x'-Ideal by A9,XBOOLE_0:def 10;
then consider r being set such that
A10: r in I & not r in x'-Ideal by TARSKI:def 3;
reconsider x1'=x' as non empty finite Subset of I by A8;
set y=x1' \/ {r};
A11: y c= I proof
let x be set; assume x in y; then x in x1' or x in
{r} by XBOOLE_0:def 2;
hence thesis by A10,TARSKI:def 1;
end;
then y is Element of bool the carrier of R by XBOOLE_1:1;
then y in D by A11; then reconsider y as Element of D;
take y; reconsider r as Element of R by A10;
take r;
thus thesis by A7,A10,XBOOLE_0:def 4;
end;
consider f be Function of NAT, D such that
A12: f.0 = e' & for n be Element of NAT holds P[n,f.n,f.(n+1)]
from RecExD(A6);
defpred Q[Nat,Element of bool the carrier of R] means
ex c being Subset of R st c = f.$1 & $2 = c-Ideal;
A13: for x being Nat ex y being Element of bool the carrier of R st Q[x,y]
proof let x be Nat; f.x in D;
then consider c being Subset of R such that
A14: c = f.x & c is non empty finite Subset of I;
reconsider y = c-Ideal as Subset of R;
take y; take c; thus thesis by A14;
end;
consider F being Function of NAT, bool the carrier of R such that
A15: for x being Element of NAT holds Q[x,F.x] from FuncExD(A13);
A16: for i being Nat holds F.i is Ideal of R proof
let i be Nat;
ex c being Subset of R st c = f.i & F.i = c-Ideal by A15
;
hence thesis;
end;
for j,k being Nat st j < k holds F.j c< F.k proof
let j,k be Nat;
defpred P[Nat] means F.j c< F.(j+1+$1);
A17: for i being Nat holds F.i c< F.(i+1) proof
let i be Nat; consider c being Subset of R such that
A18: c = f.i and
A19: F.i = c-Ideal by A15; c in D by A18;
then consider c' being Subset of R such that
A20: c' = c and
A21: c' is non empty finite Subset of I;
consider c1 being Subset of R such that
A22: c1 = f.(i+1) and
A23: F.(i+1) = c1-Ideal by A15; c1 in D by A22;
then consider c1' being Subset of R such that
A24: c1' = c1 and
A25: c1' is non empty finite Subset of I;
consider r being Element of R such that
A26: r in I \ c-Ideal and
A27: c1 = c \/ {r} by A12,A18,A22; c c= c1 by A27,XBOOLE_1:7;
hence F.i c= F.(i+1) by A19,A20,A21,A23,A24,A25,Th57;
A28: c1 c= c1-Ideal by A24,A25,Def15; r in {r} by TARSKI:def 1;
then r in c1 by A27,XBOOLE_0:def 2;
hence F.i <> F.(i+1) by A19,A23,A26,A28,XBOOLE_0:def 4;
end;
then A29: P[0];
A30: for i being Nat st P[i] holds P[i+1] proof
let i be Nat such that
A31: F.j c= F.(j+1+i) and
A32: F.j <> F.(j+1+i);
F.(j+1+i) c< F.((j+1+i)+1) by A17;
then F.(j+1+i) c= F.((j+1+i)+1) by XBOOLE_0:def 8;
then A33: F.(j+1+i) c= F.(j+1+(i+1)) by XCMPLX_1:1;
hence F.j c= F.(j+1+(i+1)) by A31,XBOOLE_1:1;
not F.(j+1+i) c= F.j by A31,A32,XBOOLE_0:def 10;
then consider x being set such that
A34: x in F.(j+1+i) and
A35: not x in F.j by TARSKI:def 3;
thus thesis by A33,A34,A35;
end;
A36: for i being Nat holds P[i]
from Ind(A29, A30);
assume j < k; then j+1 <= k by NAT_1:38;
then consider i being Nat such that
A37: k = j + 1 + i by NAT_1:28;
thus thesis by A36,A37;
end;
hence contradiction by A1,A16;
end;