:: Abelian Groups, Fields and Vector Spaces
:: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski
::
:: Received November 23, 1989
:: 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, 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;
definitions RLVECT_1, STRUCT_0, GROUP_1, ALGSTR_0;
equalities XCMPLX_0, STRUCT_0, ALGSTR_0;
expansions GROUP_1, ALGSTR_0;
theorems FUNCT_2, RLVECT_1, XCMPLX_0, BINOP_2, GROUP_1, NAT_1, XREAL_1,
XREAL_0, ALGSTR_0, STRUCT_0;
schemes FUNCT_2;
begin :: 1. GROUP STRUCTURE
definition
func G_Real -> strict addLoopStr equals
addLoopStr (# REAL,addreal,In(0,REAL) #);
coherence;
end;
registration
cluster G_Real -> non empty;
coherence;
end;
registration
cluster the carrier of G_Real -> real-membered;
coherence;
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;
compatibility by BINOP_2:def 9;
end;
registration
cluster G_Real -> Abelian add-associative right_zeroed right_complementable;
coherence
proof
thus for x,y being Element of G_Real holds x+y = y+x;
thus for x,y,z being Element of G_Real holds (x+y)+z = x+(y+z);
thus for x being Element of G_Real holds x+0.G_Real = x;
let x be Element of G_Real;
reconsider x9=x as Element of REAL;
reconsider y = -x9 as Element of G_Real by XREAL_0:def 1;
take y;
thus thesis;
end;
end;
registration
let a be Element of G_Real, x be Real;
identify -a with -x when a = x;
compatibility
proof
reconsider b = -x as Element of G_Real by XREAL_0:def 1;
assume x = a;
then b + a = 0.G_Real;
hence thesis by RLVECT_1:6;
end;
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;
compatibility;
end;
registration
cluster strict add-associative right_zeroed right_complementable Abelian for
non empty addLoopStr;
existence
proof
take G_Real;
thus thesis;
end;
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
:Def2:
for a, b, c being Element of IT holds a*(b+c) = a*b + a*c;
attr IT is left-distributive means
:Def3:
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
:Def4:
for x being Element of IT holds x * 1. IT = x;
end;
definition
func F_Real -> strict doubleLoopStr equals
doubleLoopStr (# REAL,addreal,multreal,In(1,REAL),In(0,REAL)#);
correctness;
end;
registration
cluster F_Real -> non empty;
coherence;
end;
registration
cluster the carrier of F_Real -> real-membered;
coherence;
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;
compatibility by BINOP_2:def 9;
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;
compatibility by BINOP_2:def 11;
end;
definition
let IT be non empty multLoopStr;
attr IT is well-unital means
:Def6:
for x being Element of IT holds x * 1. IT = x & 1.IT * x = x;
end;
Lm1: for L being non empty multLoopStr st L is well-unital holds 1.L = 1_L
proof
let L be non empty multLoopStr;
assume L is well-unital;
then
( for h being Element of L holds h * 1.L = h & 1.L * h = h)& L is unital;
hence thesis by GROUP_1:def 4;
end;
registration
cluster F_Real -> well-unital;
coherence;
end;
registration
cluster well-unital for non empty multLoopStr_0;
existence
proof
take F_Real;
thus thesis;
end;
end;
registration
let L be well-unital non empty multLoopStr_0;
let x be Element of L;
reduce x * 1.L to x;
reducibility by Def6;
reduce 1.L * x to x;
reducibility by Def6;
end;
definition
let IT be non empty doubleLoopStr;
attr IT is distributive means
:Def7:
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
:Def8:
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 :: redefines almost_left_invertible (ALGSTR_0, definition)
:Def9:
for x being Element of IT st x <> 0.IT ex y be Element of IT st y*x = 1.IT;
compatibility
proof
thus IT is almost_left_invertible implies for x being Element of IT st x
<> 0.IT ex y be Element of IT st y*x = 1.IT
by ALGSTR_0:def 27;
assume
A1: for x being Element of IT st x <> 0.IT ex y be Element of IT st y*
x = 1.IT;
let x be Element of IT;
assume x <> 0.IT;
hence ex y be Element of IT st y*x = 1.IT by A1;
end;
end;
set FR = F_Real;
reconsider jj=1 as Real;
registration
cluster F_Real -> unital;
coherence
proof
reconsider e = jj as Element of FR;
take e;
thus thesis;
end;
end;
registration
cluster F_Real -> add-associative right_zeroed right_complementable Abelian
commutative associative left_unital right_unital distributive
almost_left_invertible non degenerated;
coherence
proof
thus for x,y,z being Element of F_Real holds (x+y)+z = x+(y+z);
thus for x being Element of F_Real holds x+0.F_Real = x;
thus F_Real is right_complementable
proof
let x be Element of F_Real;
reconsider x9=x as Element of REAL;
reconsider y=-x9 as Element of F_Real by XREAL_0:def 1;
take y;
thus thesis;
end;
thus for x,y being Element of F_Real holds x+y = y+x;
thus for x,y being Element of F_Real holds x*y = y*x;
thus for x,y,z being Element of F_Real holds (x*y)*z = x*(y*z);
thus for x being Element of F_Real holds (1.F_Real)*x = x;
thus for x being Element of F_Real holds x*(1.F_Real) = x;
thus for x,y,z being Element of F_Real holds x*(y+z) = x*y+x*z & (y+z)*x =
y*x+z*x;
hereby
let x be Element of F_Real;
reconsider x9=x as Element of REAL;
assume
A1: x<>0.F_Real;
reconsider y = (x9)" as Element of F_Real by XREAL_0:def 1;
take y;
thus y*x = 1.F_Real by A1,XCMPLX_0:def 7;
end;
thus 0.F_Real <> 1.F_Real;
end;
end;
registration
let a be Element of F_Real, x be Real;
identify -a with -x when a = x;
compatibility
proof
reconsider b = -x as Element of FR by XREAL_0:def 1;
assume x = a;
then b + a = 0.FR;
hence thesis by RLVECT_1:6;
end;
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;
compatibility;
end;
registration
cluster distributive -> left-distributive right-distributive for non empty
doubleLoopStr;
coherence;
cluster left-distributive right-distributive -> distributive for non empty
doubleLoopStr;
coherence;
end;
registration
cluster well-unital -> left_unital right_unital for non empty multLoopStr;
coherence;
cluster left_unital right_unital -> unital for non empty multLoopStr;
coherence;
end;
registration
cluster commutative associative for non empty multMagma;
existence
proof
take F_Real;
thus thesis;
end;
end;
registration
cluster commutative associative unital for non empty multLoopStr;
existence
proof
take F_Real;
thus thesis;
end;
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;
existence
proof
take F_Real;
thus thesis;
end;
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;
coherence;
end;
::$CT 4
theorem
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
proof
let F be associative commutative well-unital distributive
almost_left_invertible non empty doubleLoopStr, x,y,z be Element of F;
assume x<>0.F;
then consider x1 being Element of F such that
A1: x1*x = 1.F by Def9;
A2: x1*x*y = x1*(x*y) & x1*(x*z) = x1*x*z by GROUP_1:def 3;
assume x*y = x*z;
then x*x1*y = z by A1,A2,Def8;
hence thesis by A1;
end;
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
A1: x <> 0.F;
redefine func x" means :: redefines " (VECTSP_1, synonym) → / (ALGSTR_0, definition)
:Def10:
it*x = 1.F;
compatibility
proof
let IT be Element of F;
A2: x is left_invertible by A1,ALGSTR_0:def 39;
then consider x1 being Element of F such that
A3: x1*x = 1.F;
x is right_mult-cancelable
proof
let y,z be Element of F;
assume
A4: y*x = z*x;
thus y = y * 1.F
.= z * x*x1 by A3,A4,GROUP_1:def 3
.= z * 1.F by A3,GROUP_1:def 3
.= z;
end;
hence thesis by A2,ALGSTR_0:def 30;
end;
end;
registration
let a be non zero Element of F_Real, x be Real;
identify a" with x" when a = x;
compatibility
proof
reconsider b = x" as Element of FR by XREAL_0:def 1;
A1: a <> 0.F_Real;
assume x = a;
then b * a = 1.FR by A1,XCMPLX_0:def 7;
hence thesis by A1,Def10;
end;
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;
compatibility;
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 Th2:
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
proof
let F be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let x be Element of F;
x*(0.F)+(0.F) = x*((0.F)+(0.F))+(0.F) by RLVECT_1:4
.= x*((0.F)+(0.F)) by RLVECT_1:4
.= x*(0.F)+x*(0.F) by Def2;
hence thesis by RLVECT_1:8;
end;
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;
reducibility
proof
y = 0.F by STRUCT_0:def 12;
hence thesis by Th2;
end;
end;
theorem Th3:
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
proof
let F be add-associative right_zeroed right_complementable left-distributive
non empty doubleLoopStr;
let x be Element of F;
(0.F)*x+(0.F) = ((0.F)+(0.F))*x+(0.F) by RLVECT_1:4
.= ((0.F)+(0.F))*x by RLVECT_1:4
.= (0.F)*x+(0.F)*x by Def3;
hence thesis by RLVECT_1:8;
end;
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;
reducibility
proof
x = 0.F by STRUCT_0:def 12;
hence thesis by Th3;
end;
end;
theorem Th4:
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
proof
let F be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr, x,y be Element of F;
x*y +x*(-y) = x*(y+(-y)) by Def2
.= x*(0.F) by RLVECT_1:def 10
.= 0.F;
hence thesis by RLVECT_1:def 10;
end;
theorem Th5:
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
proof
let F be add-associative right_zeroed right_complementable left-distributive
non empty doubleLoopStr, x,y be Element of F;
x*y +(-x)*y = (x+(-x))*y by Def3
.= (0.F)*y by RLVECT_1:def 10
.= 0.F;
hence thesis by RLVECT_1:def 10;
end;
theorem Th6:
for F be add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, x,y being Element of F holds
(-x)*(-y)= x*y
proof
let F be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, x,y be Element of F;
thus (-x)*(-y) = -x*(-y) by Th5
.= --x*y by Th4
.= x*y by RLVECT_1:17;
end;
theorem
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
proof
let F be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr, x,y,z be Element of F;
x*(y-z) = x*y+x*(-z) by Def2
.= x*y - x*z by Th4;
hence thesis;
end;
theorem Th8:
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
proof
let F be add-associative right_zeroed right_complementable associative
commutative well-unital almost_left_invertible distributive non empty
doubleLoopStr, x,y be Element of F;
x*y=0.F implies x=0.F or y=0.F
proof
assume
A1: x*y = 0.F;
assume
A2: x<>0.F;
x"*(0.F) = x"*x*y by A1,GROUP_1:def 3
.= (1.F)*y by A2,Def10
.= y;
hence thesis;
end;
hence thesis;
end;
theorem
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
proof
let K be add-associative right_zeroed right_complementable left-distributive
non empty doubleLoopStr;
let y,z,x be Element of K;
thus (y-z)*x = y*x+(-z)*x by Def3
.= y*x -z*x by Th5;
end;
:: 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;
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 F,A:], A;
take ModuleStr(#A,a,Z,l#);
thus the carrier of ModuleStr(#A,a,Z,l#) is non empty;
thus thesis;
end;
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;
coherence;
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
(the lmult of V).(x,v);
coherence;
end;
definition
let F be non empty addLoopStr;
func comp F -> UnOp of the carrier of F means
for x being Element of F holds it.x = -x;
existence
proof
deffunc F(Element of F) = -$1;
thus ex f being UnOp of the carrier of F st for x being Element of F holds
f.x = F(x) from FUNCT_2:sch 4;
end;
uniqueness
proof
let f, g be UnOp of the carrier of F such that
A1: for x being Element of F holds f.x = -x and
A2: for x being Element of F holds g.x = -x;
now
let x be object;
assume x in the carrier of F;
then reconsider y = x as Element of F;
thus f.x = -y by A1
.= g.x by A2;
end;
hence thesis by FUNCT_2:12;
end;
end;
Lm2: now
let F be add-associative right_zeroed right_complementable Abelian
associative left_unital distributive non empty doubleLoopStr;
let MLT be Function of [:the carrier of F,the carrier of F:],the carrier of
F;
set GF = ModuleStr(# the carrier of F,the addF of F,0.F,MLT #);
thus GF is Abelian
proof
let x,y be Element of GF;
reconsider x9=x,y9=y as Element of F;
thus x+y = y9+x9 by RLVECT_1:2
.= y+x;
end;
thus GF is add-associative
proof
let x,y,z be Element of GF;
reconsider x9=x,y9=y,z9=z as Element of F;
thus (x+y)+z = (x9+y9)+z9 .= x9+(y9+z9) by RLVECT_1:def 3
.= x+(y+z);
end;
thus GF is right_zeroed
proof
let x be Element of GF;
reconsider x9=x as Element of F;
thus x+0.GF = x9+(0.F) .= x by RLVECT_1:4;
end;
thus GF is right_complementable
proof
let x be Element of GF;
reconsider x9=x as Element of F;
consider t being Element of F such that
A1: x9 + t = 0.F by ALGSTR_0:def 11;
reconsider t9 = t as Element of GF;
take t9;
thus thesis by A1;
end;
end;
Lm3: now
let F be add-associative right_zeroed right_complementable associative
well-unital distributive non empty doubleLoopStr;
let MLT be Function of [:the carrier of F,the carrier of F:],the carrier of
F such that
A1: MLT = the multF of F;
let x,y be Element of F;
set LS = ModuleStr (# the carrier of F,the addF of F,0.F, MLT #);
let v,w be Element of LS;
reconsider v9 = v, w9 = w as Element of F;
thus x*(v+w) = x*(v9+w9) by A1
.= x*v9+x*w9 by Def7
.= x*v+x*w by A1;
thus (x+y)*v = (x+y)*v9 by A1
.= x*v9+y*v9 by Def7
.= x*v+y*v by A1;
thus (x*y)*v = (x*y)*v9 by A1
.= x*(y*v9) by GROUP_1:def 3
.= x*(y*v) by A1;
thus (1.F)*v = (1.F)*v9 by A1
.= v;
end;
definition
let F be non empty doubleLoopStr;
let IT be non empty ModuleStr over F;
attr IT is vector-distributive means
:Def13:
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
:Def14:
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
:Def15:
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
:Def16:
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;
existence
proof
take V = ModuleStr (# the carrier of F,the addF of F, 0.F,the multF of F#);
thus for x,y being Element of F for v being Element of V holds
(x+y)*v = x*v+y*v by Lm3;
thus for x being Element of F for v,w being Element of V
holds x*(v+w) = x*v+x*w by Lm3;
thus for x,y being Element of F for v being Element of V holds
(x*y)*v = x*(y*v) by Lm3;
thus for v being Element of V holds (1.F)*v = v by Lm3;
thus thesis by Lm2;
end;
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;
registration
let R be Ring;
let V be VectSp of R;
let v be Element of V;
reduce 1.R * v to v;
reducibility by Def16;
end;
reserve F for Field,
x for Element of F,
V for VectSp of F,
v for Element of V;
theorem Th10:
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
proof
let F be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let x be Element of F;
let V be add-associative right_zeroed right_complementable
scalar-distributive
vector-distributive scalar-associative scalar-unital non
empty ModuleStr over F, v be Element of V;
v+(0.F)*v = (1.F)*v + (0.F)*v by Def16
.= ((1.F)+(0.F))*v by Def14
.= (1.F)*v by RLVECT_1:4
.= v by Def16
.= v+0.V by RLVECT_1:4;
hence
A1: (0.F)*v = 0.V by RLVECT_1:8;
(-(1.F))*v+v = (-(1.F))*v + (1.F)*v by Def16
.= ((1.F)+(-(1.F)))*v by Def14
.= 0.V by A1,RLVECT_1:def 10;
then (-(1.F))*v + (v+(-v)) = 0.V + -v by RLVECT_1:def 3;
then 0.V + -v = (-(1.F))*v + 0.V by RLVECT_1:5
.= (-(1.F))*v by RLVECT_1:4;
hence (-1.F)*v = -v by RLVECT_1:4;
x*(0.V) = (x*(0.F))*v by A1,Def15
.= 0.V by A1;
hence thesis;
end;
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 Def15
.= 0.V by Th10;
assume x<>(0.F);
then 0.V = (1.F)*v by A1,Def10;
hence thesis;
end;
hence thesis by Th10;
end;
:: 13. APPENDIX
theorem
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
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr, v,w be Element of V;
v+w=0.V implies -v=w
proof
assume
A1: v+w=0.V;
thus w = 0.V + w by RLVECT_1:4
.= -v + v + w by RLVECT_1:5
.= -v + 0.V by A1,RLVECT_1:def 3
.= -v by RLVECT_1:4;
end;
hence thesis by RLVECT_1:5;
end;
Lm4: for V being add-associative right_zeroed right_complementable non empty
addLoopStr, v,w being Element of V holds -(w+-v)=v-w
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr, v,w be Element of V;
-(w+-v)=-(-v)-w by RLVECT_1:30;
hence thesis by RLVECT_1:17;
end;
Lm5: for V being add-associative right_zeroed right_complementable non empty
addLoopStr, v,w being Element of V holds -(-v-w)=w+v
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr, v,w be Element of V;
-(-v-w)=w+-(-v) by RLVECT_1:33;
hence thesis by RLVECT_1:17;
end;
theorem
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 by Lm4,Lm5,RLVECT_1:27,30,33;
theorem
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 by RLVECT_1:13
,14;
theorem Th15:
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)
proof
let F be add-associative right_zeroed right_complementable non empty
addLoopStr, x,y be Element of F;
x+(-y)=0.F implies x=y
proof
assume x+(-y)=0.F;
then x+((-y)+y)=0.F+y by RLVECT_1:def 3;
then x+0.F=0.F+y by RLVECT_1:5;
then x=0.F+y by RLVECT_1:4;
hence thesis by RLVECT_1:4;
end;
hence thesis by RLVECT_1:5;
end;
theorem
x<>0.F implies x"*(x*v)=v
proof
assume
A1: x<>0.F;
x"*(x*v)=(x"*x)*v by Def15
.=1.F*v by A1,Def10
.=v;
hence thesis;
end;
theorem Th17:
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
proof
let 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 be Element of F, v,w be Element of V;
A1: -x*v=(-1.F)*(x*v) by Th10
.=((-1.F)*x)*v by Def15
.=(-(1.F*x))*v by Th5;
hence -x*v=(-x)*v;
thus thesis by A1;
end;
registration
cluster commutative left_unital -> right_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;
x*(1.F) = (1.F)*x by A1;
hence thesis by A1;
end;
end;
theorem Th18:
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
proof
let 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 be Element of F, v be Element of V;
x*(-v)=x*((-1.F)*v) by Th10
.=(x*(-1.F))*v by Def15
.=(-(x*1.F))*v by Th4
.=(-x)*v;
hence thesis by Th17;
end;
theorem
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
proof
let 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 be Element of F, v,w be Element of V;
x*(v-w)=x*v+x*(-w) by Def13
.=x*v+(-x*w) by Th18;
hence thesis;
end;
theorem Th20:
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
proof
let F be add-associative right_zeroed right_complementable commutative
associative well-unital non degenerated almost_left_invertible distributive
non empty doubleLoopStr, x be Element of F;
assume
A1: x <> 0.F;
x <> 0.F implies x" <> 0.F
proof
assume
A2: x <> 0.F;
assume not thesis;
then 1.F = x*0.F by A2,Def10;
hence contradiction;
end;
then x"*(x")" = 1.F by A1,Def10;
then (x*x")*(x")" = x*1.F by GROUP_1:def 3;
then 1.F*(x")" = x*1.F by A1,Def10;
then (x")" = x*1.F;
hence thesis;
end;
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;
reducibility
proof
x <> 0.F;
hence thesis by Th20;
end;
end;
theorem
for F being Field, x being Element of F holds x <> 0.F implies
x" <> 0.F & -x" <> 0.F
proof
let F be Field, x be Element of F;
assume
A1: x <> 0.F;
hereby
assume x" = 0.F;
then 1.F = x*0.F by A1,Def10;
hence contradiction;
end;
assume -x" = 0.F;
then 1.F*x" = (-1.F)*0.F by Th6;
then x*x" = x*0.F;
then 1.F = x*0.F by A1,Def10;
hence contradiction;
end;
theorem Th22:
1.F_Real + 1.F_Real <> 0.F_Real;
definition
let IT be non empty addLoopStr;
attr IT is Fanoian means
for a being Element of IT st a + a = 0.IT holds a = 0.IT;
end;
registration
cluster Fanoian for non empty addLoopStr;
existence
proof
take F = F_Real;
let a be Element of F such that
A1: a + a = 0.F;
a = 1.F * a;
then a + a = (1.F + 1.F) * a by Def7;
hence thesis by A1,Th8,Th22;
end;
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 :: redefines Fanoian (VECTSP_1, definition)
1.F+1.F<>0.F;
compatibility
proof
thus F is Fanoian implies 1.F+1.F<>0.F;
assume
A1: 1.F+1.F<>0.F;
let a be Element of F such that
A2: a + a = 0.F;
a = 1.F * a;
then a + a = (1.F + 1.F) * a by Def7;
hence thesis by A1,A2,Th8;
end;
end;
registration
cluster strict Fanoian for Field;
existence
proof
F_Real is Fanoian;
hence thesis;
end;
end;
theorem
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 by
Th15;
theorem Th24:
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
proof
let F be add-associative right_zeroed right_complementable non empty
addLoopStr, a be Element of F;
--a = a by RLVECT_1:17;
hence thesis by RLVECT_1:12;
end;
theorem
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
proof
let F be add-associative right_zeroed right_complementable non empty
addLoopStr, a,b be Element of F;
a - b = -(b - a) by RLVECT_1:33;
hence thesis by Th24;
end;
theorem
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")
proof
let a, b, c be Element of F;
thus
A1: a <> 0.F & a*c - b = 0.F implies c = b*a"
proof
assume a <> 0.F;
then
A2: a"*a = 1.F by Def10;
assume a*c - b = 0.F;
then a"*(a*c) = b*a" by RLVECT_1:21;
then (a"*a)*c = b*a" by GROUP_1:def 3;
hence thesis by A2;
end;
assume
A3: a <> 0.F;
assume b - c*a = 0.F;
then -(b - c*a) = 0.F by RLVECT_1:12;
hence thesis by A1,A3,RLVECT_1:33;
end;
theorem
for F being add-associative right_zeroed right_complementable non
empty addLoopStr, a, b being Element of F holds a + b = -(-b + -a)
proof
let F be add-associative right_zeroed right_complementable non empty
addLoopStr, a,b be Element of F;
thus a + b = --(a + b) by RLVECT_1:17
.= -(-b + -a) by RLVECT_1:31;
end;
theorem
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
proof
let F be add-associative right_zeroed right_complementable non empty
addLoopStr, a,b,c be Element of F;
thus (b+a)-(c+a) = (b+a)+(-a+-c) by RLVECT_1:31
.= ((b+a)+-a)+-c by RLVECT_1:def 3
.= (b+(a+-a))+-c by RLVECT_1:def 3
.= (b+0.F)+-c by RLVECT_1:5
.= b-c by RLVECT_1:4;
end;
theorem
for G being add-associative right_zeroed right_complementable non
empty addLoopStr, v,w being Element of G holds -(-v+w) = -w+v
proof
let G be add-associative right_zeroed right_complementable non empty
addLoopStr, v,w be Element of G;
thus -(-v+w) = -w + --v by RLVECT_1:31
.= -w + v by RLVECT_1:17;
end;
theorem
for G being Abelian add-associative non empty addLoopStr, u,v,w
being Element of G holds u - v - w = u - w - v
proof
let G be Abelian add-associative non empty addLoopStr, u,v,w be Element of
G;
thus u - v - w = u + -v + -w .= u + -w + -v by RLVECT_1:def 3
.= u - w - v;
end;
theorem
for B being AbGroup holds multMagma (# the carrier of B, the addF of B
#) is commutative Group
proof
let B be AbGroup;
set G = multMagma (# the carrier of B, the addF of B #);
A1: for a,b be Element of G, x,y be Element of B st a = x & b = y holds a *
b = x + y;
A2: G is associative Group-like
proof
reconsider e = 0.B as Element of G;
thus for a,b,c being Element of G holds a * b * c = a * (b * c)
proof
let a,b,c be Element of G;
reconsider x = a, y = b, z = c as Element of B;
thus a * b * c = x + y + z .= x + (y + z) by RLVECT_1:def 3
.= a * (b * c);
end;
take e;
let a be Element of G;
reconsider x = a as Element of B;
thus a * e = x + 0.B .= a by RLVECT_1:4;
reconsider b = - x as Element of G;
thus e * a = x + 0.B by A1
.= a by RLVECT_1:4;
take b;
thus a * b = x + (- x) .= e by RLVECT_1:5;
thus b * a = x + (- x) by A1
.= e by RLVECT_1:5;
end;
now
let a,b be Element of G;
reconsider x = a, y = b as Element of B;
thus a * b = y + x by A1
.= b * a;
end;
hence thesis by A2,GROUP_1:def 12;
end;
begin :: Addenda
:: from COMPTRIG, 2006.08.12, A.T.
theorem
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
proof
let L be add-associative right_zeroed right_complementable
right-distributive unital non empty doubleLoopStr;
let n be Element of NAT;
assume n > 0;
then
A1: n >= 0+1 by NAT_1:13;
n = n-1+1 .= n-'1+1 by A1,XREAL_0:def 2,XREAL_1:19;
hence (power L).(0.L,n) = (power L).(0.L,n-'1)*0.L by GROUP_1:def 7
.= 0.L;
end;
:: 2007.02.14, A.T.
registration
cluster well-unital for non empty multLoopStr;
existence
proof
take F_Real;
thus thesis;
end;
end;
registration
let S be well-unital non empty multLoopStr;
identify 1_S with 1.S;
compatibility by Lm1;
end;
theorem
for L being non empty multLoopStr st L is well-unital holds 1.L = 1_L by Lm1;
definition
let G,H be non empty addMagma;
let f be Function of G,H;
attr f is additive means
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;
reducibility by Def4;
end;
registration
let L be left_unital non empty multLoopStr;
let x be Element of L;
reduce 1.L * x to x;
reducibility by Def8;
end;