now let x,
y,
z be
Element of
(IsomGroup n);
(x * y) * z = x * (y * z)
x in the
carrier of
(IsomGroup n)
;
then A1:
x in ISOM (RLMSpace n)
by Def9;
then consider x1 being
Function of
(RLMSpace n),
(RLMSpace n) such that A2:
x1 = x
and A3:
x1 is
isometric
by Def4;
y in the
carrier of
(IsomGroup n)
;
then A4:
y in ISOM (RLMSpace n)
by Def9;
then consider y1 being
Function of
(RLMSpace n),
(RLMSpace n) such that A5:
y1 = y
and A6:
y1 is
isometric
by Def4;
x1 * y1 is
isometric
by A3, A6, Th4;
then A7:
x1 * y1 in ISOM (RLMSpace n)
by Def4;
z in the
carrier of
(IsomGroup n)
;
then A8:
z in ISOM (RLMSpace n)
by Def9;
then consider z1 being
Function of
(RLMSpace n),
(RLMSpace n) such that A9:
z1 = z
and A10:
z1 is
isometric
by Def4;
y1 * z1 is
isometric
by A6, A10, Th4;
then A11:
y1 * z1 in ISOM (RLMSpace n)
by Def4;
thus (x * y) * z =
the
multF of
(IsomGroup n) . (x1 * y1),
z
by A1, A2, A4, A5, Def9
.=
(x1 * y1) * z1
by A8, A9, A7, Def9
.=
x1 * (y1 * z1)
by RELAT_1:55
.=
the
multF of
(IsomGroup n) . x,
(y1 * z1)
by A1, A2, A11, Def9
.=
x * (y * z)
by A4, A5, A8, A9, Def9
;
verum end;
hence
IsomGroup n is associative
by GROUP_1:def 4; IsomGroup n is Group-like
ex e being Element of (IsomGroup n) st
for h being Element of (IsomGroup n) holds
( h * e = h & e * h = h & ex g being Element of (IsomGroup n) st
( h * g = e & g * h = e ) )
proof
id (RLMSpace n) is
isometric
by Th5;
then A12:
id (RLMSpace n) in ISOM (RLMSpace n)
by Def4;
then reconsider e =
id (RLMSpace n) as
Element of
(IsomGroup n) by Def9;
take
e
;
for h being Element of (IsomGroup n) holds
( h * e = h & e * h = h & ex g being Element of (IsomGroup n) st
( h * g = e & g * h = e ) )
let h be
Element of
(IsomGroup n);
( h * e = h & e * h = h & ex g being Element of (IsomGroup n) st
( h * g = e & g * h = e ) )
h in the
carrier of
(IsomGroup n)
;
then A13:
h in ISOM (RLMSpace n)
by Def9;
then consider h1 being
Function of
(RLMSpace n),
(RLMSpace n) such that A14:
h1 = h
and A15:
h1 is
isometric
by Def4;
thus h * e =
h1 * (id the carrier of (RLMSpace n))
by A12, A13, A14, Def9
.=
h
by A14, FUNCT_2:23
;
( e * h = h & ex g being Element of (IsomGroup n) st
( h * g = e & g * h = e ) )
thus e * h =
(id the carrier of (RLMSpace n)) * h1
by A12, A13, A14, Def9
.=
h
by A14, FUNCT_2:23
;
ex g being Element of (IsomGroup n) st
( h * g = e & g * h = e )
A16:
rng h1 = [#] (RLMSpace n)
by A15, Def3;
h1 " is
isometric
by A15, Th3;
then A17:
h1 " in ISOM (RLMSpace n)
by Def4;
then reconsider g =
h1 " as
Element of
(IsomGroup n) by Def9;
take
g
;
( h * g = e & g * h = e )
thus h * g =
h1 * (h1 " )
by A13, A14, A17, Def9
.=
e
by A15, A16, TOPS_2:65
;
g * h = e
thus g * h =
(h1 " ) * h1
by A13, A14, A17, Def9
.=
id (dom h1)
by A15, A16, TOPS_2:65
.=
e
by FUNCT_2:def 1
;
verum
end;
hence
IsomGroup n is Group-like
by GROUP_1:def 3; verum