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, Def11;
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:11;
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:70;
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 6
.=
the addF of D . a,((omf F) . b,c)
by A4
.=
x * (y * z)
by A8
;
hence
(a * b) * c = a * (b * c)
; verum