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 doubleLoopS