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:13;
dom (SubIsomGroupRel G) = the carrier of (RLMSpace n)
by A2, ORDERS_1:13;
hence
SubIsomGroupRel G is total
by PARTFUN1:def 2; ( SubIsomGroupRel G is symmetric & SubIsomGroupRel G is transitive )
now for x, y being object st x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & [x,y] in SubIsomGroupRel G holds
[y,x] in SubIsomGroupRel Glet x,
y be
object ;
( 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) ;
f in the
carrier of
(IsomGroup n)
by A6, A8;
then
f in ISOM (RLMSpace n)
by Def9;
then reconsider f2 =
f as
onto isometric Function of
(RLMSpace n),
(RLMSpace n) by Def4;
x1 in the
carrier of
(RLMSpace n)
;
then
x1 in dom f2
by FUNCT_2:def 1;
then A9:
(f ") . y1 = x1
by A7, FUNCT_1:34;
f1 " =
f3 "
by GROUP_2:48
.=
f2 "
by Th8
.=
f "
by TOPS_2:def 4
;
hence
[y,x] in SubIsomGroupRel G
by A9, 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 for x, y, z being object st 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 holds
[x,z] in SubIsomGroupRel Glet x,
y,
z be
object ;
( 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 A10:
(
x in the
carrier of
(RLMSpace n) &
y in the
carrier of
(RLMSpace n) &
z in the
carrier of
(RLMSpace n) )
and A11:
[x,y] in SubIsomGroupRel G
and A12:
[y,z] in SubIsomGroupRel G
;
[x,z] in SubIsomGroupRel Greconsider x1 =
x,
y1 =
y,
z1 =
z as
Element of
(RLMSpace n) by A10;
consider f being
Function such that A13:
f in the
carrier of
G
and A14:
f . x1 = y1
by A11, Def10;
reconsider f2 =
f as
Element of
G by A13;
A15:
the
carrier of
G c= the
carrier of
(IsomGroup n)
by GROUP_2:def 5;
then reconsider f3 =
f2 as
Element of
(IsomGroup n) ;
f in the
carrier of
(IsomGroup n)
by A13, A15;
then A16:
f in ISOM (RLMSpace n)
by Def9;
consider g being
Function such that A17:
g in the
carrier of
G
and A18:
g . y1 = z1
by A12, Def10;
reconsider g2 =
g as
Element of
G by A17;
A19:
x1 in the
carrier of
(RLMSpace n)
;
reconsider g3 =
g2 as
Element of
(IsomGroup n) by A15;
(
f2 in G &
g2 in G )
;
then A20:
g3 * f3 in G
by GROUP_2:50;
g in the
carrier of
(IsomGroup n)
by A17, A15;
then
g in ISOM (RLMSpace n)
by Def9;
then
g3 * f3 = g * f
by A16, Def9;
then A21:
g * f in the
carrier of
G
by A20;
f is
onto isometric Function of
(RLMSpace n),
(RLMSpace n)
by A16, Def4;
then
x1 in dom f
by A19, FUNCT_2:def 1;
then
(g * f) . x1 = z1
by A14, A18, FUNCT_1:13;
hence
[x,z] in SubIsomGroupRel G
by A21, 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