let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; :: thesis: for a, b, c being Element of the carrier of F \ {(0. F)} holds (a * b) * c = a * (b * c)
let a, b, c be Element of H1(F) \ {(0. F)}; :: thesis: (a * b) * c = a * (b * c)
set B = H1(F) \ {(0. F)};
set P = (omf F) ! H1(F),(0. F);
reconsider e = 1. F as Element of H1(F) \ {(0. F)} by Lm26;
reconsider D = addLoopStr(# (H1(F) \ {(0. F)}),((omf F) ! H1(F),(0. F)),e #) as strict AbGroup by Def11;
reconsider a = a, b = b, c = c as Element of D ;
A1:
(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 A2:
dom ((omf F) || (H1(F) \ {(0. F)})) = [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):]
by FUNCT_2:def 1;
A3:
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)};
:: thesis: ( the addF of D . s,t is Element of H1(F) \ {(0. F)} & (omf F) . s,t is Element of H1(F) \ {(0. F)} )
A4:
[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 A5:
W = (omf F) || (H1(F) \ {(0. F)})
by A1;
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 A2, A4, A5, FUNCT_1:70;
:: thesis: verum
end;
A6:
for x, y being Element of H1(F) \ {(0. F)} holds (omf F) . x,y = the addF of D . x,y
A7:
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)};
:: thesis: ( (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) )
A8:
the
addF of
D . x,
y is
Element of
H1(
F)
\ {(0. F)}
by A3;
(omf F) . y,
z is
Element of
H1(
F)
\ {(0. F)}
by A3;
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 A6, A8;
:: thesis: verum
end;
reconsider x = a, y = b, z = c as Element of F ;
(x * y) * z =
(omf F) . (the addF of D . a,b),c
by A6
.=
(a + b) + c
by A7
.=
a + (b + c)
by RLVECT_1:def 6
.=
the addF of D . a,((omf F) . b,c)
by A6
.=
x * (y * z)
by A7
;
hence
(a * b) * c = a * (b * c)
; :: thesis: verum