:: Abelian Groups, Fields and Vector Spaces :: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski :: :: Received November 23, 1989 :: Copyright (c) 1990-2021 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, STRUCT_0, NUMBERS, BINOP_2, CARD_1, SUBSET_1, ARYTM_3, RLVECT_1, SUPINF_2, ARYTM_1, RELAT_1, MESFUNC1, GROUP_1, LATTICES, BINOP_1, FUNCT_1, ZFMISC_1, XXREAL_0, VECTSP_1, MEMBERED, MSSUBFAM, FUNCT_7, REAL_1, XCMPLX_0, VECTSP_2, FUNCSDOM; notations XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1, FUNCT_2, BINOP_1, FUNCT_7, XCMPLX_0, XXREAL_0, XREAL_0, NAT_D, BINOP_2, MEMBERED, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1; constructors BINOP_1, XXREAL_0, NAT_1, BINARITH, RLVECT_1, GROUP_1, BINOP_2, NAT_D, RELSET_1, MEMBERED, FUNCT_7; registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, STRUCT_0, GROUP_1, ALGSTR_0, MEMBERED; requirements NUMERALS, SUBSET, ARITHM; begin :: 1. GROUP STRUCTURE definition func G_Real -> strict addLoopStr equals :: VECTSP_1:def 1 addLoopStr (# REAL,addreal,In(0,REAL) #); end; registration cluster G_Real -> non empty; end; registration cluster the carrier of G_Real -> real-membered; end; registration let a,b be Element of G_Real, x,y be Real; identify a+b with x+y when a = x, b = y; end; registration cluster G_Real -> Abelian add-associative right_zeroed right_complementable; end; registration let a be Element of G_Real, x be Real; identify -a with -x when a = x; end; registration let a,b be Element of G_Real, x,y be Real; identify a-b with x-y when a = x, b = y; end; registration cluster strict add-associative right_zeroed right_complementable Abelian for non empty addLoopStr; end; definition mode AddGroup is add-associative right_zeroed right_complementable non empty addLoopStr; end; definition mode AbGroup is Abelian AddGroup; end; :: 4. FIELD STRUCTURE definition let IT be non empty doubleLoopStr; attr IT is right-distributive means :: VECTSP_1:def 2 for a, b, c being Element of IT holds a*(b+c) = a*b + a*c; attr IT is left-distributive means :: VECTSP_1:def 3 for a, b, c being Element of IT holds (b+c)*a = b*a + c*a; end; definition let IT be non empty multLoopStr; attr IT is right_unital means :: VECTSP_1:def 4 for x being Element of IT holds x * 1. IT = x; end; definition func F_Real -> strict doubleLoopStr equals :: VECTSP_1:def 5 doubleLoopStr (# REAL,addreal,multreal,In(1,REAL),In(0,REAL)#); end; registration cluster F_Real -> non empty; end; registration cluster the carrier of F_Real -> real-membered; end; registration let a,b be Element of F_Real, x,y be Real; identify a+b with x+y when a = x, b = y; end; registration let a,b be Element of F_Real, x,y be Real; identify a*b with x*y when a = x, b = y; end; definition let IT be non empty multLoopStr; attr IT is well-unital means :: VECTSP_1:def 6 for x being Element of IT holds x * 1. IT = x & 1.IT * x = x; end; registration cluster F_Real -> well-unital; end; registration cluster well-unital for non empty multLoopStr_0; end; registration let L be well-unital non empty multLoopStr_0; let x be Element of L; reduce x * 1.L to x; reduce 1.L * x to x; end; definition let IT be non empty doubleLoopStr; attr IT is distributive means :: VECTSP_1:def 7 for x,y,z being Element of IT holds x* (y+z) = x*y+x*z & (y+z)*x = y*x+z*x; end; definition let IT be non empty multLoopStr; attr IT is left_unital means :: VECTSP_1:def 8 for x being Element of IT holds 1.IT * x = x; end; definition let IT be non empty multLoopStr_0; redefine attr IT is almost_left_invertible means :: VECTSP_1:def 9 for x being Element of IT st x <> 0.IT ex y be Element of IT st y*x = 1.IT; end; registration cluster F_Real -> unital; end; registration cluster F_Real -> add-associative right_zeroed right_complementable Abelian commutative associative left_unital right_unital distributive almost_left_invertible non degenerated; end; registration let a be Element of F_Real, x be Real; identify -a with -x when a = x; end; registration let a,b be Element of F_Real, x,y be Real; identify a-b with x-y when a = x, b = y; end; registration cluster distributive -> left-distributive right-distributive for non empty doubleLoopStr; cluster left-distributive right-distributive -> distributive for non empty doubleLoopStr; end; registration cluster well-unital -> left_unital right_unital for non empty multLoopStr; cluster left_unital right_unital -> unital for non empty multLoopStr; end; registration cluster commutative associative for non empty multMagma; end; registration cluster commutative associative unital for non empty multLoopStr; end; registration cluster add-associative right_zeroed right_complementable Abelian commutative associative left_unital right_unital distributive almost_left_invertible non degenerated well-unital strict for non empty doubleLoopStr; end; definition mode Ring is Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr; end; definition mode Skew-Field is non degenerated almost_left_invertible Ring; end; definition mode Field is commutative Skew-Field; end; :: 6. AXIOMS OF FIELD registration cluster well-unital -> unital for non empty multLoopStr; end; ::$CT 4 theorem :: VECTSP_1:5 for F being associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x,y,z being Element of F holds (x <> 0.F & x*y = x*z) implies y = z; notation let F be associative commutative well-unital almost_left_invertible non empty doubleLoopStr, x be Element of F; synonym x" for /x; end; definition let F be associative commutative well-unital almost_left_invertible non empty doubleLoopStr, x be Element of F; assume x <> 0.F; redefine func x" means :: VECTSP_1:def 10 it*x = 1.F; end; registration let a be non zero Element of F_Real, x be Real; identify a" with x" when a = x; end; registration let a,b be non zero Element of F_Real, x,y be Real; identify a/b with x/y when a = x, b = y; end; :: definition :: let F be associative commutative well-unital distributive :: almost_left_invertible non empty doubleLoopStr, x,y be Element of F; :: func x/y ->Element of F equals :: x*y"; :: coherence; :: end; ::$CD theorem :: VECTSP_1:6 for F being add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, x being Element of F holds x*(0.F) = 0.F; registration let F be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr; let x be Element of F; let y be zero Element of F; reduce x * y to y; end; theorem :: VECTSP_1:7 for F being add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, x being Element of F holds (0.F)*x = 0.F; registration let F be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr; let x be zero Element of F; let y be Element of F; reduce x * y to x; end; theorem :: VECTSP_1:8 for F be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, x,y being Element of F holds x*(-y) = -x*y; theorem :: VECTSP_1:9 for F be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, x,y being Element of F holds (-x)*y = -x*y; theorem :: VECTSP_1:10 for F be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, x,y being Element of F holds (-x)*(-y)= x*y; theorem :: VECTSP_1:11 for F be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, x,y,z being Element of F holds x*(y-z) = x*y - x*z; theorem :: VECTSP_1:12 for F being add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non empty doubleLoopStr, x,y being Element of F holds x*y=0.F iff x=0.F or y=0.F; theorem :: VECTSP_1:13 for K being add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr for a,b,c be Element of K holds (a- b)*c =a*c -b*c; :: 8. VECTOR SPACE STRUCTURE definition let F be 1-sorted; struct(addLoopStr) ModuleStr over F (# carrier -> set, addF -> BinOp of the carrier, ZeroF -> Element of the carrier, lmult -> Function of [:the carrier of F,the carrier:], the carrier #); end; registration let F be 1-sorted; cluster non empty strict for ModuleStr over F; end; registration let F 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 F,A:], A; cluster ModuleStr(#A,a,Z,l#) -> non empty; end; definition let F be 1-sorted; mode Scalar of F is Element of F; end; definition let F be 1-sorted; let VS be ModuleStr over F; mode Scalar of VS is Scalar of F; mode Vector of VS is Element of VS; end; definition let F be non empty 1-sorted, V be non empty ModuleStr over F; let x be Element of F; let v be Element of V; func x*v -> Element of V equals :: VECTSP_1:def 12 (the lmult of V).(x,v); end; definition let F be non empty addLoopStr; func comp F -> UnOp of the carrier of F means :: VECTSP_1:def 13 for x being Element of F holds it.x = -x; end; definition let F be non empty doubleLoopStr; let IT be non empty ModuleStr over F; attr IT is vector-distributive means :: VECTSP_1:def 14 for x being Element of F for v,w being Element of IT holds x*(v+w) = x*v+x*w; attr IT is scalar-distributive means :: VECTSP_1:def 15 for x,y being Element of F for v being Element of IT holds (x+y)*v = x*v+y*v; attr IT is scalar-associative means :: VECTSP_1:def 16 for x,y being Element of F for v being Element of IT holds (x*y)*v = x*(y*v); attr IT is scalar-unital means :: VECTSP_1:def 17 for v being Element of IT holds (1.F)*v = v; end; registration let F be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr; cluster scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable Abelian strict for non empty ModuleStr over F; end; definition let F be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr; mode VectSp of F is scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable Abelian non empty ModuleStr over F; end; reserve F for Field, x for Element of F, V for VectSp of F, v for Element of V; theorem :: VECTSP_1:14 for F being add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, x being Element of F for V being add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty ModuleStr over F, v being Element of V holds (0.F)*v = 0.V & (-1.F)*v = -v & x*(0.V) = 0.V; theorem :: VECTSP_1:15 x*v = 0.V iff x = 0.F or v = 0.V; :: 13. APPENDIX theorem :: VECTSP_1:16 for V being add-associative right_zeroed right_complementable non empty addLoopStr, v,w being Element of V holds v+w=0.V iff -v=w; theorem :: VECTSP_1:17 for V being add-associative right_zeroed right_complementable non empty addLoopStr, u,v,w being Element of V holds -(v+w)=-w-v & -(w+-v)=v-w & - (v-w)=w+-v & -(-v-w)=w+v & u-(w+v)=u-v-w; theorem :: VECTSP_1:18 for V being add-associative right_zeroed right_complementable non empty addLoopStr, v being Element of V holds 0.V-v=-v & v-0.V=v; theorem :: VECTSP_1:19 for F being add-associative right_zeroed right_complementable non empty addLoopStr, x,y being Element of F holds (x+(-y)=0.F iff x=y) & (x-y =0.F iff x=y); theorem :: VECTSP_1:20 x<>0.F implies x"*(x*v)=v; theorem :: VECTSP_1:21 for F be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable non empty ModuleStr over F, x being Element of F, v,w being Element of V holds -x*v=(-x) *v & w-x*v=w+(-x)*v; registration cluster commutative left_unital -> right_unital for non empty multLoopStr; end; theorem :: VECTSP_1:22 for F be add-associative right_zeroed right_complementable Abelian associative well-unital right_unital distributive non empty doubleLoopStr, V be scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable non empty ModuleStr over F, x being Element of F, v being Element of V holds x*(-v)=-x*v; theorem :: VECTSP_1:23 for F be add-associative right_zeroed right_complementable Abelian associative well-unital right_unital distributive non empty doubleLoopStr, V be scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable non empty ModuleStr over F, x being Element of F, v,w being Element of V holds x*(v-w)=x *v-x*w; theorem :: VECTSP_1:24 for F being add-associative right_zeroed right_complementable commutative associative well-unital non degenerated almost_left_invertible distributive non empty doubleLoopStr, x being Element of F holds x <> 0.F implies (x")" = x; registration let F be add-associative right_zeroed right_complementable commutative associative well-unital almost_left_invertible distributive non degenerated doubleLoopStr; let x be non zero Element of F; reduce (x")" to x; end; theorem :: VECTSP_1:25 for F being Field, x being Element of F holds x <> 0.F implies x" <> 0.F & -x" <> 0.F; theorem :: VECTSP_1:26 1.F_Real + 1.F_Real <> 0.F_Real; definition let IT be non empty addLoopStr; attr IT is Fanoian means :: VECTSP_1:def 18 for a being Element of IT st a + a = 0.IT holds a = 0.IT; end; registration cluster Fanoian for non empty addLoopStr; end; definition let F be add-associative right_zeroed right_complementable commutative associative well-unital almost_left_invertible non degenerated distributive non empty doubleLoopStr; redefine attr F is Fanoian means :: VECTSP_1:def 19 1.F+1.F<>0.F; end; registration cluster strict Fanoian for Field; end; theorem :: VECTSP_1:27 for F being add-associative right_zeroed right_complementable non empty addLoopStr, a,b being Element of F holds a - b = 0.F implies a = b; theorem :: VECTSP_1:28 for F being add-associative right_zeroed right_complementable non empty addLoopStr, a being Element of F holds -a = 0.F implies a = 0.F; theorem :: VECTSP_1:29 for F being add-associative right_zeroed right_complementable non empty addLoopStr, a, b being Element of F holds a - b = 0.F implies b - a = 0. F; theorem :: VECTSP_1:30 for a, b, c being Element of F holds (a <> 0.F & a*c - b = 0.F implies c = b*a") & (a <> 0.F & b - c*a = 0.F implies c = b*a"); theorem :: VECTSP_1:31 for F being add-associative right_zeroed right_complementable non empty addLoopStr, a, b being Element of F holds a + b = -(-b + -a); theorem :: VECTSP_1:32 for F being add-associative right_zeroed right_complementable non empty addLoopStr, a, b, c being Element of F holds (b+a)-(c+a) = b-c; theorem :: VECTSP_1:33 for G being add-associative right_zeroed right_complementable non empty addLoopStr, v,w being Element of G holds -(-v+w) = -w+v; theorem :: VECTSP_1:34 for G being Abelian add-associative non empty addLoopStr, u,v,w being Element of G holds u - v - w = u - w - v; theorem :: VECTSP_1:35 for B being AbGroup holds multMagma (# the carrier of B, the addF of B #) is commutative Group; begin :: Addenda :: from COMPTRIG, 2006.08.12, A.T. theorem :: VECTSP_1:36 for L be add-associative right_zeroed right_complementable right-distributive unital non empty doubleLoopStr for n be Element of NAT st n > 0 holds (power L).(0.L,n) = 0.L; :: 2007.02.14, A.T. registration cluster well-unital for non empty multLoopStr; end; registration let S be well-unital non empty multLoopStr; identify 1_S with 1.S; end; theorem :: VECTSP_1:37 for L being non empty multLoopStr st L is well-unital holds 1.L = 1_L; definition let G,H be non empty addMagma; let f be Function of G,H; attr f is additive means :: VECTSP_1:def 20 for x,y being Element of G holds f.(x+y) = f.x+f.y; end; registration let L be right_unital non empty multLoopStr; let x be Element of L; reduce x * 1.L to x; end; registration let L be left_unital non empty multLoopStr; let x be Element of L; reduce 1.L * x to x; end;