now for x, y, z being Element of (IsomGroup n) holds (x * y) * z = x * (y * z)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 reconsider x1 =
x as
onto isometric Function of
(RLMSpace n),
(RLMSpace n) by Def4;
y in the
carrier of
(IsomGroup n)
;
then A2:
y in ISOM (RLMSpace n)
by Def9;
then reconsider y1 =
y as
onto isometric Function of
(RLMSpace n),
(RLMSpace n) by Def4;
A3:
x1 * y1 in ISOM (RLMSpace n)
by Def4;
z in the
carrier of
(IsomGroup n)
;
then A4:
z in ISOM (RLMSpace n)
by Def9;
then reconsider z1 =
z as
onto isometric Function of
(RLMSpace n),
(RLMSpace n) by Def4;
A5:
y1 * z1 in ISOM (RLMSpace n)
by Def4;
thus (x * y) * z =
the
multF of
(IsomGroup n) . (
(x1 * y1),
z)
by A1, A2, Def9
.=
(x1 * y1) * z1
by A4, A3, Def9
.=
x1 * (y1 * z1)
by RELAT_1:36
.=
the
multF of
(IsomGroup n) . (
x,
(y1 * z1))
by A1, A5, Def9
.=
x * (y * z)
by A2, A4, Def9
;
verum end;
hence
IsomGroup n is associative
by GROUP_1:def 3; 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
A6:
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 A7:
h in ISOM (RLMSpace n)
by Def9;
then reconsider h1 =
h as
onto isometric Function of
(RLMSpace n),
(RLMSpace n) by Def4;
thus h * e =
h1 * (id the carrier of (RLMSpace n))
by A6, A7, Def9
.=
h
by FUNCT_2:17
;
( 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 A6, A7, Def9
.=
h
by FUNCT_2:17
;
ex g being Element of (IsomGroup n) st
( h * g = e & g * h = e )
A8:
rng h1 = [#] (RLMSpace n)
by FUNCT_2:def 3;
A9:
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 A7, A9, Def9
.=
e
by A8, TOPS_2:52
;
g * h = e
thus g * h =
(h1 ") * h1
by A7, A9, Def9
.=
id (dom h1)
by A8, TOPS_2:52
.=
e
by FUNCT_2:def 1
;
verum
end;
hence
IsomGroup n is Group-like
by GROUP_1:def 2; verum