:: From Double Loops to Fields
:: by Wojciech Skaba and Micha{\l} Muzalewski
::
:: Received September 27, 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, CARD_1, SUPINF_2, VECTSP_1, SUBSET_1,
RELAT_1, ALGSTR_1, ARYTM_1, ARYTM_3, STRUCT_0, RLVECT_1, BINOP_1,
LATTICES, MESFUNC1, GROUP_1, ALGSTR_2, NUMBERS;
notations SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, REAL_1, STRUCT_0, ALGSTR_0,
RLVECT_1, GROUP_1, VECTSP_1, ALGSTR_1;
constructors BINOP_2, ALGSTR_1, RLVECT_1, VECTSP_1, MEMBERED, REAL_1,
XXREAL_0, NUMBERS, GROUP_1;
registrations VECTSP_1, ALGSTR_1, ALGSTR_0, MEMBERED, XREAL_0;
requirements SUBSET;
theorems VECTSP_1, ALGSTR_1, RLVECT_1, GROUP_1, STRUCT_0, ALGSTR_0, XCMPLX_1;
begin :: DOUBLE LOOPS
reserve L for non empty doubleLoopStr;
Lm1: 0 = 0.F_Real by STRUCT_0:def 6,VECTSP_1:def 5;
Lm2: for a,b being Element of F_Real st a<>0.F_Real
ex x being Element of F_Real st a*x=b
proof
let a,b be Element of F_Real such that
A1: a<>0.F_Real;
reconsider p=a, q=b as Element of REAL by VECTSP_1:def 5;
reconsider x = q/p as Element of F_Real by VECTSP_1:def 5;
p*(q/p) = q by A1,Lm1,XCMPLX_1:87;
then a*x = b;
hence thesis;
end;
Lm3: for a,b being Element of F_Real st a<>0.F_Real ex x being Element of
F_Real st x*a=b
proof
let a,b be Element of F_Real;
assume a<>0.F_Real;
then ex x being Element of F_Real st a*x=b by Lm2;
hence thesis;
end;
Lm4: ( for a,x,y being Element of F_Real st a<>0.F_Real holds a*x=a*y implies
x=y)& for a,x,y being Element of F_Real st a<>0.F_Real holds x*a=y*a implies x=
y by VECTSP_1:5;
Lm5: ( for a being Element of F_Real holds a*0.F_Real = 0.F_Real)& for a being
Element of F_Real holds 0.F_Real*a = 0.F_Real by VECTSP_1:12;
:: Below is the basic definition of the mode of DOUBLE LOOP.
:: The F_Real example in accordance with the many theorems proved above
:: is used to prove the existence.
registration
cluster F_Real -> multLoop_0-like;
coherence by Lm2,Lm3,Lm4,Lm5,ALGSTR_1:16;
end;
:: In the following part of this article the negation and minus functions
:: are defined. This is the only definition of both functions in this article
:: while some of their features are independently proved
:: for various structures.
definition
let L be left_add-cancelable add-right-invertible non empty addLoopStr;
let a be Element of L;
func -a -> Element of L means
:Def1:
a+it = 0.L;
existence by ALGSTR_1:def 4;
uniqueness by ALGSTR_0:def 3;
end;
definition
let L be left_add-cancelable add-right-invertible non empty addLoopStr;
let a,b be Element of L;
func a-b -> Element of L equals
a+ -b;
correctness;
end;
registration
cluster strict Abelian add-associative commutative associative distributive
non degenerated left_zeroed right_zeroed Loop-like well-unital multLoop_0-like
for non empty doubleLoopStr;
existence
proof
take F_Real;
thus thesis;
end;
end;
definition
mode doubleLoop is left_zeroed right_zeroed Loop-like well-unital
multLoop_0-like non empty doubleLoopStr;
end;
definition
mode leftQuasi-Field is Abelian add-associative right-distributive non
degenerated doubleLoop;
end;
reserve a,b,c,x,y,z for Element of L;
:: The following theorem shows that the basic set of axioms of the
:: left quasi-field may be replaced with the following one,
:: by just removing a few and adding some other axioms.
theorem
L is leftQuasi-Field iff (for a holds a + 0.L = a) & (for a ex x st a+
x = 0.L) & (for a,b,c holds (a+b)+c = a+(b+c)) & (for a,b holds a+b = b+a) & 0.
L <> 1.L & (for a holds a * 1.L = a) & (for a holds 1.L * a = a) & (for a,b st
a<>0.L ex x st a*x=b) & (for a,b st a<>0.L ex x st x*a=b) & (for a,x,y st a<>0.
L holds a*x=a*y implies x=y) & (for a,x,y st a<>0.L holds x*a=y*a implies x=y)
& (for a holds a*0.L = 0.L) & (for a holds 0.L*a = 0.L) & for a,b,c holds a*(b+
c) = a*b + a*c
proof
thus L is leftQuasi-Field implies (for a holds a + 0.L = a) & (for a ex x st
a+x = 0.L) & (for a,b,c holds (a+b)+c = a+(b+c)) & (for a,b holds a+b = b+a) &
0.L <> 1.L & (for a holds a * 1.L = a) & (for a holds 1.L * a = a) & (for a,b
st a<>0.L ex x st a*x=b) & (for a,b st a<>0.L ex x st x*a=b) & (for a,x,y st a
<>0.L holds a*x=a*y implies x=y) & (for a,x,y st a<>0.L holds x*a=y*a implies x
=y) & (for a holds a*0.L = 0.L) & (for a holds 0.L*a = 0.L) & for a,b,c holds a
*(b+c) = a*b + a*c by ALGSTR_1:6,16,RLVECT_1:def 2,def 3,def 4,STRUCT_0:def 8
,VECTSP_1:def 2;
assume that
A1: for a holds a + 0.L = a and
A2: for a ex x st a+x = 0.L and
A3: for a,b,c holds (a+b)+c = a+(b+c) and
A4: for a,b holds a+b = b+a and
A5: ( 0.L <> 1.L & for a holds a * 1.L = a )&( ( for a holds 1.L * a = a
)& for a, b st a<>0.L ex x st a*x=b ) & ( ( for a,b st a<>0.L ex x st x*a=b)&
for a,x,y st a<>0.L holds a*x=a*y implies x=y )&( ( for a,x,y st a<>0.L holds
x*a=y*a implies x=y)& for a holds a*0.L = 0.L ) &( ( for a holds 0.L*a = 0.L)&
for a,b,c holds a*(b+c) = a*b + a*c);
A6: for a holds 0.L + a = a
proof
let a;
thus 0.L + a = a + 0.L by A4
.= a by A1;
end;
A7: for a,b ex x st a+x=b
proof
let a,b;
consider y such that
A8: a+y = 0.L by A2;
take x = y+b;
thus a+x = 0.L + b by A3,A8
.= b by A6;
end;
A9: for a,b ex x st x+a=b
proof
let a,b;
consider x such that
A10: a+x=b by A7;
take x;
thus thesis by A4,A10;
end;
A11: for a,x,y holds a+x=a+y implies x=y
proof
let a,x,y;
consider z such that
A12: z+a = 0.L by A1,A2,A3,ALGSTR_1:3;
assume a+x = a+y;
then (z+a)+x = z+(a+y) by A3
.= (z+a)+y by A3;
hence x = 0.L + y by A6,A12
.= y by A6;
end;
for a,x,y holds x+a=y+a implies x=y
proof
let a,x,y;
assume x+a = y+a;
then a+x= y+a by A4
.= a+y by A4;
hence thesis by A11;
end;
hence thesis by A1,A3,A4,A5,A6,A7,A9,A11,ALGSTR_1:6,16,def 2,RLVECT_1:def 2
,def 3,def 4,STRUCT_0:def 8,VECTSP_1:def 2,def 6;
end;
theorem Th2:
for G being Abelian right-distributive doubleLoop, a,b being
Element of G holds a*(-b) = -(a*b)
proof
let G be Abelian right-distributive doubleLoop, a,b be Element of G;
a*b + a*(-b) = a*(b+ -b) by VECTSP_1:def 2
.= a*0.G by Def1
.= 0.G by ALGSTR_1:16;
hence thesis by Def1;
end;
theorem Th3:
for G being Abelian left_add-cancelable add-right-invertible
non empty addLoopStr, a being Element of G holds -(-a) = a
proof
let G be Abelian left_add-cancelable add-right-invertible non empty
addLoopStr, a be Element of G;
-a+a = 0.G by Def1;
hence thesis by Def1;
end;
theorem
for G being Abelian right-distributive doubleLoop holds (-1.G)*(-1.G) = 1.G
proof
let G be Abelian right-distributive doubleLoop;
thus (-1.G)*(-1.G) = -((-1.G)*1_G) by Th2
.= -(-1.G)
.= 1.G by Th3;
end;
theorem
for G being Abelian right-distributive doubleLoop, a,x,y being Element
of G holds a*(x-y) = a*x - a*y
proof
let G be Abelian right-distributive doubleLoop, a,x,y be Element of G;
thus a*(x-y) = a*x + a*(-y) by VECTSP_1:def 2
.= a*x - a*y by Th2;
end;
:: RIGHT QUASI-FIELD
:: The next contemplated algebraic structure is so called right quasi-field.
:: This structure is defined as a DOUBLE LOOP augmented with three axioms.
:: The reasoning is similar to that of left quasi-field.
definition
mode rightQuasi-Field is Abelian add-associative left-distributive non
degenerated doubleLoop;
end;
theorem
L is rightQuasi-Field iff (for a holds a + 0.L = a) & (for a ex x st a
+x = 0.L) & (for a,b,c holds (a+b)+c = a+(b+c)) & (for a,b holds a+b = b+a) &
0.L <> 1.L & (for a holds a * 1.L = a) & (for a holds 1.L * a = a) & (for a,b
st a<>0.L ex x st a*x=b) & (for a,b st a<>0.L ex x st x*a=b) & (for a,x,y st a
<>0.L holds a*x=a*y implies x=y) & (for a,x,y st a<>0.L holds x*a=y*a implies x
=y) & (for a holds a*0.L = 0.L) & (for a holds 0.L*a = 0.L) & for a,b,c holds (
b+c)*a = b*a + c*a
proof
thus L is rightQuasi-Field implies (for a holds a + 0.L = a) & (for a ex x
st a+x = 0.L) & (for a,b,c holds (a+b)+c = a+(b+c)) & (for a,b holds a+b = b+a)
& 0.L <> 1.L & (for a holds a * 1.L = a) & (for a holds 1.L * a = a) & (for a,b
st a<>0.L ex x st a*x=b) & (for a,b st a<>0.L ex x st x*a=b) & (for a,x,y st a
<>0.L holds a*x=a*y implies x=y) & (for a,x,y st a<>0.L holds x*a=y*a implies x
=y) & (for a holds a*0.L = 0.L) & (for a holds 0.L*a = 0.L) & for a,b,c holds (
b+c)*a = b*a + c*a by ALGSTR_1:6,16,RLVECT_1:def 2,def 3,def 4,STRUCT_0:def 8
,VECTSP_1:def 3;
assume that
A1: for a holds a + 0.L = a and
A2: for a ex x st a+x = 0.L and
A3: for a,b,c holds (a+b)+c = a+(b+c) and
A4: for a,b holds a+b = b+a and
A5: ( 0.L <> 1.L & for a holds a * 1.L = a )&( ( for a holds 1.L * a = a
)& for a, b st a<>0.L ex x st a*x=b ) & ( ( for a,b st a<>0.L ex x st x*a=b)&
for a,x,y st a<>0.L holds a*x=a*y implies x=y )&( ( for a,x,y st a<>0.L holds
x*a=y*a implies x=y)& for a holds a*0.L = 0.L ) &( ( for a holds 0.L*a = 0.L)&
for a,b,c holds (b+c)*a = b*a + c*a);
A6: for a,b ex x st x+a=b
proof
let a,b;
consider y such that
A7: y+a = 0.L by A1,A2,A3,ALGSTR_1:3;
take x = b+y;
thus x+a = b + 0.L by A3,A7
.= b by A1;
end;
A8: for a holds 0.L + a = a
proof
let a;
thus 0.L + a = a + 0.L by A4
.= a by A1;
end;
A9: for a,x,y holds a+x=a+y implies x=y
proof
let a,x,y;
consider z such that
A10: z+a = 0.L by A1,A2,A3,ALGSTR_1:3;
assume a+x = a+y;
then (z+a)+x = z+(a+y) by A3
.= (z+a)+y by A3;
hence x = 0.L + y by A8,A10
.= y by A8;
end;
A11: for a,x,y holds x+a=y+a implies x=y
proof
let a,x,y;
consider z such that
A12: a+z = 0.L by A2;
assume x+a = y+a;
then x+(a+z) = (y+a)+z by A3
.= y+(a+z) by A3;
hence x = y + 0.L by A1,A12
.= y by A1;
end;
for a,b ex x st a+x=b
proof
let a,b;
consider y such that
A13: a+y = 0.L by A2;
take x = y+b;
thus a+x = 0.L + b by A3,A13
.= b by A8;
end;
hence thesis by A1,A3,A4,A5,A8,A6,A9,A11,ALGSTR_1:6,16,def 2,RLVECT_1:def 2
,def 3,def 4,STRUCT_0:def 8,VECTSP_1:def 3,def 6;
end;
:: Below, the three features concerned with the - function,
:: numbered 20..22 are proved. Where necessary, a few additional
:: facts are included. They are independent of the similar proofs
:: performed for the left quasi-field.
reserve G for left-distributive doubleLoop,
a,b,x,y for Element of G;
theorem Th7:
(-b)*a = -(b*a)
proof
b*a + (-b)*a = (b+(-b))*a by VECTSP_1:def 3
.= 0.G*a by Def1
.= 0.G by ALGSTR_1:16;
hence thesis by Def1;
end;
theorem
for G being Abelian left-distributive doubleLoop holds (-1.G)*(-1.G) = 1.G
proof
let G be Abelian left-distributive doubleLoop;
thus (-1.G)*(-1.G) = -(1_G*(-1.G)) by Th7
.= -(-1.G)
.= 1.G by Th3;
end;
theorem
(x-y)*a = x*a - y*a
proof
thus (x-y)*a = x*a + (-y)*a by VECTSP_1:def 3
.= x*a - y*a by Th7;
end;
:: DOUBLE SIDED QUASI-FIELD
:: The next contemplated algebraic structure is so called double sided
:: quasi-field. This structure is also defined as a DOUBLE LOOP augmented
:: with four axioms, while its relevance to left/right quasi-field is
:: independently contemplated.
:: The reasoning is similar to that of left/right quasi-field.
definition
mode doublesidedQuasi-Field is Abelian add-associative distributive non
degenerated doubleLoop;
end;
reserve a,b,c,x,y,z for Element of L;
theorem
L is doublesidedQuasi-Field iff (for a holds a + 0.L = a) & (for a ex
x st a+x = 0.L) & (for a,b,c holds (a+b)+c = a+(b+c)) & (for a,b holds a+b = b+
a) & 0.L <> 1.L & (for a holds a * 1.L = a) & (for a holds 1.L * a = a) & (for
a,b st a<>0.L ex x st a*x=b) & (for a,b st a<>0.L ex x st x*a=b) & (for a,x,y
st a<>0.L holds a*x=a*y implies x=y) & (for a,x,y st a<>0.L holds x*a=y*a
implies x=y) & (for a holds a*0.L = 0.L) & (for a holds 0.L*a = 0.L) & (for a,b
,c holds a*(b+c) = a*b + a*c) & for a,b,c holds (b+c)*a = b*a + c*a
proof
thus L is doublesidedQuasi-Field implies (for a holds a + 0.L = a) & (for a
ex x st a+x = 0.L) & (for a,b,c holds (a+b)+c = a+(b+c)) & (for a,b holds a+b =
b+a) & 0.L <> 1.L & (for a holds a * 1.L = a) & (for a holds 1.L * a = a) & (
for a,b st a<>0.L ex x st a*x=b) & (for a,b st a<>0.L ex x st x*a=b) & (for a,x
,y st a<>0.L holds a*x=a*y implies x=y) & (for a,x,y st a<>0.L holds x*a=y*a
implies x=y) & (for a holds a*0.L = 0.L) & (for a holds 0.L*a = 0.L) & (for a,b
,c holds a*(b+c) = a*b + a*c) & for a,b,c holds (b+c)*a = b*a + c*a by
ALGSTR_1:6,16,RLVECT_1:def 2,def 3,def 4,STRUCT_0:def 8,VECTSP_1:def 7;
assume that
A1: for a holds a + 0.L = a and
A2: for a ex x st a+x = 0.L and
A3: for a,b,c holds (a+b)+c = a+(b+c) and
A4: for a,b holds a+b = b+a and
A5: ( 0.L <> 1.L & for a holds a * 1.L = a )&( ( for a holds 1.L * a = a
)& for a, b st a<>0.L ex x st a*x=b ) & ( ( for a,b st a<>0.L ex x st x*a=b)&
for a,x,y st a<>0.L holds a*x=a*y implies x=y )&( ( for a,x,y st a<>0.L holds
x*a=y*a implies x=y)& for a holds a*0.L = 0.L ) &( ( ( for a holds 0.L*a = 0.L)
& for a,b,c holds a*(b+c) = a*b + a*c )& for a,b, c holds (b+c)*a = b*a + c*a);
A6: for a,b ex x st x+a=b
proof
let a,b;
consider y such that
A7: y+a = 0.L by A1,A2,A3,ALGSTR_1:3;
take x = b+y;
thus x+a = b + 0.L by A3,A7
.= b by A1;
end;
A8: for a holds 0.L + a = a
proof
let a;
thus 0.L + a = a + 0.L by A4
.= a by A1;
end;
A9: for a,x,y holds a+x=a+y implies x=y
proof
let a,x,y;
consider z such that
A10: z+a = 0.L by A1,A2,A3,ALGSTR_1:3;
assume a+x = a+y;
then (z+a)+x = z+(a+y) by A3
.= (z+a)+y by A3;
hence x = 0.L + y by A8,A10
.= y by A8;
end;
A11: for a,x,y holds x+a=y+a implies x=y
proof
let a,x,y;
consider z such that
A12: a+z = 0.L by A2;
assume x+a = y+a;
then x+(a+z) = (y+a)+z by A3
.= y+(a+z) by A3;
hence x = y + 0.L by A1,A12
.= y by A1;
end;
for a,b ex x st a+x=b
proof
let a,b;
consider y such that
A13: a+y = 0.L by A2;
take x = y+b;
thus a+x = 0.L + b by A3,A13
.= b by A8;
end;
hence thesis by A1,A3,A4,A5,A8,A6,A9,A11,ALGSTR_1:6,16,def 2,RLVECT_1:def 2
,def 3,def 4,STRUCT_0:def 8,VECTSP_1:def 6,def 7;
end;
:: SKEW FIELD
:: A Skew-Field is defined as a double sided quasi-field extended
:: with the associativity of multiplication.
definition
mode _Skew-Field is associative doublesidedQuasi-Field;
end;
Lm6: 0.L <> 1.L & (for a holds a * 1.L = a) & (for a st a<>0.L ex x st a*x =
1.L) & (for a,b,c holds (a*b)*c = a*(b*c)) & (for a holds a*0.L = 0.L) implies
(a*b = 1.L implies b*a = 1.L)
proof
assume that
A1: 0.L <> 1.L and
A2: for a holds a * 1.L = a and
A3: for a st a<>0.L ex x st a*x = 1.L and
A4: for a,b,c holds (a*b)*c = a*(b*c) and
A5: for a holds a*0.L = 0.L;
thus a*b = 1.L implies b*a = 1.L
proof
assume
A6: a*b = 1.L;
then b<>0.L by A1,A5;
then consider x such that
A7: b * x = 1.L by A3;
thus b*a = (b*a) * (b*x) by A2,A7
.= ((b*a) * b) * x by A4
.= (b * 1.L) * x by A4,A6
.= 1.L by A2,A7;
end;
end;
Lm7: 0.L <> 1.L & (for a holds a * 1.L = a) & (for a st a<>0.L ex x st a*x =
1.L) & (for a,b,c holds (a*b)*c = a*(b*c)) & (for a holds a*0.L = 0.L) implies
1.L*a = a*1.L
proof
assume that
A1: 0.L <> 1.L and
A2: for a holds a * 1.L = a and
A3: for a st a<>0.L ex x st a*x = 1.L and
A4: for a,b,c holds (a*b)*c = a*(b*c) and
A5: for a holds a*0.L = 0.L;
A6: a<>0.L implies 1.L*a = a*1.L
proof
assume a<>0.L;
then consider x such that
A7: a * x = 1.L by A3;
thus 1.L*a = a * (x*a) by A4,A7
.= a*1.L by A1,A2,A3,A4,A5,A7,Lm6;
end;
a=0.L implies 1.L*a = a*1.L
proof
assume
A8: a=0.L;
hence 1.L*a = 0.L by A5
.= a*1.L by A2,A8;
end;
hence thesis by A6;
end;
Lm8: 0.L <> 1.L & (for a holds a * 1.L = a) & (for a st a<>0.L ex x st a*x =
1.L) & (for a,b,c holds (a*b)*c = a*(b*c)) & (for a holds a*0.L = 0.L) implies
for a st a<>0.L ex x st x*a = 1.L
proof
assume that
A1: 0.L <> 1.L & for a holds a * 1.L = a and
A2: for a st a<>0.L ex x st a*x = 1.L and
A3: ( for a,b,c holds (a*b)*c = a*(b*c))& for a holds a*0.L = 0.L;
let a;
assume a<>0.L;
then consider x such that
A4: a * x = 1.L by A2;
x*a=1.L by A1,A2,A3,A4,Lm6;
hence thesis;
end;
:: The following theorem shows that the basic set of axioms of the
:: skew field may be replaced with the following one,
:: by just removing a few and adding some other axioms.
:: A few theorems proved earlier are highly utilized.
theorem Th11:
L is _Skew-Field iff (for a holds a + 0.L = a) & (for a ex x st a+x = 0.L)
& (for a,b,c holds (a+b)+c = a+(b+c)) & (for a,b holds a+b = b+a)
& 0.L <> 1.L & (for a holds a * 1.L = a)
& (for a st a<>0.L ex x st a*x = 1.L) & (for a holds a*0.L = 0.L)
& (for a holds 0.L*a = 0.L) & (for a,b,c holds (a*b)*c = a*(b*c))
& (for a,b,c holds a*(b+c) = a*b + a*c)
& (for a,b,c holds (b+c)*a = b*a + c*a)
proof
thus L is _Skew-Field implies (for a holds a + 0.L = a)
& (for a ex x st a+x = 0.L) & (for a,b,c holds (a+b)+c = a+(b+c))
& (for a,b holds a+b = b+a) & 0.L <> 1.L & (for a holds a * 1.L = a)
& (for a st a<>0.L ex x st a*x = 1.L) & (for a holds a*0.L = 0.L)
& (for a holds 0.L*a = 0.L) & (for a,b,c holds (a*b)*c = a*(b*c))
& (for a,b,c holds a*(b+c) = a*b + a*c)
& (for a,b,c holds (b+c)*a = b*a + c*a) by ALGSTR_1:6,16,GROUP_1:def 3
,RLVECT_1:def 2,def 3,def 4,STRUCT_0:def 8,VECTSP_1:def 7;
assume
A1: (for a holds a + 0.L = a) & (for a ex x st a+x = 0.L)
& (for a,b,c holds (a+b)+c = a+(b+c)) & (for a,b holds a+b = b+a)
& 0.L <> 1.L & (for a holds a * 1.L = a)
& (for a st a<>0.L ex x st a*x = 1.L) & (for a holds a*0.L = 0.L)
& (for a holds 0.L*a = 0.L) & (for a,b,c holds (a*b)*c = a*(b*c))
& (for a,b,c holds a*(b+c) = a*b + a*c)
& (for a,b,c holds (b+c)*a = b*a + c*a);
now thus
A2: for a holds 0.L + a = a
proof
let a;
thus 0.L + a = a + 0.L by A1
.= a by A1;
end;
thus for a,b ex x st a+x=b
proof
let a,b;
consider y such that
A3: a+y = 0.L by A1;
take x = y+b;
thus a+x = 0.L + b by A1,A3
.= b by A2;
end;
thus for a,b ex x st x+a=b
proof
let a,b;
consider y such that
A4: y+a = 0.L by A1,ALGSTR_1:3;
take x = b+y;
thus x+a = b + 0.L by A1,A4
.= b by A1;
end;
thus for a,x,y holds a+x=a+y implies x=y
proof
let a,x,y;
consider z such that
A5: z+a = 0.L by A1,ALGSTR_1:3;
assume a+x = a+y;
then (z+a)+x = z+(a+y) by A1
.= (z+a)+y by A1;
hence x = 0.L + y by A2,A5
.= y by A2;
end;
thus for a,x,y holds x+a=y+a implies x=y
proof
let a,x,y;
consider z such that
A6: a+z = 0.L by A1;
assume x+a = y+a;
then x+(a+z) = (y+a)+z by A1
.= y+(a+z) by A1;
hence x = y + 0.L by A1,A6
.= y by A1;
end; thus
A7: for a holds 1.L * a = a
proof
let a;
thus 1.L*a = a*1.L by A1,Lm7
.= a by A1;
end;
thus for a,b st a<>0.L ex x st a*x=b
proof
let a,b;
assume a<>0.L;
then consider y such that
A8: a*y = 1.L by A1;
take x = y*b;
thus a*x = 1.L * b by A1,A8
.= b by A7;
end;
thus for a,b st a<>0.L ex x st x*a=b
proof
let a,b;
assume a<>0.L;
then consider y such that
A9: y*a = 1.L by A1,Lm8;
take x = b*y;
thus x*a = b * 1.L by A1,A9
.= b by A1;
end;
thus for a,x,y st a<>0.L holds a*x=a*y implies x=y
proof
let a,x,y;
assume a<>0.L;
then consider z such that
A10: z*a = 1.L by A1,Lm8;
assume a*x = a*y;
then (z*a)*x = z*(a*y) by A1
.= (z*a)*y by A1;
hence x = 1.L * y by A7,A10
.= y by A7;
end;
thus for a,x,y st a<>0.L holds x*a=y*a implies x=y
proof
let a,x,y;
assume a<>0.L;
then consider z such that
A11: a*z = 1.L by A1;
assume x*a = y*a;
then x*(a*z) = (y*a)*z by A1
.= y*(a*z) by A1;
hence x = y * 1.L by A1,A11
.= y by A1;
end;
end;
hence thesis by A1,ALGSTR_1:6,16,def 2,GROUP_1:def 3,RLVECT_1:def 2,def 3
,def 4,STRUCT_0:def 8,VECTSP_1:def 6,def 7;
end;
:: FIELD
:: A _Field is defined as a Skew-Field with the axiom of the commutativity
:: of multiplication.
definition
mode _Field is commutative _Skew-Field;
end;
theorem
L is _Field iff (for a holds a + 0.L = a) & (for a ex x st a+x = 0.L)
& (for a,b,c holds (a+b)+c = a+(b+c)) & (for a,b holds a+b = b+a) & 0.L <> 1.L
& (for a holds a * 1.L = a) & (for a st a<>0.L ex x st a*x = 1.L) & (for a
holds a*0.L = 0.L) & (for a,b,c holds (a*b)*c = a*(b*c)) & (for a,b,c holds a*(
b+c) = a*b + a*c) & for a,b holds a*b = b*a
proof
thus L is _Field implies (for a holds a + 0.L = a) & (for a ex x st a+x = 0.
L) & (for a,b,c holds (a+b)+c = a+(b+c)) & (for a,b holds a+b = b+a) & 0.L <>
1.L & (for a holds a * 1.L = a) & (for a st a<>0.L ex x st a*x = 1.L) & (for a
holds a*0.L = 0.L) & (for a,b,c holds (a*b)*c = a*(b*c)) & (for a,b,c holds a*(
b+c) = a*b + a*c) & for a,b holds a*b = b*a by Th11,GROUP_1:def 12;
assume that
A1: ( ( for a holds a + 0.L = a)& for a ex x st a+x = 0.L )&( ( for a,b,
c holds ( a +b)+c = a+(b+c))& for a,b holds a+b = b+a ) &( ( 0.L <> 1.L & for a
holds a * 1.L = a )& for a st a<>0.L ex x st a*x = 1.L ) and
A2: for a holds a*0.L = 0.L and
A3: for a,b,c holds (a*b)*c = a*(b*c) and
A4: for a,b,c holds a*(b+c) = a*b + a*c and
A5: for a,b holds a*b = b*a;
A6: for a holds 0.L*a = 0.L
proof
let a;
thus 0.L*a = a*0.L by A5
.= 0.L by A2;
end;
for a,b,c holds (b+c)*a = b*a + c*a
proof
let a,b,c;
thus (b+c)*a = a*(b+c) by A5
.= a*b + a*c by A4
.= b*a + a*c by A5
.= b*a + c*a by A5;
end;
hence thesis by A1,A2,A3,A4,A5,A6,Th11,GROUP_1:def 12;
end;