Copyright (c) 1990 Association of Mizar Users
environ vocabulary VECTSP_1, RLVECT_1, LATTICES, ARYTM_1, FUNCSDOM, BINOP_1, RELAT_1, ARYTM_3, FUNCT_1, BOOLE, MIDSP_1, FUNCT_3, VECTSP_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_2, BINOP_1, STRUCT_0, RLVECT_1, VECTSP_1, FUNCSDOM, MIDSP_1, FUNCT_3; constructors BINOP_1, VECTSP_1, MIDSP_1, FUNCT_3, MEMBERED, XBOOLE_0; clusters VECTSP_1, STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions VECTSP_1, RLVECT_1, STRUCT_0; theorems VECTSP_1, FUNCT_2, TARSKI, RLVECT_1, STRUCT_0; begin :: 1. RING reserve FS for non empty doubleLoopStr; reserve F for Field; definition let IT be non empty multLoopStr; canceled; attr IT is well-unital means :Def2: for x being Element of IT holds x*(1_ IT) = x & (1_ IT)*x = x; end; definition cluster well-unital -> left_unital right_unital (non empty multLoopStr); coherence proof let F be non empty multLoopStr; assume A1: F is well-unital; hence for x being Element of F holds (1_ F)*x = x by Def2; thus for x being Element of F holds x*(1_ F) = x by A1,Def2; end; cluster left_unital right_unital -> well-unital (non empty multLoopStr); coherence proof let F be non empty multLoopStr; assume F is left_unital right_unital; hence for x being Element of F holds x*(1_ F) = x & (1_ F)*x = x by VECTSP_1:def 13,def 19; end; cluster strict Abelian add-associative right_zeroed right_complementable well-unital distributive (non empty doubleLoopStr); existence proof consider F being strict Field; for x,y,z being Scalar of F holds x+y = y+x & (x+y)+z = x+(y+z) & x+(0.F) = x & x+(-x) = 0.F & x*(1_ F) = x & (1_ F)*x = x & x*(y+z) = x*y+x*z & (y+z)*x = y*x+z*x by RLVECT_1:10,def 6,def 10,VECTSP_1:def 18,def 19; then F is well-unital distributive by Def2; hence thesis; end; end; theorem (for x,y,z being Scalar of FS holds x+y = y+x & (x+y)+z = x+(y+z) & x+(0.FS) = x & x+(-x) = 0.FS & x*(1_ FS) = x & (1_ FS)*x = x & (x*y)*z = x*(y*z) & x*(y+z) = x*y+x*z & (y+z)*x = y*x+z*x) iff FS is Ring proof thus (for x,y,z being Scalar of FS holds x+y = y+x & (x+y)+z = x+(y+z) & x+(0.FS) = x & x+(-x) = 0.FS & x*(1_ FS) = x & (1_ FS)*x = x & (x*y)*z = x*(y*z) & x*(y+z) = x*y+x*z & (y+z)*x = y*x+z*x) implies FS is Ring proof assume A1: for x,y,z being Scalar of FS holds x+y = y+x & (x+y)+z = x+(y+z) & x+(0.FS) = x & x+(-x) = 0.FS & x*(1_ FS) = x & (1_ FS)*x = x & (x*y)*z = x*(y*z) & x*(y+z) = x*y+x*z & (y+z)*x = y*x+z*x; FS is right_complementable proof let v be Element of FS; take -v; thus v + -v = 0.FS by A1; end; hence thesis by A1,RLVECT_1:def 5,def 6,def 7,VECTSP_1:def 13,def 16,def 18, def 19; end; assume A2: FS is Ring; let x,y,z be Scalar of FS; thus thesis by A2,RLVECT_1:def 5,def 6,def 7,def 10,VECTSP_1:def 13,def 16,def 18,def 19; end; :: 3. RING definition cluster strict Ring; existence proof consider F being strict Field; reconsider F as Ring; F is associative; hence thesis; end; end; :: 5. COMMUTATIVE RING definition cluster commutative Ring; existence proof consider F; reconsider F as Ring; F is commutative; hence thesis; end; end; definition mode comRing is commutative Ring; end; definition cluster strict comRing; existence proof consider F being strict Field; reconsider F as Ring; F is comRing; hence thesis; end; end; definition let IT be non empty multLoopStr_0; canceled 2; attr IT is domRing-like means :Def5: for x,y being Element of IT holds x*y = 0.IT implies x = 0.IT or y = 0.IT; end; definition cluster strict non degenerated domRing-like comRing; existence proof consider F being strict Field; reconsider F as comRing; 0.F <> 1_ F & for x,y being Scalar of F holds x*y = 0.F implies x = 0.F or y = 0.F by VECTSP_1:44,def 21; then F is domRing-like by Def5; hence thesis; end; end; definition mode domRing is domRing-like non degenerated comRing; end; canceled 11; theorem F is domRing proof reconsider F as comRing; 0.F <> 1_ F & (for x,y being Scalar of F holds x*y = 0.F implies x = 0.F or y = 0.F) by VECTSP_1:44,def 21; hence thesis by Def5; end; definition cluster non degenerated Field-like Ring; existence proof consider F; F is Ring; hence thesis; end; end; definition mode Skew-Field is non degenerated Field-like Ring; end; definition cluster strict Skew-Field; existence proof consider F being strict Field; F is Ring; hence thesis; end; end; reserve R for Ring; canceled 2; theorem (for x being Scalar of R holds (x <> 0.R implies ex y be Scalar of R st x*y = 1_ R) & 0.R <> 1_ R ) implies R is Skew-Field by VECTSP_1:def 20,def 21; :: 10. AXIOMS OF SKEW-FIELD canceled 2; theorem F is Skew-Field; definition cluster commutative left_unital -> well-unital (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 HGrStr), x,y being Element of F holds x*y = y*x; then x*(1_ F) = (1_ F)*x by A1; hence x*(1_ F) = x & (1_ F)*x = x by A1,VECTSP_1:def 19; end; cluster commutative right_unital -> well-unital (non empty multLoopStr); coherence proof let F be non empty multLoopStr; assume A2: F is commutative right_unital; let x be Scalar of F; for F be commutative (non empty HGrStr), x,y being Element of F holds x*y = y*x; then x*(1_ F) = (1_ F)*x by A2; hence x*(1_ F) = x & (1_ F)*x = x by A2,VECTSP_1:def 13; end; end; :: 11. SOME PROPERTIES OF RING reserve R for Abelian add-associative right_zeroed right_complementable (non empty LoopStr), x, y, z for Scalar of R; Lm1: x + y = z implies x = z - y proof assume A1: x + y = z; thus x = x + 0.R by RLVECT_1:10 .= x + (y + -y) by RLVECT_1:def 10 .= z + (-y) by A1,RLVECT_1:def 6 .= z - y by RLVECT_1:def 11; end; Lm2: x = z - y implies x + y = z proof assume x = z - y; then x + y = (z + -y) + y by RLVECT_1:def 11 .= z + (y + -y) by RLVECT_1:def 6 .= z + 0.R by RLVECT_1:def 10 .= z by RLVECT_1:10; hence thesis; end; canceled 2; theorem (x + y = z iff x = z - y) & (x + y = z iff y = z - x) by Lm1,Lm2; canceled 11; theorem Th34: for R being add-associative right_zeroed right_complementable (non empty LoopStr), 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 LoopStr), x be Element of R; thus x=0.R implies -x=0.R by RLVECT_1:25; assume -x = 0.R; then -(-x) = 0.R by RLVECT_1:25; hence thesis by RLVECT_1:30; end; canceled 3; theorem for R being add-associative right_zeroed Abelian right_complementable (non empty LoopStr) 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 LoopStr); let x,y be Element of R; take z = -y+x; z+y = x+(-y+y) by RLVECT_1:def 6 .= x+0.R by RLVECT_1:16 .= x by RLVECT_1:10; hence thesis; end; :: 12. SOME PROPERTIES OF SKEW-FIELD reserve SF for Skew-Field, x, y, z for Scalar of SF; theorem Th39: 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 proof let F be add-associative right_zeroed right_complementable distributive non degenerated (non empty doubleLoopStr), x, y be Element of F; now A1: x = 0.F implies x*y <> 1_ F proof assume x = 0.F; then x*y = 0.F by VECTSP_1:39; hence thesis by VECTSP_1:def 21; end; y = 0.F implies x*y <> 1_ F proof assume y = 0.F; then x*y = 0.F by VECTSP_1:36; hence thesis by VECTSP_1:def 21; end; hence thesis by A1; end; hence thesis; end; theorem Th40: for SF being non degenerated Field-like associative Abelian 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 y*x = 1_ SF proof let SF be non degenerated Field-like associative Abelian add-associative right_zeroed right_complementable well-unital distributive (non empty doubleLoopStr), x be Element of SF; assume x<>0.SF; then consider y be Element of SF such that A1: x*y = 1_ SF by VECTSP_1:def 20; y<>0.SF by A1,Th39; then consider z be Element of SF such that A2: y*z = 1_ SF by VECTSP_1:def 20; A3: z = (x*y)*z by A1,Def2 .= x*1_ SF by A2,VECTSP_1:def 16 .= x by Def2; take y; thus thesis by A2,A3; end; theorem Th41: x*y = 1_ SF implies y*x = 1_ SF proof assume A1: x*y = 1_ SF; then x<>0.SF by Th39; then consider z such that A2: z*x = 1_ SF by Th40; y = (z*x)*y by A2,Def2 .= z*1_ SF by A1,VECTSP_1:def 16 .= z by Def2; hence thesis by A2; end; theorem Th42: for SF being non degenerated Field-like 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 Field-like 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: u * x = 1_ SF by A2,Th40; y = (u*x)*y by A3,Def2 .= u*(x*z) by A1,VECTSP_1:def 16 .= 1_ SF*z by A3,VECTSP_1:def 16 .= z by Def2; hence thesis; end; definition let SF be non degenerated Field-like associative Abelian add-associative right_zeroed right_complementable well-unital distributive (non empty doubleLoopStr), x be Element of SF; assume A1: x<>0.SF; canceled; func x" -> Scalar of SF means :Def7: x * it = 1_ SF; existence by A1,VECTSP_1:def 20; uniqueness by A1,Th42; end; definition let SF,x,y; func x/y -> Scalar of SF equals :Def8: x * y"; correctness; end; theorem Th43: x<>0.SF implies x * x" =1_ SF & x" * x =1_ SF proof assume x<>0.SF; then x * x" = 1_ SF by Def7; hence thesis by Th41; end; canceled; theorem Th45: x*y = 1_ SF implies x = y" & y = x" proof now A1: x*y = 1_ SF implies x = y" proof assume A2: x*y = 1_ SF; then A3: y<>0.SF by Th39; y*x = 1_ SF by A2,Th41; hence thesis by A3,Def7; end; x*y = 1_ SF implies y = x" proof assume A4: x*y = 1_ SF; then x<>0.SF by Th39; hence thesis by A4,Def7; end; hence thesis by A1; end; hence thesis; end; theorem Th46: 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 VECTSP_1:def 16 .=x"*(y"*y*x) by VECTSP_1:def 16 .=x"*(1_ SF*x) by A2,Th43 .=x"*x by Def2 .=1_ SF by A1,Th43; hence thesis by Th45; 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,VECTSP_1:36; hence y = 0.SF by A2,Th42; end; hence thesis; end; theorem Th48: x<>0.SF implies x"<>0.SF proof assume A1:x<>0.SF; assume x"=0.SF; then x*x"=0.SF by VECTSP_1:36; then 1_ SF=0.SF by A1,Th43; hence contradiction by VECTSP_1:def 21; end; theorem Th49: x<>0.SF implies x""=x proof assume A1: x<>0.SF; A2: x""=x""*1_ SF by Def2 .=x"" * (x" * x) by A1,Th43 .=x""*x"*x by VECTSP_1:def 16; x"<>0.SF by A1,Th48; then x""=1_ SF*x by A2,Th43; hence thesis by Def2; end; theorem Th50: x<>0.SF implies ((1_ SF)/x=x" & (1_ SF)/x"=x) proof A1: for x holds (1_ SF)/x=x" proof let x; (1_ SF)/x= 1_ SF * x" by Def8 .=x" by Def2; hence thesis; end; x<>0.SF implies (1_ SF)/x"=x proof assume A2: x<>0.SF; (1_ SF)/x"=x"" by A1 .=x by A2,Th49; hence thesis; end; hence thesis by A1; end; theorem x<>0.SF implies x*((1_ SF)/x)=1_ SF & ((1_ SF)/x)*x=1_ SF proof A1: x<>0.SF implies x*((1_ SF)/x)=1_ SF proof assume A2:x<>0.SF; hence x*((1_ SF)/x)=x*x" by Th50 .=1_ SF by A2,Th43; end; x<>0.SF implies ((1_ SF)/x)*x=1_ SF proof assume A3:x<>0.SF; hence ((1_ SF)/x)*x=x"*x by Th50 .=1_ SF by A3,Th43; end; hence thesis by A1; end; theorem x<>0.SF implies x/x = 1_ SF proof assume A1: x<>0.SF; thus x/x=x*x" by Def8 .=1_ SF by A1,Th43; end; theorem Th53: 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*y" by Def8 .=x*1_ SF*y" by Def2 .=x*(z*z")*y" by A2,Th43 .=(x*z)*z"*y" by VECTSP_1:def 16 .=(x*z)*(z"*y") by VECTSP_1:def 16 .=(x*z)*(y*z)" by A1,A2,Th46 .=(x*z)/(y*z) by Def8; end; theorem Th54: y<>0.SF implies (-x/y=(-x)/y & x/(-y)=-x/y) proof assume A1:y<>0.SF; A2: for x,y holds -x/y=(-x)/y proof let x,y; thus -x/y=-(x*y") by Def8 .=(-x)*y" by VECTSP_1:41 .=(-x)/y by Def8; end; A3: -1_ SF<>0.SF proof 1_ SF<>0.SF by VECTSP_1:def 21; hence thesis by Th34; end; x/(-y)=-x/y proof x/(-y)=(x*(-1_ SF))/((-y)*(-1_ SF)) proof -y<>0.SF by A1,Th34; hence thesis by A3,Th53; end; then x/(-y)=(-x*1_ SF)/((-y)*(-1_ SF)) by VECTSP_1:40 .= (-x)/((-y)*(-1_ SF)) by Def2 .= (-x)/(-(-y)*1_ SF) by VECTSP_1:40 .= (-x)/((-(-y))*1_ SF) by VECTSP_1:41 .= (-x)/(y*1_ SF) by RLVECT_1:30 .= (-x)/y by Def2 .= -x/y by A2; hence thesis; end; hence thesis by A2; end; theorem z<>0.SF implies ( x/z + y/z = (x+y)/z ) & ( x/z - y/z = (x-y)/z ) proof A1: for x,y,z holds ( x/z + y/z = (x+y)/z ) proof let x,y,z; thus x/z + y/z=x*z" + y/z by Def8 .=x*z" + y*z" by Def8 .=(x+y)*z" by VECTSP_1:def 18 .=(x+y)/z by Def8; end; z<>0.SF implies x/z - y/z = (x-y)/z proof assume A2:z<>0.SF; thus x/z - y/z = x/z+ -y/z by RLVECT_1:def 11 .=x/z+(-y)/z by A2,Th54 .=(x+ -y)/z by A1 .=(x-y)/z by RLVECT_1:def 11; end; hence thesis by A1; 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 A3: z"<>0.SF by Th48; thus x/(y/z)=x/(y*z") by Def8 .=x*(y*z")" by Def8 .=x*(z""*y") by A1,A3,Th46 .=x*(z*y") by A2,Th49 .=(x*z)*y" by VECTSP_1:def 16 .=(x*z)/y by Def8; end; theorem y<>0.SF implies x/y*y=x proof assume A1:y<>0.SF; thus x/y*y=x*y"*y by Def8 .=x*(y"*y) by VECTSP_1:def 16 .=x*1_ SF by A1,Th43 .=x by Def2; end; :: 13. LEFT-, RIGHT-, AND BI-MODULE STRUCTURE definition let FS be 1-sorted; struct(LoopStr) RightModStr over FS (# carrier -> set, add -> BinOp of the carrier, Zero -> Element of the carrier, rmult -> Function of [: the carrier, the carrier of FS:], the carrier #); end; definition let FS be 1-sorted; cluster non empty RightModStr over FS; existence proof consider A being non empty set, a being BinOp of A, Z being Element of A, r being 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; definition 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 by STRUCT_0:def 1; 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 (VectSpStr over FS1, RightModStr over FS2) BiModStr over FS1,FS2 (# carrier -> set, add -> BinOp of the carrier, Zero -> 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; definition let FS1,FS2 be 1-sorted; cluster non empty BiModStr over FS1,FS2; existence proof consider A being non empty set, a being BinOp of A, Z being Element of A, l being Function of [:the carrier of FS1,A:],A, r being 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; definition 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 by STRUCT_0:def 1; 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 LoopStr); func AbGr R -> strict AbGroup equals :Def9: LoopStr (#the carrier of R, the add of R, the Zero of R#); coherence proof reconsider IT = LoopStr(# the carrier of R,the add of R,the Zero of R #) as non empty LoopStr by STRUCT_0:def 1; 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 x'=x,y'=y,z'=z as Scalar of R; A1: (the Zero of IT) = 0.R by RLVECT_1:def 2; thus x+y = (the add of IT).(x,y) by RLVECT_1:5 .= y'+x' by RLVECT_1:5 .= (the add of R).(y',x') by RLVECT_1:5 .= y+x by RLVECT_1:5; thus (x+y)+z = (the add of IT).(x+y,z) by RLVECT_1:5 .= (the add of IT).((the add of IT).(x,y),z) by RLVECT_1:5 .= (the add of R).((x'+y'),z') by RLVECT_1:5 .= (x'+y')+z' by RLVECT_1:5 .= x'+(y'+z') by RLVECT_1:def 6 .= (the add of R).(x',(y'+z')) by RLVECT_1:5 .= (the add of R).(x',(the add of R).(y',z')) by RLVECT_1:5 .= (the add of IT).(x,y+z) by RLVECT_1:5 .= x+(y+z) by RLVECT_1:5; thus x+0.IT = (the add of IT).(x,0.IT) by RLVECT_1:5 .= (the add of IT).(x,(the Zero of IT)) by RLVECT_1:def 2 .= x'+(0.R) by A1,RLVECT_1:5 .= x by RLVECT_1:10; consider b being Scalar of R such that A2: x' + b = 0.R by RLVECT_1:def 8; reconsider b' = b as Element of IT; take b'; thus x + b' = (the add of IT).(x,b') by RLVECT_1:5 .= x'+ b by RLVECT_1:5 .= 0.IT by A1,A2,RLVECT_1:def 2; end; hence thesis by VECTSP_1:7; end; end; deffunc LEFTMODULE(Ring) = VectSpStr(# the carrier of $1,the add of $1, the Zero of $1, the mult of $1 #); Lm3: LEFTMODULE(R) is Abelian add-associative right_zeroed right_complementable proof A1:now let x,y,z be Scalar of R; let x',y',z' be Element of LEFTMODULE(R); assume A2: x = x' & y = y' & z = z'; thus x + y = (the add of R).(x,y) by RLVECT_1:5 .= x'+ y' by A2,RLVECT_1:5; end; thus LEFTMODULE(R) is Abelian proof let x,y be Element of LEFTMODULE(R); reconsider x'= x, y'= y as Scalar of R; thus x+y = y'+ x' by A1 .= y + x by A1; end; thus LEFTMODULE(R) is add-associative proof let x,y,z be Element of LEFTMODULE(R); reconsider x'= x, y'= y, z'= z as Scalar of R; A3: x + y = x'+ y' by A1; A4: y + z = y'+ z' by A1; thus (x+y)+z = (x'+ y') + z' by A1,A3 .= x'+ (y'+ z') by RLVECT_1:def 6 .= x + (y + z) by A1,A4; end; A5: 0.(LEFTMODULE(R)) = the Zero of R by RLVECT_1:def 2 .= 0.R by RLVECT_1:def 2; thus LEFTMODULE(R) is right_zeroed proof let x be Element of LEFTMODULE(R); reconsider x'= x as Scalar of R; thus x+(0.(LEFTMODULE(R))) = x'+ (0.R) by A1,A5 .= x by RLVECT_1:10; end; let x be Element of LEFTMODULE(R); reconsider x'= x as Scalar of R; consider b' being Scalar of R such that A6: x' + b' = 0.R by RLVECT_1:def 8; reconsider b = b' as Element of LEFTMODULE(R); take b; thus x+b = 0.(LEFTMODULE(R)) by A1,A5,A6; end; definition let R; cluster Abelian add-associative right_zeroed right_complementable strict (non empty VectSpStr over R); existence proof LEFTMODULE(R) is Abelian add-associative right_zeroed right_complementable by Lm3; hence thesis; end; end; definition let R; canceled; func LeftModule R -> Abelian add-associative right_zeroed right_complementable strict (non empty VectSpStr over R) equals :Def11: VectSpStr (# the carrier of R, the add of R, the Zero of R, the mult of R #); coherence by Lm3; end; deffunc RIGHTMODULE(Ring) = RightModStr(# the carrier of $1,the add of $1, the Zero of $1, the mult of $1 #); Lm4: RIGHTMODULE(R) is Abelian add-associative right_zeroed right_complementable proof A1:now let x,y,z be Scalar of R; let x',y',z' be Element of RIGHTMODULE(R); assume A2: x = x' & y = y' & z = z'; thus x + y = (the add of R).(x,y) by RLVECT_1:5 .= x'+ y' by A2,RLVECT_1:5; end; thus RIGHTMODULE(R) is Abelian proof let x,y be Element of RIGHTMODULE(R); reconsider x'= x, y'= y as Scalar of R; thus x+y = y'+ x' by A1 .= y + x by A1; end; thus RIGHTMODULE(R) is add-associative proof let x,y,z be Element of RIGHTMODULE(R); reconsider x'= x, y'= y, z'= z as Scalar of R; A3: x + y = x'+ y' by A1; A4: y + z = y'+ z' by A1; thus (x+y)+z = (x'+ y') + z' by A1,A3 .= x'+ (y'+ z') by RLVECT_1:def 6 .= x + (y + z) by A1,A4; end; A5: 0.(RIGHTMODULE(R)) = the Zero of R by RLVECT_1:def 2 .= 0.R by RLVECT_1: def 2; thus RIGHTMODULE(R) is right_zeroed proof let x be Element of RIGHTMODULE(R); reconsider x'= x as Scalar of R; thus x+(0.(RIGHTMODULE(R))) = x'+ (0.R) by A1,A5 .= x by RLVECT_1:10; end; let x be Element of RIGHTMODULE(R); reconsider x'= x as Scalar of R; consider b' being Scalar of R such that A6: x' + b' = 0.R by RLVECT_1:def 8; reconsider b = b' as Element of RIGHTMODULE(R); take b; thus x+b = 0.(RIGHTMODULE(R)) by A1,A5,A6; end; definition let R; cluster Abelian add-associative right_zeroed right_complementable strict (non empty RightModStr over R); existence proof RIGHTMODULE(R) is Abelian add-associative right_zeroed right_complementable by Lm4; hence thesis; end; end; definition let R; canceled 2; func RightModule R -> Abelian add-associative right_zeroed right_complementable strict (non empty RightModStr over R) equals :Def14: RightModStr (# the carrier of R, the add of R, the Zero of R, the mult of R #); coherence by Lm4; 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 :Def15: (the rmult of V).(v,x); coherence; end; definition canceled; func op1 -> UnOp of {{}} means not contradiction; existence; uniqueness by FUNCT_2:66; func op0 -> Element of {{}} means not contradiction; existence; uniqueness proof let x,y be Element of {{}}; x = {} & y = {} by TARSKI:def 1; hence thesis; end; end; deffunc BIMODULE(Ring,Ring) = BiModStr(# {{}},op2,op0, pr2 (the carrier of $1, {{}}), pr1 ({{}},the carrier of $2) #); Lm5: BIMODULE(R1,R2) is Abelian add-associative right_zeroed right_complementable proof set G = BiModStr(# {{}},op2,op0,pr2 (the carrier of R1, {{}}), pr1 ({{}},the carrier of R2) #); now let x,y,z be Element of G; x+y = {} & y+x = {} & (x+y)+z = {} & x+(y+z) = {} & x+(0.G) = {} & x = {} & x+(-x) = {} & (0.G) = {} by TARSKI:def 1; hence x+y = y+x & (x+y)+z = x+(y+z) & x+(0.G) = x & ex x' being Element of G st x+x' = 0.G; end; hence thesis by RLVECT_1:def 5,def 6,def 7,def 8; end; definition let R1,R2; cluster Abelian add-associative right_zeroed right_complementable strict (non empty BiModStr over R1,R2); existence proof BIMODULE(R1,R2) is Abelian add-associative right_zeroed right_complementable by Lm5; hence thesis; end; end; definition let R1,R2; canceled 2; func BiModule(R1,R2) -> Abelian add-associative right_zeroed right_complementable strict (non empty BiModStr over R1,R2) equals :Def21: BiModStr (# {{}},op2,op0,pr2 (the carrier of R1, {{}}), pr1 ({{}},the carrier of R2) #); coherence by Lm5; end; canceled 13; theorem Th71: 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 mult of R; set LS = VectSpStr (# the carrier of R,the add of R, the Zero of R ,MLT #); A1: LS = LeftModule R by Def11; 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 v' = v , w' = w as Scalar of R; A2: (the lmult of LS).(x,w) = x*w by VECTSP_1:def 24; A3: (the lmult of LS).(y,v) = y*v by VECTSP_1:def 24; thus x*(v+w) = (the lmult of LS).(x,(v+w)) by VECTSP_1:def 24 .= MLT.(x,(the add of R).(v',w')) by RLVECT_1:5 .= MLT.(x,v'+w') by RLVECT_1:5 .= x*(v'+w') by VECTSP_1:def 10 .= x*v'+x*w' by VECTSP_1:def 18 .= (the add of R).(x*v',x*w') by RLVECT_1:5 .= (the add of R).(MLT.(x,v'),x*w') by VECTSP_1:def 10 .= (the add of R). ((the lmult of LS).(x,v),(the lmult of LS).(x,w)) by VECTSP_1:def 10 .= (the add of R).(x*v,x*w) by A2,VECTSP_1:def 24 .= x*v+x*w by RLVECT_1:5; thus (x+y)*v = (the lmult of LS).((x+y),v) by VECTSP_1:def 24 .= (x+y)*v' by VECTSP_1:def 10 .= x*v'+y*v' by VECTSP_1:def 18 .= (the add of R).(x*v',y*v') by RLVECT_1:5 .= (the add of R).(MLT.(x,v'),y*v') by VECTSP_1:def 10 .= (the add of R). ((the lmult of LS).(x,v),(the lmult of LS).(y,v)) by VECTSP_1:def 10 .= (the add of R).(x*v,y*v) by A3,VECTSP_1:def 24 .= x*v+y*v by RLVECT_1:5; thus (x*y)*v = (the lmult of LS).((x*y),v) by VECTSP_1:def 24 .= (x*y)*v' by VECTSP_1:def 10 .= x*(y*v') by VECTSP_1:def 16 .= MLT.(x,y*v') by VECTSP_1:def 10 .= (the lmult of LS).(x,(the lmult of LS).(y,v)) by VECTSP_1:def 10 .= (the lmult of LS).(x,(y*v)) by VECTSP_1:def 24 .= x*(y*v) by VECTSP_1:def 24; thus (1_ R)*v = MLT.(1_ R,v') by VECTSP_1:def 24 .= (1_ R)*v' by VECTSP_1:def 10 .= v by Def2; end; hence thesis by A1; end; definition let R; cluster VectSp-like Abelian add-associative right_zeroed right_complementable strict (non empty VectSpStr over R); existence proof take LeftModule R; thus 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 by Th71; thus thesis; end; end; definition let R; mode LeftMod of R is Abelian add-associative right_zeroed right_complementable VectSp-like (non empty VectSpStr over R); end; Lm6: LeftModule R is VectSp-like proof let x,y be Scalar of R; let v,w be Vector of LeftModule R; thus thesis by Th71; end; definition let R; cluster LeftModule R -> Abelian add-associative right_zeroed right_complementable strict VectSp-like; coherence by Lm6; end; :: 18. AXIOMS OF LEFT MODULE OF RING canceled 5; theorem Th77: 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 GF = LoopStr (# the carrier of R,the add of R,the Zero of R #); GF = AbGr R by Def9; then reconsider GF as AbGroup; set MLT = the mult of R; set LS = RightModStr (# the carrier of R,the add of R,the Zero of R,MLT #); A1: LS = RightModule R by Def14; 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 v' = v , w' = w as Scalar of R; A2: (the rmult of LS).(w,x) = w*x by Def15; A3: (the rmult of LS).(v,y) = v*y by Def15; thus (v+w)*x = (the rmult of LS).((v+w),x) by Def15 .= MLT.((the add of R).(v',w'),x) by RLVECT_1:5 .= MLT.(v'+w',x) by RLVECT_1:5 .= (v'+w')*x by VECTSP_1:def 10 .= v'*x+w'*x by VECTSP_1:def 18 .= (the add of R).(v'*x,w'*x) by RLVECT_1:5 .= (the add of R).(MLT.(v',x),w'*x) by VECTSP_1:def 10 .= (the add of GF). ((the rmult of LS).(v,x),(the rmult of LS).(w,x)) by VECTSP_1:def 10 .= (the add of GF).(v*x,w*x) by A2,Def15 .= v*x+w*x by RLVECT_1:5; thus v*(x+y) = (the rmult of LS).(v,(x+y)) by Def15 .= v'*(x+y) by VECTSP_1:def 10 .= v'*x+v'*y by VECTSP_1:def 18 .= (the add of R).(v'*x,v'*y) by RLVECT_1:5 .= (the add of R).(MLT.(v',x),v'*y) by VECTSP_1:def 10 .= (the add of GF). ((the rmult of LS).(v,x),(the rmult of LS).(v,y)) by VECTSP_1:def 10 .= (the add of GF).(v*x,v*y) by A3,Def15 .= v*x+v*y by RLVECT_1:5; thus v*(y*x) = (the rmult of LS).(v,(y*x)) by Def15 .= v'*(y*x) by VECTSP_1:def 10 .= (v'*y)*x by VECTSP_1:def 16 .= MLT.(v'*y,x) by VECTSP_1:def 10 .= (the rmult of LS).((the rmult of LS).(v,y),x) by VECTSP_1:def 10 .= (the rmult of LS).((v*y),x) by Def15 .= (v*y)*x by Def15; thus v*(1_ R) = MLT.(v',1_ R) by Def15 .= v'*(1_ R) by VECTSP_1:def 10 .= v by Def2; end; hence thesis by A1; end; definition let R be non empty doubleLoopStr; let IT be non empty RightModStr over R; canceled; attr IT is RightMod-like means :Def23: 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; definition let R; cluster Abelian add-associative right_zeroed right_complementable RightMod-like strict (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 Th77; 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; Lm7: RightModule R is RightMod-like proof let x,y be Scalar of R; let v,w be Vector of RightModule R; thus thesis by Th77; end; definition let R; cluster RightModule R -> Abelian add-associative right_zeroed right_complementable RightMod-like; coherence by Lm7; end; :: 20. AXIOMS OF RIGHT MODULE OF RING Lm8: 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 G = BiModule(R1,R2); set a = {}; A1: G = BiModStr (# {{}},op2,op0,pr2(the carrier of R1, {{}}), pr1({{}},the carrier of R2) #) by Def21; let x,y be Scalar of R1, p,q be Scalar of R2, v,w be Vector of G; x*(v+w) = a & x*v+x*w = a & (x+y)*v = a & x*v+y*v = a & (x*y)*v = a & x*(y*v) = a & (1_ R1)*v = a & v = a by A1,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; (v+w)*p = a & v*p+w*p = a & v*(p+q) = a & v*p+v*q = a & v*(q*p) = a & (v*q)*p = a & v*(1_ R2) = a & v = a & x*(v*p) = a & (x*v)*p = a by A1,TARSKI:def 1; hence thesis; end; definition let R1,R2; let IT be non empty BiModStr over R1,R2; attr IT is BiMod-like means :Def24: 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; definition let R1,R2; cluster Abelian add-associative right_zeroed right_complementable RightMod-like VectSp-like BiMod-like strict (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 Lm8; hence thesis by Def23,Def24,VECTSP_1:def 26; end; end; definition let R1,R2; mode BiMod of R1,R2 is Abelian add-associative right_zeroed right_complementable RightMod-like VectSp-like BiMod-like (non empty BiModStr over R1,R2); end; canceled 5; 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 VectSp-like BiMod-like by Def23,Def24,VECTSP_1:def 26; theorem Th84: 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 Lm8; hence thesis by Def23,Def24,VECTSP_1:def 26; end; definition let R1,R2; cluster BiModule(R1,R2) -> Abelian add-associative right_zeroed right_complementable RightMod-like VectSp-like BiMod-like; coherence by Th84; end;