:: Construction of Rings and Left-, Right-, and Bi-Modules over a Ring
:: by Micha{\l} Muzalewski
::
:: Received June 20, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ALGSTR_0, VECTSP_1, MESFUNC1, GROUP_1, SUBSET_1,
RELAT_1, STRUCT_0, RLVECT_1, LATTICES, FUNCSDOM, BINOP_1, SUPINF_2,
ARYTM_3, ARYTM_1, FUNCT_1, ZFMISC_1, FUNCT_5, MCART_1, VECTSP_2, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_2, BINOP_1,
FUNCT_5, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM,
FUNCT_3;
constructors FUNCT_3, VECTSP_1, FUNCSDOM, FUNCT_5, NUMBERS, GROUP_1;
registrations XBOOLE_0, STRUCT_0, VECTSP_1, ALGSTR_0;
requirements SUBSET, BOOLE;
definitions VECTSP_1, RLVECT_1, STRUCT_0, ALGSTR_0;
equalities VECTSP_1, STRUCT_0, ALGSTR_0, ORDINAL1;
expansions VECTSP_1, RLVECT_1, ALGSTR_0;
theorems VECTSP_1, TARSKI, RLVECT_1, GROUP_1, ALGSTR_0;
begin :: 1. RING
reserve FS for non empty doubleLoopStr;
reserve F for Field;
Lm1: for L being non empty multLoopStr st L is well-unital holds 1.(L) = 1_L
by GROUP_1:def 4;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
unital distributive for non empty doubleLoopStr;
existence
proof
set F = the strict Field;
F is unital distributive;
hence thesis;
end;
end;
definition
let IT be non empty multLoopStr_0;
attr IT is domRing-like means :Def1:
for x,y being Element of IT holds x*y = 0.IT implies x = 0.IT or y = 0.IT;
end;
registration
cluster strict non degenerated commutative almost_left_invertible
domRing-like for Ring;
existence
proof
set F = the strict Field;
for x,y being Scalar of F holds x*y = 0.F implies x = 0.F or y = 0.F
by VECTSP_1:12; then
F is domRing-like;
hence thesis;
end;
end;
definition
mode comRing is commutative Ring;
end;
definition
mode domRing is domRing-like non degenerated comRing;
end;
theorem
F is domRing
proof
for x,y being Scalar of F holds x*y = 0.F implies x = 0.F or y = 0.F
by VECTSP_1:12;
hence thesis by Def1;
end;
:: 10. AXIOMS OF SKEW-FIELD
registration
cluster commutative left_unital -> well-unital for non empty multLoopStr;
coherence
proof
let F be non empty multLoopStr;
assume
A1: F is commutative left_unital;
let x be Scalar of F;
for F be commutative non empty multMagma, x,y being Element of F
holds x*y = y*x;
then x*(1.F) = (1.F)*x by A1;
hence thesis by A1;
end;
cluster commutative right_unital -> well-unital for non empty multLoopStr;
coherence
proof
let F be non empty multLoopStr;
assume
A2: F is commutative right_unital;
let x be Element of F;
for F be commutative non empty multMagma, x,y being Element of F
holds x*y = y*x;
then x*(1.F) = (1.F)*x by A2;
hence thesis by A2;
end;
end;
:: 11. SOME PROPERTIES OF RING
reserve R for Abelian add-associative right_zeroed right_complementable non
empty addLoopStr,
x, y, z for Scalar of R;
Lm2: x + y = z implies x = z - y
proof
assume
A1: x + y = z;
thus x = x + 0.R by RLVECT_1:4
.= x + (y + -y) by RLVECT_1:def 10
.= z - y by A1,RLVECT_1:def 3;
end;
Lm3: x = z - y implies x + y = z
proof
assume x = z - y;
then x + y = z + (y + -y) by RLVECT_1:def 3
.= z + 0.R by RLVECT_1:def 10
.= z by RLVECT_1:4;
hence thesis;
end;
theorem
(x + y = z iff x = z - y) & (x + y = z iff y = z - x) by Lm2,Lm3;
theorem Th3:
for R being add-associative right_zeroed right_complementable
non empty addLoopStr, x being Element of R holds x=0.R iff -x=0.R
proof
let R be add-associative right_zeroed right_complementable non empty
addLoopStr, x be Element of R;
thus x=0.R implies -x=0.R by RLVECT_1:12;
assume -x = 0.R;
then -(-x) = 0.R by RLVECT_1:12;
hence thesis by RLVECT_1:17;
end;
theorem
for R being add-associative right_zeroed Abelian right_complementable
non empty addLoopStr
for x,y being Element of R
ex z being Element of R st x = y+z & x = z+y
proof
let R be add-associative right_zeroed Abelian right_complementable non
empty addLoopStr;
let x,y be Element of R;
take z = -y+x;
z+y = x+(-y+y) by RLVECT_1:def 3
.= x+0.R by RLVECT_1:5
.= x by RLVECT_1:4;
hence thesis;
end;
:: 12. SOME PROPERTIES OF SKEW-FIELD
reserve SF for Skew-Field,
x, y, z for Scalar of SF;
theorem
for F being add-associative right_zeroed right_complementable
distributive non degenerated non empty doubleLoopStr
for x, y being Element of F holds x*y = 1.F implies x<>0.F & y<>0.F;
theorem Th6:
for SF being non degenerated almost_left_invertible associative
add-associative right_zeroed right_complementable well-unital
distributive non empty doubleLoopStr,
x being Element of SF holds x<>0.SF implies
ex y being Element of SF st x*y = 1.SF
proof
let SF be non degenerated almost_left_invertible associative add-associative
right_zeroed right_complementable well-unital right_unital distributive non
empty doubleLoopStr, x be Element of SF;
assume x<>0.SF;
then consider y be Element of SF such that
A1: y*x = 1.SF by VECTSP_1:def 9;
take y;
y<>0.SF by A1;
then consider z be Element of SF such that
A2: z*y = 1.SF by VECTSP_1:def 9;
z = z*(y*x) by A1
.= 1.SF*x by A2,GROUP_1:def 3
.= x;
hence thesis by A2;
end;
theorem Th7:
for SF being add-associative right_zeroed right_complementable
distributive non degenerated almost_left_invertible associative well-unital
non empty doubleLoopStr
for x,y being Element of SF st y*x = 1.SF holds x*y = 1.SF
proof
let SF be non degenerated almost_left_invertible associative add-associative
right_zeroed right_complementable well-unital distributive non empty
doubleLoopStr;
let x,y be Element of SF;
assume
A1: y*x = 1.SF;
then x<>0.SF;
then consider z being Element of SF such that
A2: x*z = 1_SF by Th6;
y = y*(x*z) by A2
.= 1_SF*z by A1,GROUP_1:def 3
.= z;
hence thesis by A2;
end;
theorem Th8:
for SF being non degenerated almost_left_invertible associative
Abelian add-associative right_zeroed right_complementable well-unital
distributive non empty doubleLoopStr, x,y,z being Element of SF holds x * y =
x * z & x<>0.SF implies y = z
proof
let SF be non degenerated almost_left_invertible associative Abelian
add-associative right_zeroed right_complementable well-unital distributive non
empty doubleLoopStr, x,y,z be Element of SF;
assume that
A1: x * y = x * z and
A2: x<>0.SF;
consider u being Element of SF such that
A3: x * u = 1_SF by A2,Th6;
A4: u * x = 1_SF by A3,Th7;
then y = (u*x)*y
.= u*(x*z) by A1,GROUP_1:def 3
.= 1_SF*z by A4,GROUP_1:def 3
.= z;
hence thesis;
end;
notation
let SF be non degenerated almost_left_invertible associative add-associative
right_zeroed right_complementable well-unital distributive non empty
doubleLoopStr, x be Element of SF;
synonym x" for /x;
end;
definition
let SF be non degenerated almost_left_invertible associative add-associative
right_zeroed right_complementable well-unital distributive non empty
doubleLoopStr, x be Element of SF;
assume
A1: x<>0.SF;
redefine func x" means :Def2: :: redefines " (VECTSP_2, synonym) → / (ALGSTR_0, definition)
it * x = 1.SF;
compatibility
proof
let IT be Element of SF;
A2: x is left_invertible by A1,ALGSTR_0:def 39;
then consider y being Element of SF such that
A3: y*x = 1.SF;
x is right_invertible
proof
take y;
thus thesis by A3,Th7;
end;
then consider x1 being Element of SF such that
A4: x*x1 = 1.SF;
x is right_mult-cancelable
proof
let y,z be Element of SF;
assume
A5: y*x = z*x;
thus y = y * 1.SF
.= z * x*x1 by A4,A5,GROUP_1:def 3
.= z * 1.SF by A4,GROUP_1:def 3
.= z;
end;
hence thesis by A2,ALGSTR_0:def 30;
end;
end;
:: definition
:: let SF,x,y;
:: func x/y -> Scalar of SF equals
:: x * y";
:: correctness;
:: end;
::$CD
theorem Th9:
x<>0.SF implies x * x" = 1.SF & x" * x = 1.SF
proof
assume x<>0.SF;
then x"*x = 1_SF by Def2;
hence thesis by Th7;
end;
theorem Th10:
y*x = 1_SF implies x = y" & y = x"
proof
A1: y*x = 1_SF implies y = x"
proof
assume
A2: y*x = 1_SF;
then x<>0.SF;
hence thesis by A2,Def2;
end;
y*x = 1_SF implies x = y"
proof
assume y*x = 1_SF;
then y<>0.SF & x*y = 1_SF by Th7;
hence thesis by Def2;
end;
hence thesis by A1;
end;
theorem Th11:
x<>0.SF & y<>0.SF implies x"*y"=(y*x)"
proof
assume
A1: x<>0.SF;
assume
A2: y<>0.SF;
x"*y"*(y*x) =x"*(y"*(y*x)) by GROUP_1:def 3
.=x"*(y"*y*x) by GROUP_1:def 3
.=x"*(1_SF*x) by A2,Th9
.=x"*x
.=1_SF by A1,Th9;
hence thesis by Th10;
end;
theorem
x*y = 0.SF implies x = 0.SF or y = 0.SF
proof
now
assume that
A1: x*y = 0.SF and
A2: x <> 0.SF;
x*y = x*(0.SF) by A1;
hence y = 0.SF by A2,Th8;
end;
hence thesis;
end;
theorem Th13:
x<>0.SF implies x"<>0.SF
proof
assume
A1: x<>0.SF;
assume x"=0.SF;
then x*x"=0.SF;
then 1.SF=0.SF by A1,Th9;
hence contradiction;
end;
theorem Th14:
x<>0.SF implies x""=x
proof
assume
A1: x<>0.SF;
then
A2: x"<>0.SF by Th13;
x""=x""*1_SF
.=x"" * (x" * x) by A1,Th9
.=x""*x"*x by GROUP_1:def 3;
then x""=1_SF*x by A2,Th9;
hence thesis;
end;
theorem
x<>0.SF implies (1_SF)/x=x" & (1_SF)/x"=x by Th14;
theorem
x<>0.SF implies x*((1_SF)/x)=1_SF & ((1_SF)/x)*x=1_SF by Th9;
theorem
x<>0.SF implies x/x = 1_SF by Th9;
theorem Th18:
y<>0.SF & z<>0.SF implies x/y=(x*z)/(y*z)
proof
assume
A1: y<>0.SF;
assume
A2: z<>0.SF;
thus x/y=x*1_SF*y"
.=x*(z*z")*y" by A2,Th9
.=(x*z)*z"*y" by GROUP_1:def 3
.=(x*z)*(z"*y") by GROUP_1:def 3
.=(x*z)/(y*z) by A1,A2,Th11;
end;
theorem Th19:
y<>0.SF implies -x/y=(-x)/y & x/(-y)=-x/y
proof
assume y<>0.SF;
then
A1: -y<>0.SF by Th3;
thus
A2: -x/y=(-x)/y by VECTSP_1:9;
-1.SF<>0.SF by Th3;
then x/(-y)=(x*(-1_SF))/((-y)*(-1_SF)) by A1,Th18;
then x/(-y)=(-x*1_SF)/((-y)*(-1_SF)) by VECTSP_1:8
.= (-x)/((-y)*(-1_SF))
.= (-x)/(-(-y)*1_SF) by VECTSP_1:8
.= (-x)/((-(-y))*1_SF)
.= (-x)/(y*1_SF) by RLVECT_1:17
.= -x/y by A2;
hence thesis;
end;
theorem
z<>0.SF implies x/z + y/z = (x+y)/z & x/z - y/z = (x-y)/z
proof
z<>0.SF implies x/z - y/z = (x-y)/z
proof
assume z<>0.SF;
hence x/z - y/z =x/z+(-y)/z by Th19
.=(x-y)/z by VECTSP_1:def 7;
end;
hence thesis by VECTSP_1:def 7;
end;
theorem
y<>0.SF & z<>0.SF implies x/(y/z)=(x*z)/y
proof
assume
A1: y<>0.SF;
assume
A2: z<>0.SF;
then z"<>0.SF by Th13;
hence x/(y/z)=x*(z""*y") by A1,Th11
.=x*(z*y") by A2,Th14
.=(x*z)/y by GROUP_1:def 3;
end;
theorem
y<>0.SF implies x/y*y=x
proof
assume
A1: y<>0.SF;
thus x/y*y=x*(y"*y) by GROUP_1:def 3
.=x*1_SF by A1,Th9
.=x;
end;
:: 13. LEFT-, RIGHT-, AND BI-MODULE STRUCTURE
definition
let FS be 1-sorted;
struct(addLoopStr) RightModStr over FS (#
carrier -> set,
addF -> BinOp of the carrier,
ZeroF -> Element of the carrier,
rmult -> Function of [: the carrier, the carrier of FS:], the carrier #);
end;
registration
let FS be 1-sorted;
cluster non empty for RightModStr over FS;
existence
proof
set A = the non empty set,a = the BinOp of A,Z = the Element of A,
r =the Function of [:A,the carrier of FS:],A;
take RightModStr(#A,a,Z,r#);
thus the carrier of RightModStr(#A,a,Z,r#) is non empty;
end;
end;
registration
let FS be 1-sorted;
let A be non empty set, a be BinOp of A, Z be Element of A,
r be Function of [:A,the carrier of FS:],A;
cluster RightModStr(#A,a,Z,r#) -> non empty;
coherence;
end;
definition
let FS;
let RMS be non empty RightModStr over FS;
mode Scalar of RMS is Element of FS;
mode Vector of RMS is Element of RMS;
end;
definition
let FS1,FS2 be 1-sorted;
struct (ModuleStr over FS1, RightModStr over FS2) BiModStr over FS1,FS2 (#
carrier -> set,
addF -> BinOp of the carrier,
ZeroF -> Element of the carrier,
lmult -> Function of [:the carrier of FS1, the carrier:], the carrier,
rmult -> Function of [:the carrier, the carrier of FS2:], the carrier #);
end;
registration
let FS1,FS2 be 1-sorted;
cluster non empty for BiModStr over FS1,FS2;
existence
proof
set A = the non empty set,a = the BinOp of A,Z = the Element of A,
l =the Function of [:the carrier of FS1,A:],A,
r = the Function of [:A,the carrier of FS2:],A;
take BiModStr(#A,a,Z,l,r#);
thus the carrier of BiModStr(#A,a,Z,l,r#) is non empty;
end;
end;
registration
let FS1,FS2 be 1-sorted;
let A be non empty set, a be BinOp of A, Z be Element of A,
l be Function of [:the carrier of FS1,A:],A,
r be Function of [:A,the carrier of FS2:],A;
cluster BiModStr(#A,a,Z,l,r#) -> non empty;
coherence;
end;
:: 14. PREDE LEFT-MODULE OF RING
reserve R, R1, R2 for Ring;
definition
let R be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr;
func AbGr R -> strict AbGroup equals
addLoopStr (#the carrier of R, the addF of R, 0.R#);
coherence
proof
reconsider IT = addLoopStr(# the carrier of R,the addF of R,0.R #) as non
empty addLoopStr;
A1: for x,y,z being Element of IT holds x+y = y+x & (x+y)+z = x+(y+z) & x+
(0.IT) = x & ex v being Element of IT st x+v = 0.IT
proof
let x,y,z be Element of IT;
reconsider x9=x,y9=y,z9=z as Scalar of R;
thus x+y = y9+x9 by RLVECT_1:2
.= y+x;
thus (x+y)+z = (x9+y9)+z9 .= x9+(y9+z9) by RLVECT_1:def 3
.= x+(y+z);
thus x+0.IT = x9+(0.R) .= x by RLVECT_1:4;
consider b being Scalar of R such that
A2: x9 + b = 0.R by ALGSTR_0:def 11;
reconsider b9 = b as Element of IT;
take b9;
thus thesis by A2;
end;
IT is right_complementable
proof
let x be Element of IT;
reconsider x9=x as Scalar of R;
consider b being Scalar of R such that
A3: x9 + b = 0.R by ALGSTR_0:def 11;
reconsider b9 = b as Element of IT;
take b9;
thus thesis by A3;
end;
hence thesis by A1,RLVECT_1:def 2,def 3,def 4;
end;
end;
deffunc LEFTMODULE(Ring) = ModuleStr(# the carrier of $1,the addF of $1, 0.$1,
the multF of $1 #);
Lm4: LEFTMODULE(R) is Abelian add-associative right_zeroed right_complementable
proof
A1: for x,y,z being Scalar of R for x9,y9,z9 be Element of LEFTMODULE(R) st
x = x9 & y = y9 & z = z9 holds x + y = x9+ y9;
thus LEFTMODULE(R) is Abelian
proof
let x,y be Element of LEFTMODULE(R);
reconsider x9= x, y9= y as Scalar of R;
thus x+y = y9+ x9 by A1
.= y + x;
end;
thus LEFTMODULE(R) is add-associative
proof
let x,y,z be Element of LEFTMODULE(R);
reconsider x9= x, y9= y, z9= z as Scalar of R;
thus (x+y)+z = (x9+ y9) + z9 .= x9+ (y9+ z9) by RLVECT_1:def 3
.= x + (y + z);
end;
thus LEFTMODULE(R) is right_zeroed
proof
let x be Element of LEFTMODULE(R);
reconsider x9= x as Scalar of R;
thus x+(0.(LEFTMODULE(R))) = x9+ (0.R) .= x by RLVECT_1:4;
end;
let x be Element of LEFTMODULE(R);
reconsider x9= x as Scalar of R;
consider b9 being Scalar of R such that
A2: x9 + b9 = 0.R by ALGSTR_0:def 11;
reconsider b = b9 as Element of LEFTMODULE(R);
take b;
thus thesis by A2;
end;
registration
let R;
cluster Abelian add-associative right_zeroed right_complementable strict for
non empty ModuleStr over R;
existence
proof
LEFTMODULE(R) is Abelian add-associative right_zeroed
right_complementable by Lm4;
hence thesis;
end;
end;
definition
let R;
func LeftModule R -> Abelian add-associative right_zeroed
right_complementable strict non empty ModuleStr over R equals
ModuleStr (# the carrier of R, the addF of R, 0.R, the multF of R #);
coherence by Lm4;
end;
deffunc RIGHTMODULE(Ring) = RightModStr(# the carrier of $1,the addF of $1, 0.
$1, the multF of $1 #);
Lm5: RIGHTMODULE (R) is Abelian add-associative right_zeroed
right_complementable
proof
A1: for x,y,z being Scalar of R for x9,y9,z9 be Element of RIGHTMODULE(R) st
x = x9 & y = y9 & z = z9 holds x + y = x9+ y9;
thus RIGHTMODULE(R) is Abelian
proof
let x,y be Element of RIGHTMODULE(R);
reconsider x9= x, y9= y as Scalar of R;
thus x+y = y9+ x9 by A1
.= y + x;
end;
thus RIGHTMODULE(R) is add-associative
proof
let x,y,z be Element of RIGHTMODULE(R);
reconsider x9= x, y9= y, z9= z as Scalar of R;
thus (x+y)+z = (x9+ y9) + z9 .= x9+ (y9+ z9) by RLVECT_1:def 3
.= x + (y + z);
end;
thus RIGHTMODULE(R) is right_zeroed
proof
let x be Element of RIGHTMODULE(R);
reconsider x9= x as Scalar of R;
thus x+(0.(RIGHTMODULE(R))) = x9+ (0.R) .= x by RLVECT_1:4;
end;
let x be Element of RIGHTMODULE(R);
reconsider x9= x as Scalar of R;
consider b9 being Scalar of R such that
A2: x9 + b9 = 0.R by ALGSTR_0:def 11;
reconsider b = b9 as Element of RIGHTMODULE(R);
take b;
thus thesis by A2;
end;
registration let R;
cluster Abelian add-associative right_zeroed right_complementable strict for
non empty RightModStr over R;
existence
proof
RIGHTMODULE(R) is Abelian add-associative right_zeroed
right_complementable by Lm5;
hence thesis;
end;
end;
definition let R;
func RightModule R -> Abelian add-associative right_zeroed
right_complementable strict non empty RightModStr over R equals
RightModStr
(# the carrier of R, the addF of R, 0.R, the multF of R #);
coherence by Lm5;
end;
definition
let R be non empty 1-sorted, V be non empty RightModStr over R;
let x be Element of R;
let v be Element of V;
func v*x -> Element of V equals
(the rmult of V).(v,x);
coherence;
end;
deffunc BIMODULE(Ring,Ring) = BiModStr(# {0},op2,op0,
pr2 (the carrier of $1,{0}), pr1 ({0},the carrier of $2) #);
Lm6: BIMODULE (R1,R2) is Abelian add-associative right_zeroed
right_complementable
proof
set G = BiModStr(#{0},op2,op0,pr2 (the carrier of R1, {0}),
pr1 ({0},the carrier of R2) #);
A1: now
let x,y,z be Element of G;
A2: x+(0.G) = {} by TARSKI:def 1;
x+y = {} & (x+y)+z = {} by TARSKI:def 1;
hence x+y = y+x & (x+y)+z = x+(y+z) & x+(0.G) = x & ex x9 being Element of
G st x+x9 = 0.G by A2,TARSKI:def 1;
end;
G is right_complementable
proof
let x be Element of G;
take x;
thus thesis by TARSKI:def 1;
end;
hence thesis by A1;
end;
registration let R1,R2;
cluster Abelian add-associative right_zeroed right_complementable strict for
non empty BiModStr over R1,R2;
existence
proof
BIMODULE(R1,R2) is Abelian add-associative right_zeroed
right_complementable by Lm6;
hence thesis;
end;
end;
definition let R1,R2;
func BiModule(R1,R2) -> Abelian add-associative right_zeroed
right_complementable strict non empty BiModStr over R1,R2 equals
BiModStr (#{0},op2,op0,
pr2(the carrier of R1, {0}), pr1({0},the carrier of R2) #);
coherence by Lm6;
end;
theorem Th23:
for x,y being Scalar of R for v,w being Vector of LeftModule R
holds x*(v+w) = x*v+x*w & (x+y)*v = x*v+y*v & (x*y)*v = x*(y*v) & (1.R)*v = v
proof
set MLT = the multF of R;
set LS = ModuleStr (# the carrier of R,the addF of R, 0.R,MLT #);
for x,y being Scalar of R for v,w being Vector of LS holds x*(v+w) = x*v
+x*w & (x+y)*v = x*v+y*v & (x*y)*v = x*(y*v) & (1_R)*v = v
proof
let x,y be Scalar of R;
let v,w be Vector of LS;
reconsider v9 = v, w9 = w as Scalar of R;
thus x*(v+w) = x*(v9+w9) .= x*v9+x*w9 by VECTSP_1:def 7
.= x*v+x*w;
thus (x+y)*v = (x+y)*v9 .= x*v9+y*v9 by VECTSP_1:def 7
.= x*v+y*v;
thus (x*y)*v = (x*y)*v9 .= x*(y*v9) by GROUP_1:def 3
.= x*(y*v);
thus (1_R)*v = (1_R)*v9 .= v;
end;
hence thesis;
end;
registration
let R;
cluster vector-distributive scalar-distributive scalar-associative
scalar-unital Abelian add-associative right_zeroed
right_complementable strict for non empty ModuleStr over R;
existence
proof
take LeftModule R;
thus for x being Scalar of R for v,w being Vector of LeftModule R
holds x*(v+w) = x*v+x*w by Th23;
thus for x,y being Scalar of R for v being Vector of LeftModule R
holds (x+y)*v = x*v+y*v by Th23;
thus for x,y being Scalar of R for v being Vector of LeftModule R
holds (x*y)*v = x*(y*v) by Th23;
thus for v being Vector of LeftModule R holds (1.R)*v = v by Th23;
thus thesis;
end;
end;
definition
let R;
mode LeftMod of R is Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over R;
end;
Lm7: LeftModule R is vector-distributive scalar-distributive
scalar-associative scalar-unital
by Th23;
registration let R;
cluster LeftModule R -> Abelian add-associative right_zeroed
right_complementable strict vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence by Lm7;
end;
:: 18. AXIOMS OF LEFT MODULE OF RING
theorem Th24:
for x,y being Scalar of R for v,w being Vector of RightModule R holds
(v+w)*x = v*x+w*x & v*(x+y) = v*x+v*y & v*(y*x) = (v*y)*x & v*(1_R) = v
proof
set MLT = the multF of R;
set LS = RightModStr (# the carrier of R,the addF of R,0.R,MLT #);
for x,y being Scalar of R for v,w being Vector of LS holds (v+w)*x = v*x
+w*x & v*(x+y) = v*x+v*y & v*(y*x) = (v*y)*x & v*(1_R) = v
proof
let x,y be Scalar of R;
let v,w be Vector of LS;
reconsider v9 = v, w9 = w as Scalar of R;
thus (v+w)*x = (v9+w9)*x .= v9*x+w9*x by VECTSP_1:def 7
.= v*x+w*x;
thus v*(x+y) = v9*(x+y) .= v9*x+v9*y by VECTSP_1:def 7
.= v*x+v*y;
thus v*(y*x) = v9*(y*x) .= (v9*y)*x by GROUP_1:def 3
.= (v*y)*x;
thus v*(1_R) = v9*(1_R) .= v;
end;
hence thesis;
end;
definition
let R be non empty doubleLoopStr;
let IT be non empty RightModStr over R;
attr IT is RightMod-like means :Def8:
for x,y being Scalar of R for v,w being Vector of IT holds
(v+w)*x = v*x+w*x & v*(x+y) = v*x+v*y &
v*(y*x) = (v*y)*x & v*(1_R) = v;
end;
registration let R;
cluster Abelian add-associative right_zeroed right_complementable
RightMod-like strict for non empty RightModStr over R;
existence
proof
take RightModule R;
thus RightModule R is Abelian add-associative right_zeroed
right_complementable;
thus for x,y being Scalar of R for v,w being Vector of RightModule R holds
(v+w)*x = v*x+w*x & v*(x+y) = v*x+v*y & v*(y*x) = (v*y)*x & v*(1_R) = v by Th24
;
thus thesis;
end;
end;
definition
let R;
mode RightMod of R is Abelian add-associative right_zeroed
right_complementable RightMod-like non empty RightModStr over R;
end;
Lm8: RightModule R is RightMod-like by Th24;
registration let R;
cluster RightModule R -> Abelian add-associative right_zeroed
right_complementable RightMod-like;
coherence by Lm8;
end;
:: 20. AXIOMS OF RIGHT MODULE OF RING
Lm9: for x,y being Scalar of R1 for p,q being Scalar of R2 for v,w being
Vector of BiModule(R1,R2) holds x*(v+w) = x*v+x*w & (x+y)*v = x*v+y*v & (x*y)*v
= x*(y*v) & (1_R1)*v = v & (v+w)*p = v*p+w*p & v*(p+q) = v*p+v*q & v*(q*p) = (v
*q)*p & v*(1_R2) = v & x*(v*p) = (x*v)*p
proof
set a = {};
set G = BiModule(R1,R2);
let x,y be Scalar of R1, p,q be Scalar of R2, v,w be Vector of G;
A1: (x*y)*v = a & (1_R1)*v = a by TARSKI:def 1;
x*(v+w) = a & (x+y)*v = a by TARSKI:def 1;
hence x*(v+w) = x*v+x*w & (x+y)*v = x*v+y*v & (x*y)*v = x*(y*v) & (1_R1)*v =
v by A1,TARSKI:def 1;
A2: v*(q*p) = a & v*(1_R2) = a by TARSKI:def 1;
A3: x*(v*p) = a by TARSKI:def 1;
(v+w)*p = a & v*(p+q) = a by TARSKI:def 1;
hence thesis by A2,A3,TARSKI:def 1;
end;
definition
let R1, R2 be non empty multMagma;
let IT be non empty BiModStr over R1,R2;
attr IT is BiMod-like means :Def9:
for x being Scalar of R1 for p being
Scalar of R2 for v being Vector of IT holds x*(v*p) = (x*v)*p;
end;
registration let R1,R2;
cluster Abelian add-associative right_zeroed right_complementable
RightMod-like vector-distributive scalar-distributive scalar-associative
scalar-unital BiMod-like strict for non empty BiModStr over R1,R2;
existence
proof
take BiModule (R1,R2);
thus BiModule (R1,R2) is Abelian add-associative right_zeroed
right_complementable;
for x,y being Scalar of R1 for p,q being Scalar of R2 for v,w being
Vector of BiModule(R1,R2) holds x*(v+w) = x*v+x*w & (x+y)*v = x*v+y*v & (x*y)*v
= x*(y*v) & (1_R1)*v = v & (v+w)*p = v*p+w*p & v*(p+q) = v*p+v*q & v*(q*p) = (v
*q)*p & v*(1_R2) = v & x*(v*p) = (x*v)*p by Lm9;
hence thesis;
end;
end;
definition let R1,R2;
mode BiMod of R1,R2 is Abelian add-associative right_zeroed
right_complementable RightMod-like vector-distributive scalar-distributive
scalar-associative scalar-unital BiMod-like non empty BiModStr over R1,R2;
end;
theorem
for V being non empty BiModStr over R1,R2 holds
(for x,y being Scalar of R1
for p,q being Scalar of R2
for v,w being Vector of V holds x*(v+w) = x*v+x*w & (x+y)*v = x*v+y*v &
(x*y)*v = x*(y*v) & (1_R1)*v = v & (v+w)*p = v*p+w*p &
v*(p+q) = v*p+v*q & v*(q*p) = (v*q)*p & v*(1_R2) = v & x*(v*p) = (x*v)*p)
iff
V is RightMod-like vector-distributive scalar-distributive
scalar-associative scalar-unital BiMod-like;
theorem Th26:
BiModule(R1,R2) is BiMod of R1,R2
proof
for x,y being Scalar of R1, p,q being Scalar of R2, v,w being Vector of
BiModule(R1,R2) holds x*(v+w) = x*v+x*w & (x+y)*v = x*v+y*v & (x*y)*v = x*(y*v)
& (1_R1)*v = v & (v+w)*p = v*p+w*p & v*(p+q) = v*p+v*q & v*(q*p) = (v*q)*p & v*
(1_R2) = v & x*(v*p) = (x*v)*p by Lm9;
hence thesis by Def8,Def9,VECTSP_1:def 14,def 15,def 16,def 17;
end;
registration let R1,R2;
cluster BiModule(R1,R2) -> Abelian add-associative right_zeroed
right_complementable RightMod-like vector-distributive scalar-distributive
scalar-associative scalar-unital BiMod-like;
coherence by Th26;
end;
theorem
for L being non empty multLoopStr st L is well-unital holds 1.(L) =
1_L by Lm1;
begin :: MOD_1
theorem
for K be add-associative right_zeroed right_complementable
right-distributive right_unital non empty doubleLoopStr
for a be Element of K holds a * (- 1.K) = - a
proof
let K be add-associative right_zeroed right_complementable
right-distributive right_unital non empty doubleLoopStr;
let x be Element of K;
thus x * (- 1.K) = x * (0.K - 1.K) by RLVECT_1:14
.= x * 0.K - x * 1.K by VECTSP_1:11
.= 0.K - x * 1.K
.= - x * 1.K by RLVECT_1:14
.= - x;
end;
theorem
for K be add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr
for a be Element of K holds (- 1.K) * a = - a
proof
let K be add-associative right_zeroed right_complementable left-distributive
left_unital non empty doubleLoopStr;
let x be Element of K;
thus (- 1.K) * x = (0.K - 1.K) * x by RLVECT_1:14
.= 0.K * x - 1.K * x by VECTSP_1:13
.= 0.K - 1.K * x
.= - 1.K * x by RLVECT_1:14
.= - x;
end;
reserve R for Abelian add-associative right_zeroed right_complementable
associative well-unital right_unital distributive non empty doubleLoopStr,
F for non degenerated almost_left_invertible Ring,
x for Scalar of F,
V for add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital
non empty
ModuleStr over F,
v for Vector of V;
theorem
x*v = 0.V iff x = 0.F or v = 0.V
proof
x*v = 0.V implies x = 0.F or v = 0.V
proof
assume x*v = 0.V;
then
A1: (x"*x)*v = x"*(0.V) by VECTSP_1:def 16
.= 0.V by VECTSP_1:14;
assume x<> 0.F;
then 0.V = (1_F)*v by A1,Th9;
hence thesis by VECTSP_1:def 17;
end;
hence thesis by VECTSP_1:14;
end;
theorem
x<>0.F implies x"*(x*v)=v
proof
assume
A1: x<>0.F;
x"*(x*v) = (x"*x)*v by VECTSP_1:def 16
.= 1_F *v by A1,Th9
.= v by VECTSP_1:def 17;
hence thesis;
end;
reserve V for add-associative right_zeroed right_complementable RightMod-like
non empty RightModStr over R;
reserve x for Scalar of R;
reserve v,w for Vector of V;
theorem Th32:
v*(0.R) = 0.V & v*(-1_R) = -v & (0.V)*x = 0.V
proof
v + v*(0.R) = v* (1_R) + v*(0.R) by Def8
.= v*((1_R) + (0.R)) by Def8
.= v*(1_R) by RLVECT_1:4
.= v by Def8
.= v + 0.V by RLVECT_1:4;
hence
A1: v*(0.R) = 0.V by RLVECT_1:8;
v*(-(1_R)) + v = v*( -(1_R)) + v* (1_R) by Def8
.= v*((-(1_R)) + (1_R)) by Def8
.= 0.V by A1,RLVECT_1:5;
then v*(-(1_R)) + (v + -v) = 0.V + -v by RLVECT_1:def 3;
then 0.V + -v = v*(-(1_R)) + 0.V by RLVECT_1:5
.= v*(-(1_R)) by RLVECT_1:4;
hence v*(-1_R) = -v by RLVECT_1:4;
(0.V)*x = v*((0.R) *x) by A1,Def8
.= 0.V by A1;
hence thesis;
end;
theorem Th33:
-v*x = v*(-x) & w - v*x = w + v*(-x)
proof
A1: -v*x = (v*x) * (-1_R) by Th32
.= v*(x* (-1_R)) by Def8
.= v*(-(x* 1_R)) by VECTSP_1:8;
hence -v* x = v*(-x);
thus thesis by A1;
end;
theorem Th34:
(-v)*x = -v*x
proof
(-v)*x = (v*(-1_R))*x by Th32
.= v*((-1_R) *x) by Def8
.= v*(-(1_R *x)) by VECTSP_1:9
.= v*(-x);
hence thesis by Th33;
end;
theorem
(v - w)*x = v*x - w*x
proof
(v - w)*x = (v + (-w))*x .= v*x + (-w) *x by Def8
.= v*x + (-w * x) by Th34;
hence thesis;
end;
reserve F for non degenerated almost_left_invertible Ring;
reserve x for Scalar of F;
reserve V for add-associative right_zeroed right_complementable RightMod-like
non empty RightModStr over F;
reserve v for Vector of V;
theorem
v*x = 0.V iff x = 0.F or v = 0.V
proof
v*x = 0.V implies x = 0.F or v = 0.V
proof
assume v*x = 0.V;
then
A1: v*(x*x") = (0.V)*x" by Def8
.= 0.V by Th32;
assume x<>(0.F);
then 0.V = v*(1_F) by A1,Th9;
hence thesis by Def8;
end;
hence thesis by Th32;
end;
theorem
x<>0.F implies (v*x)*x"=v
proof
assume
A1: x<>0.F;
(v*x)*x" = v*(x*x") by Def8
.= v* 1_F by A1,Th9
.= v by Def8;
hence thesis;
end;
registration
cluster almost_left_invertible -> domRing-like for associative well-unital
add-associative right_zeroed right_complementable right-distributive
non empty doubleLoopStr;
coherence
proof
let L be associative well-unital add-associative right_zeroed
right_complementable right-distributive non empty doubleLoopStr;
assume
A1: L is almost_left_invertible;
for x,y being Element of L holds x*y = 0.L implies x = 0.L or y = 0.L
proof
let x,y be Element of L;
assume
A2: x*y = 0.L;
now
assume that
A3: x <> 0.L and
A4: y <> 0.L;
consider xx being Element of L such that
A5: xx * x = 1.L by A1,A3;
y = 1.L * y
.= xx * (x * y) by A5,GROUP_1:def 3
.= 0.L by A2;
hence contradiction by A4;
end;
hence thesis;
end;
hence thesis;
end;
end;