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
object such that A3:
x in NonZero L
and A4:
y in NonZero L
and A5:
z = [x,y]
by ZFMISC_1:84;
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:12;
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 the carrier of L \ {(0. L)} -subsetpreserving
by REALSET1:def 4; REALSET2:def 4 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 the carrier of L \ {(0. L)} -subsetpreserving BinOp of L by A2, REALSET1:def 4;
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 2 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:49
.=
b * a
by A1, GROUP_1:def 12
.=
w + v
by A7, A9, A11, FUNCT_1:49
;
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;
A14:
a * b = 1. L
by A1, A13, GROUP_1:def 12;
then
b <> 0. L
by A1, VECTSP_1:6;
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:49;
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 3 (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:5;
then A17:
[u,((om || B) . (v,w))] in [:B,B:]
by A7, A9, ZFMISC_1:87;
A18:
[u,v] in [:B,B:]
;
then
P . (
u,
v)
in B
by FUNCT_2:5;
then
[((om || B) . (u,v)),w] in [:B,B:]
by A7, A9, ZFMISC_1:87;
hence (u + v) + w =
om . (
((om || B) . (u,v)),
w)
by A7, A9, FUNCT_1:49
.=
(a * b) * c
by A18, FUNCT_1:49
.=
a * (b * c)
by A1, GROUP_1:def 3
.=
om . (
u,
((om || B) . (v,w)))
by A16, FUNCT_1:49
.=
u + (v + w)
by A7, A9, A17, FUNCT_1:49
;
verum
end;
addLoopStr(# B,P,e #) is right_zeroed
proof
let v be
Element of
addLoopStr(#
B,
P,
e #);
RLVECT_1:def 4 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:49
.=
v
by A1
;
verum
end;
hence
addLoopStr(# B,P,e #) is AbGroup
by A10, A15, A12; verum