set S = SubIsomGroupRel G;
set X = the carrier of (RLMSpace n);
then A2:
SubIsomGroupRel G is_reflexive_in the carrier of (RLMSpace n)
by RELAT_2:def 1;
then A3:
field (SubIsomGroupRel G) = the carrier of (RLMSpace n)
by ORDERS_1:98;
dom (SubIsomGroupRel G) = the carrier of (RLMSpace n)
by A2, ORDERS_1:98;
hence
SubIsomGroupRel G is total
by PARTFUN1:def 4; ( SubIsomGroupRel G is symmetric & SubIsomGroupRel G is transitive )
now let x,
y be
set ;
( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & [x,y] in SubIsomGroupRel G implies [y,x] in SubIsomGroupRel G )assume that A4:
(
x in the
carrier of
(RLMSpace n) &
y in the
carrier of
(RLMSpace n) )
and A5:
[x,y] in SubIsomGroupRel G
;
[y,x] in SubIsomGroupRel Greconsider x1 =
x,
y1 =
y as
Element of
(RLMSpace n) by A4;
consider f being
Function such that A6:
f in the
carrier of
G
and A7:
f . x1 = y1
by A5, Def10;
reconsider f1 =
f as
Element of
G by A6;
A8:
the
carrier of
G c= the
carrier of
(IsomGroup n)
by GROUP_2:def 5;
then reconsider f3 =
f1 as
Element of
(IsomGroup n) by TARSKI:def 3;
f in the
carrier of
(IsomGroup n)
by A6, A8;
then
f in ISOM (RLMSpace n)
by Def9;
then consider f2 being
Function of
(RLMSpace n),
(RLMSpace n) such that A9:
f2 = f
and A10:
f2 is
isometric
by Def4;
x1 in the
carrier of
(RLMSpace n)
;
then
x1 in dom f
by A9, FUNCT_2:def 1;
then A11:
(f " ) . y1 = x1
by A7, A9, A10, FUNCT_1:56;
A12:
rng f2 = the
carrier of
(RLMSpace n)
by A10, Def3;
f1 " =
f3 "
by GROUP_2:57
.=
f2 "
by A9, Th11
.=
f "
by A9, A10, A12, TOPS_2:def 4
;
hence
[y,x] in SubIsomGroupRel G
by A11, Def10;
verum end;
then
SubIsomGroupRel G is_symmetric_in the carrier of (RLMSpace n)
by RELAT_2:def 3;
hence
SubIsomGroupRel G is symmetric
by A3, RELAT_2:def 11; SubIsomGroupRel G is transitive
now let x,
y,
z be
set ;
( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & z in the carrier of (RLMSpace n) & [x,y] in SubIsomGroupRel G & [y,z] in SubIsomGroupRel G implies [x,z] in SubIsomGroupRel G )assume that A13:
(
x in the
carrier of
(RLMSpace n) &
y in the
carrier of
(RLMSpace n) &
z in the
carrier of
(RLMSpace n) )
and A14:
[x,y] in SubIsomGroupRel G
and A15:
[y,z] in SubIsomGroupRel G
;
[x,z] in SubIsomGroupRel Greconsider x1 =
x,
y1 =
y,
z1 =
z as
Element of
(RLMSpace n) by A13;
consider f being
Function such that A16:
f in the
carrier of
G
and A17:
f . x1 = y1
by A14, Def10;
reconsider f2 =
f as
Element of
G by A16;
A18:
the
carrier of
G c= the
carrier of
(IsomGroup n)
by GROUP_2:def 5;
then reconsider f3 =
f2 as
Element of
(IsomGroup n) by TARSKI:def 3;
f in the
carrier of
(IsomGroup n)
by A16, A18;
then A19:
f in ISOM (RLMSpace n)
by Def9;
consider g being
Function such that A20:
g in the
carrier of
G
and A21:
g . y1 = z1
by A15, Def10;
reconsider g2 =
g as
Element of
G by A20;
A22:
x1 in the
carrier of
(RLMSpace n)
;
reconsider g3 =
g2 as
Element of
(IsomGroup n) by A18, TARSKI:def 3;
(
f2 in G &
g2 in G )
by STRUCT_0:def 5;
then A23:
g3 * f3 in G
by GROUP_2:59;
g in the
carrier of
(IsomGroup n)
by A20, A18;
then
g in ISOM (RLMSpace n)
by Def9;
then
g3 * f3 = g * f
by A19, Def9;
then A24:
g * f in the
carrier of
G
by A23, STRUCT_0:def 5;
ex
f1 being
Function of
(RLMSpace n),
(RLMSpace n) st
(
f1 = f &
f1 is
isometric )
by A19, Def4;
then
x1 in dom f
by A22, FUNCT_2:def 1;
then
(g * f) . x1 = z1
by A17, A21, FUNCT_1:23;
hence
[x,z] in SubIsomGroupRel G
by A24, Def10;
verum end;
then
SubIsomGroupRel G is_transitive_in the carrier of (RLMSpace n)
by RELAT_2:def 8;
hence
SubIsomGroupRel G is transitive
by A3, RELAT_2:def 16; verum