:: From Double Loops to Fields
:: by Wojciech Skaba and Micha{\l} Muzalewski
::
:: Received September 27, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
0 = 0. F_Real
by STRUCT_0:def 6, VECTSP_1:def 15;
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:33;
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:44;
:: deftheorem ALGSTR_2:def 1 :
canceled;
:: deftheorem ALGSTR_2:def 2 :
canceled;
:: deftheorem ALGSTR_2:def 3 :
canceled;
:: deftheorem ALGSTR_2:def 4 :
canceled;
:: deftheorem ALGSTR_2:def 5 :
canceled;
:: deftheorem ALGSTR_2:def 6 :
canceled;
:: deftheorem Def7 defines - ALGSTR_2:def 7 :
:: deftheorem defines - ALGSTR_2:def 8 :
theorem :: ALGSTR_2:1
canceled;
theorem :: ALGSTR_2:2
canceled;
theorem :: ALGSTR_2:3
canceled;
theorem :: ALGSTR_2:4
canceled;
theorem :: ALGSTR_2:5
canceled;
theorem :: ALGSTR_2:6
canceled;
theorem :: ALGSTR_2:7
canceled;
theorem :: ALGSTR_2:8
canceled;
theorem :: ALGSTR_2:9
canceled;
theorem :: ALGSTR_2:10
canceled;
theorem :: ALGSTR_2:11
canceled;
theorem :: ALGSTR_2:12
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 :: ALGSTR_2:13
canceled;
theorem Th14: :: ALGSTR_2:14
theorem Th15: :: ALGSTR_2:15
theorem :: ALGSTR_2:16
theorem :: ALGSTR_2:17
theorem :: ALGSTR_2:18
canceled;
theorem :: ALGSTR_2:19
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 :: ALGSTR_2:20
canceled;
theorem Th21: :: ALGSTR_2:21
theorem :: ALGSTR_2:22
canceled;
theorem :: ALGSTR_2:23
theorem :: ALGSTR_2:24
theorem :: ALGSTR_2:25
canceled;
theorem :: ALGSTR_2:26
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
theorem :: ALGSTR_2:27
canceled;
theorem :: ALGSTR_2:28
canceled;
theorem :: ALGSTR_2:29
canceled;
theorem :: ALGSTR_2:30
canceled;
theorem :: ALGSTR_2:31
canceled;
theorem Th32: :: ALGSTR_2:32
theorem :: ALGSTR_2:33
canceled;
theorem :: ALGSTR_2:34