environ
vocabularies HIDDEN, 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 HIDDEN, SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, REAL_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, ALGSTR_1;
definitions ;
theorems VECTSP_1, ALGSTR_1, RLVECT_1, GROUP_1, STRUCT_0, ALGSTR_0, XCMPLX_1;
schemes ;
registrations VECTSP_1, ALGSTR_1, ALGSTR_0, MEMBERED, XREAL_0;
constructors HIDDEN, BINOP_2, ALGSTR_1, RLVECT_1, VECTSP_1, MEMBERED, REAL_1, XXREAL_0, NUMBERS, GROUP_1;
requirements HIDDEN, SUBSET;
equalities ;
expansions ;
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 holds
ex x being Element of F_Real st a * x = b
Lm3:
for a, b being Element of F_Real st a <> 0. F_Real holds
ex x being Element of F_Real st x * a = b
Lm4:
( ( for a, x, y being Element of F_Real st a <> 0. F_Real & a * x = a * y holds
x = y ) & ( for a, x, y being Element of F_Real st a <> 0. F_Real & x * a = y * a holds
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;
theorem
for
L being non
empty doubleLoopStr holds
(
L is
leftQuasi-Field iff ( ( for
a being
Element of
L holds
a + (0. L) = a ) & ( for
a being
Element of
L ex
x being
Element of
L st
a + x = 0. L ) & ( for
a,
b,
c being
Element of
L holds
(a + b) + c = a + (b + c) ) & ( for
a,
b being
Element of
L holds
a + b = b + a ) &
0. L <> 1. L & ( for
a being
Element of
L holds
a * (1. L) = a ) & ( for
a being
Element of
L holds
(1. L) * a = a ) & ( for
a,
b being
Element of
L st
a <> 0. L holds
ex
x being
Element of
L st
a * x = b ) & ( for
a,
b being
Element of
L st
a <> 0. L holds
ex
x being
Element of
L st
x * a = b ) & ( for
a,
x,
y being
Element of
L st
a <> 0. L &
a * x = a * y holds
x = y ) & ( for
a,
x,
y being
Element of
L st
a <> 0. L &
x * a = y * a holds
x = y ) & ( for
a being
Element of
L holds
a * (0. L) = 0. L ) & ( for
a being
Element of
L holds
(0. L) * a = 0. L ) & ( for
a,
b,
c being
Element of
L holds
a * (b + c) = (a * b) + (a * c) ) ) )
theorem
for
L being non
empty doubleLoopStr holds
(
L is
rightQuasi-Field iff ( ( for
a being
Element of
L holds
a + (0. L) = a ) & ( for
a being
Element of
L ex
x being
Element of
L st
a + x = 0. L ) & ( for
a,
b,
c being
Element of
L holds
(a + b) + c = a + (b + c) ) & ( for
a,
b being
Element of
L holds
a + b = b + a ) &
0. L <> 1. L & ( for
a being
Element of
L holds
a * (1. L) = a ) & ( for
a being
Element of
L holds
(1. L) * a = a ) & ( for
a,
b being
Element of
L st
a <> 0. L holds
ex
x being
Element of
L st
a * x = b ) & ( for
a,
b being
Element of
L st
a <> 0. L holds
ex
x being
Element of
L st
x * a = b ) & ( for
a,
x,
y being
Element of
L st
a <> 0. L &
a * x = a * y holds
x = y ) & ( for
a,
x,
y being
Element of
L st
a <> 0. L &
x * a = y * a holds
x = y ) & ( for
a being
Element of
L holds
a * (0. L) = 0. L ) & ( for
a being
Element of
L holds
(0. L) * a = 0. L ) & ( for
a,
b,
c being
Element of
L holds
(b + c) * a = (b * a) + (c * a) ) ) )
theorem
for
L being non
empty doubleLoopStr holds
(
L is
doublesidedQuasi-Field iff ( ( for
a being
Element of
L holds
a + (0. L) = a ) & ( for
a being
Element of
L ex
x being
Element of
L st
a + x = 0. L ) & ( for
a,
b,
c being
Element of
L holds
(a + b) + c = a + (b + c) ) & ( for
a,
b being
Element of
L holds
a + b = b + a ) &
0. L <> 1. L & ( for
a being
Element of
L holds
a * (1. L) = a ) & ( for
a being
Element of
L holds
(1. L) * a = a ) & ( for
a,
b being
Element of
L st
a <> 0. L holds
ex
x being
Element of
L st
a * x = b ) & ( for
a,
b being
Element of
L st
a <> 0. L holds
ex
x being
Element of
L st
x * a = b ) & ( for
a,
x,
y being
Element of
L st
a <> 0. L &
a * x = a * y holds
x = y ) & ( for
a,
x,
y being
Element of
L st
a <> 0. L &
x * a = y * a holds
x = y ) & ( for
a being
Element of
L holds
a * (0. L) = 0. L ) & ( for
a being
Element of
L holds
(0. L) * a = 0. L ) & ( for
a,
b,
c being
Element of
L holds
a * (b + c) = (a * b) + (a * c) ) & ( for
a,
b,
c being
Element of
L holds
(b + c) * a = (b * a) + (c * a) ) ) )
Lm6:
for L being non empty doubleLoopStr
for a, b being Element of L st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) & a * b = 1. L holds
b * a = 1. L
Lm7:
for L being non empty doubleLoopStr
for a being Element of L st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) holds
(1. L) * a = a * (1. L)
Lm8:
for L being non empty doubleLoopStr st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) holds
for a being Element of L st a <> 0. L holds
ex x being Element of L st x * a = 1. L
:: The F_Real example in accordance with the many theorems proved above
:: is used to prove the existence.