let L be non degenerated doubleLoopStr ; ( L is add-associative & L is right_zeroed & L is right_complementable & L is Abelian & L is commutative & L is associative & L is well-unital & L is distributive & L is almost_left_invertible implies L is Field-like )
set B = NonZero L;
assume A1:
( L is add-associative & L is right_zeroed & L is right_complementable & L is Abelian & L is commutative & L is associative & L is well-unital & L is distributive & L is almost_left_invertible )
; L is Field-like
A2:
for y being set st y in [:(NonZero L),(NonZero L):] holds
the multF of L . y in NonZero L
proof
let z be
set ;
( z in [:(NonZero L),(NonZero L):] implies the multF of L . z in NonZero L )
assume
z in [:(NonZero L),(NonZero L):]
;
the multF of L . z in NonZero L
then consider x,
y being
set such that A3:
x in NonZero L
and A4:
y in NonZero L
and A5:
z = [x,y]
by ZFMISC_1:103;
reconsider x =
x,
y =
y as
Element of
L by A3, A4;
not
y in {(0. L)}
by A4, XBOOLE_0:def 5;
then A6:
y <> 0. L
by TARSKI:def 1;
not
x in {(0. L)}
by A3, XBOOLE_0:def 5;
then
x <> 0. L
by TARSKI:def 1;
then
x * y <> 0. L
by A1, A6, VECTSP_1:44;
then
not
x * y in {(0. L)}
by TARSKI:def 1;
hence
the
multF of
L . z in NonZero L
by A5, XBOOLE_0:def 5;
verum
end;
hence
the multF of L is DnT of 0. L,the carrier of L
by REALSET1:def 8; REALSET2:def 11 for B being non empty set
for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup
reconsider om = the multF of L as DnT of 0. L,the carrier of L by A2, REALSET1:def 8;
let B be non empty set ; for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup
let P be BinOp of B; for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup
let e be Element of B; ( B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) implies addLoopStr(# B,P,e #) is AbGroup )
assume that
A7:
B = NonZero L
and
A8:
e = 1. L
and
A9:
P = the multF of L || (NonZero L)
; addLoopStr(# B,P,e #) is AbGroup
set K = addLoopStr(# B,P,e #);
A10:
addLoopStr(# B,P,e #) is Abelian
proof
let v,
w be
Element of
addLoopStr(#
B,
P,
e #);
RLVECT_1:def 5 v + w = w + v
reconsider a =
v,
b =
w as
Element of
L by A7, XBOOLE_0:def 5;
A11:
[w,v] in [:B,B:]
;
[v,w] in [:B,B:]
;
hence v + w =
a * b
by A7, A9, FUNCT_1:72
.=
b * a
by A1, GROUP_1:def 16
.=
w + v
by A7, A9, A11, FUNCT_1:72
;
verum
end;
A12:
addLoopStr(# B,P,e #) is right_complementable
proof
let v be
Element of
addLoopStr(#
B,
P,
e #);
ALGSTR_0:def 16 v is right_complementable
reconsider a =
v as
Element of
L by A7, XBOOLE_0:def 5;
not
a in {(0. L)}
by A7, XBOOLE_0:def 5;
then
a <> 0. L
by TARSKI:def 1;
then consider b being
Element of
L such that A13:
b * a = 1. L
by A1, VECTSP_1:def 20;
A14:
a * b = 1. L
by A1, A13, GROUP_1:def 16;
then
b <> 0. L
by A1, VECTSP_1:36;
then
not
b in {(0. L)}
by TARSKI:def 1;
then reconsider w =
b as
Element of
addLoopStr(#
B,
P,
e #)
by A7, XBOOLE_0:def 5;
take
w
;
ALGSTR_0:def 11 v + w = 0. addLoopStr(# B,P,e #)
[v,w] in [:B,B:]
;
hence
v + w = 0. addLoopStr(#
B,
P,
e #)
by A7, A8, A9, A14, FUNCT_1:72;
verum
end;
A15:
addLoopStr(# B,P,e #) is add-associative
proof
let u,
v,
w be
Element of
addLoopStr(#
B,
P,
e #);
RLVECT_1:def 6 (u + v) + w = u + (v + w)
reconsider a =
u,
b =
v,
c =
w as
Element of
L by A7, XBOOLE_0:def 5;
A16:
[v,w] in [:B,B:]
;
then
P . v,
w in B
by FUNCT_2:7;
then A17:
[u,((om || B) . v,w)] in [:B,B:]
by A7, A9, ZFMISC_1:106;
A18:
[u,v] in [:B,B:]
;
then
P . u,
v in B
by FUNCT_2:7;
then
[((om || B) . u,v),w] in [:B,B:]
by A7, A9, ZFMISC_1:106;
hence (u + v) + w =
om . ((om || B) . u,v),
w
by A7, A9, FUNCT_1:72
.=
(a * b) * c
by A18, FUNCT_1:72
.=
a * (b * c)
by A1, GROUP_1:def 4
.=
om . u,
((om || B) . v,w)
by A16, FUNCT_1:72
.=
u + (v + w)
by A7, A9, A17, FUNCT_1:72
;
verum
end;
addLoopStr(# B,P,e #) is right_zeroed
proof
let v be
Element of
addLoopStr(#
B,
P,
e #);
RLVECT_1:def 7 v + (0. addLoopStr(# B,P,e #)) = v
reconsider a =
v as
Element of
L by A7, XBOOLE_0:def 5;
[v,(0. addLoopStr(# B,P,e #))] in [:B,B:]
;
hence v + (0. addLoopStr(# B,P,e #)) =
a * (1. L)
by A7, A8, A9, FUNCT_1:72
.=
v
by A1, VECTSP_1:def 16
;
verum
end;
hence
addLoopStr(# B,P,e #) is AbGroup
by A10, A15, A12; verum