set S = SubIsomGroupRel G;
set X = the carrier of ();
now :: thesis: for x being object st x in the carrier of () holds
[x,x] in SubIsomGroupRel G
let x be object ; :: thesis: ( x in the carrier of () implies [x,x] in SubIsomGroupRel G )
assume x in the carrier of () ; :: thesis:
then reconsider x1 = x as Element of () ;
1_ () = id () by Th7;
then id () in G by GROUP_2:46;
then A1: id () in the carrier of G ;
(id ()) . x1 = x1 ;
hence [x,x] in SubIsomGroupRel G by ; :: thesis: verum
end;
then A2: SubIsomGroupRel G is_reflexive_in the carrier of () by RELAT_2:def 1;
then A3: field () = the carrier of () by ORDERS_1:13;
dom () = the carrier of () by ;
hence SubIsomGroupRel G is total by PARTFUN1:def 2; :: thesis:
now :: thesis: for x, y being object st x in the carrier of () & y in the carrier of () & [x,y] in SubIsomGroupRel G holds
[y,x] in SubIsomGroupRel G
let x, y be object ; :: thesis: ( x in the carrier of () & y in the carrier of () & [x,y] in SubIsomGroupRel G implies [y,x] in SubIsomGroupRel G )
assume that
A4: ( x in the carrier of () & y in the carrier of () ) and
A5: [x,y] in SubIsomGroupRel G ; :: thesis:
reconsider x1 = x, y1 = y as Element of () by A4;
consider f being Function such that
A6: f in the carrier of G and
A7: f . x1 = y1 by ;
reconsider f1 = f as Element of G by A6;
A8: the carrier of G c= the carrier of () by GROUP_2:def 5;
then reconsider f3 = f1 as Element of () ;
f in the carrier of () by A6, A8;
then f in ISOM () by Def9;
then reconsider f2 = f as onto isometric Function of (),() by Def4;
x1 in the carrier of () ;
then x1 in dom f2 by FUNCT_2:def 1;
then A9: (f ") . y1 = x1 by ;
f1 " = f3 " by GROUP_2:48
.= f2 " by Th8
.= f " by TOPS_2:def 4 ;
hence [y,x] in SubIsomGroupRel G by ; :: thesis: verum
end;
then SubIsomGroupRel G is_symmetric_in the carrier of () by RELAT_2:def 3;
hence SubIsomGroupRel G is symmetric by ; :: thesis:
now :: thesis: for x, y, z being object st x in the carrier of () & y in the carrier of () & z in the carrier of () & [x,y] in SubIsomGroupRel G & [y,z] in SubIsomGroupRel G holds
[x,z] in SubIsomGroupRel G
let x, y, z be object ; :: thesis: ( x in the carrier of () & y in the carrier of () & z in the carrier of () & [x,y] in SubIsomGroupRel G & [y,z] in SubIsomGroupRel G implies [x,z] in SubIsomGroupRel G )
assume that
A10: ( x in the carrier of () & y in the carrier of () & z in the carrier of () ) and
A11: [x,y] in SubIsomGroupRel G and
A12: [y,z] in SubIsomGroupRel G ; :: thesis:
reconsider x1 = x, y1 = y, z1 = z as Element of () by A10;
consider f being Function such that
A13: f in the carrier of G and
A14: f . x1 = y1 by ;
reconsider f2 = f as Element of G by A13;
A15: the carrier of G c= the carrier of () by GROUP_2:def 5;
then reconsider f3 = f2 as Element of () ;
f in the carrier of () by ;
then A16: f in ISOM () by Def9;
consider g being Function such that
A17: g in the carrier of G and
A18: g . y1 = z1 by ;
reconsider g2 = g as Element of G by A17;
A19: x1 in the carrier of () ;
reconsider g3 = g2 as Element of () by A15;
( f2 in G & g2 in G ) ;
then A20: g3 * f3 in G by GROUP_2:50;
g in the carrier of () by ;
then g in ISOM () by Def9;
then g3 * f3 = g * f by ;
then A21: g * f in the carrier of G by A20;
f is onto isometric Function of (),() by ;
then x1 in dom f by ;
then (g * f) . x1 = z1 by ;
hence [x,z] in SubIsomGroupRel G by ; :: thesis: verum
end;
then SubIsomGroupRel G is_transitive_in the carrier of () by RELAT_2:def 8;
hence SubIsomGroupRel G is transitive by ; :: thesis: verum