let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; for a, b, c being Element of NonZero F holds (a * b) * c = a * (b * c)
let a, b, c be Element of NonZero F; (a * b) * c = a * (b * c)
set B = H1(F) \ {(0. F)};
set P = (omf F) ! (H1(F),(0. F));
A1:
H1(F) \ {(0. F)} = NonZero F
;
then reconsider e = 1. F as Element of H1(F) \ {(0. F)} by STRUCT_0:2;
reconsider D = addLoopStr(# (H1(F) \ {(0. F)}),((omf F) ! (H1(F),(0. F))),e #) as strict AbGroup by A1, Def4;
reconsider a = a, b = b, c = c as Element of D ;
reconsider x = a, y = b, z = c as Element of F ;
A2:
(omf F) || (H1(F) \ {(0. F)}) is Function of [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):],(H1(F) \ {(0. F)})
by REALSET1:7;
then A3:
dom ((omf F) || (H1(F) \ {(0. F)})) = [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):]
by FUNCT_2:def 1;
A4:
for x, y being Element of H1(F) \ {(0. F)} holds (omf F) . (x,y) = the addF of D . (x,y)
A5:
for s, t being Element of H1(F) \ {(0. F)} holds
( the addF of D . (s,t) is Element of H1(F) \ {(0. F)} & (omf F) . (s,t) is Element of H1(F) \ {(0. F)} )
proof
let s,
t be
Element of
H1(
F)
\ {(0. F)};
( the addF of D . (s,t) is Element of H1(F) \ {(0. F)} & (omf F) . (s,t) is Element of H1(F) \ {(0. F)} )
A6:
[s,t] in [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):]
;
consider W being
Function of
[:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):],
(H1(F) \ {(0. F)}) such that A7:
W = (omf F) || (H1(F) \ {(0. F)})
by A2;
W . (
s,
t) is
Element of
H1(
F)
\ {(0. F)}
;
hence
( the
addF of
D . (
s,
t) is
Element of
H1(
F)
\ {(0. F)} &
(omf F) . (
s,
t) is
Element of
H1(
F)
\ {(0. F)} )
by A3, A6, A7, FUNCT_1:47;
verum
end;
A8:
for x, y, z being Element of H1(F) \ {(0. F)} holds
( (omf F) . (( the addF of D . (x,y)),z) = the addF of D . (( the addF of D . (x,y)),z) & the addF of D . (x,((omf F) . (y,z))) = (omf F) . (x,((omf F) . (y,z))) )
proof
let x,
y,
z be
Element of
H1(
F)
\ {(0. F)};
( (omf F) . (( the addF of D . (x,y)),z) = the addF of D . (( the addF of D . (x,y)),z) & the addF of D . (x,((omf F) . (y,z))) = (omf F) . (x,((omf F) . (y,z))) )
A9:
(omf F) . (
y,
z) is
Element of
H1(
F)
\ {(0. F)}
by A5;
the
addF of
D . (
x,
y) is
Element of
H1(
F)
\ {(0. F)}
by A5;
hence
(
(omf F) . (
( the addF of D . (x,y)),
z)
= the
addF of
D . (
( the addF of D . (x,y)),
z) & the
addF of
D . (
x,
((omf F) . (y,z)))
= (omf F) . (
x,
((omf F) . (y,z))) )
by A4, A9;
verum
end;
(x * y) * z =
(omf F) . (( the addF of D . (a,b)),c)
by A4
.=
(a + b) + c
by A8
.=
a + (b + c)
by RLVECT_1:def 3
.=
the addF of D . (a,((omf F) . (b,c)))
by A4
.=
x * (y * z)
by A8
;
hence
(a * b) * c = a * (b * c)
; verum