let G1, G2 be Group; :: thesis: for f being Homomorphism of G1,G2 st f is one-to-one holds
FuncLatt f is one-to-one
let f be Homomorphism of G1,G2; :: thesis: ( f is one-to-one implies FuncLatt f is one-to-one )
assume A1:
f is one-to-one
; :: thesis: FuncLatt f is one-to-one
for x1, x2 being set st x1 in dom (FuncLatt f) & x2 in dom (FuncLatt f) & (FuncLatt f) . x1 = (FuncLatt f) . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
:: thesis: ( x1 in dom (FuncLatt f) & x2 in dom (FuncLatt f) & (FuncLatt f) . x1 = (FuncLatt f) . x2 implies x1 = x2 )
assume A2:
(
x1 in dom (FuncLatt f) &
x2 in dom (FuncLatt f) &
(FuncLatt f) . x1 = (FuncLatt f) . x2 )
;
:: thesis: x1 = x2
then reconsider x1 =
x1,
x2 =
x2 as
strict Subgroup of
G1 by GROUP_3:def 1;
reconsider A1 =
f .: the
carrier of
x1,
A2 =
f .: the
carrier of
x2 as
Subset of
G2 ;
A4:
(
(FuncLatt f) . x1 = gr A1 &
(FuncLatt f) . x2 = gr A2 )
by Def3;
A5:
dom f = the
carrier of
G1
by FUNCT_2:def 1;
1_ G1 in x1
by GROUP_2:55;
then A6:
1_ G1 in the
carrier of
x1
by STRUCT_0:def 5;
reconsider y =
f . (1_ G1) as
Element of
G2 ;
A7:
y in f .: the
carrier of
x1
by A5, A6, FUNCT_1:def 12;
A8:
for
g being
Element of
G2 st
g in f .: the
carrier of
x1 holds
g " in f .: the
carrier of
x1
for
g1,
g2 being
Element of
G2 st
g1 in f .: the
carrier of
x1 &
g2 in f .: the
carrier of
x1 holds
g1 * g2 in f .: the
carrier of
x1
then consider B1 being
strict Subgroup of
G2 such that A16:
the
carrier of
B1 = f .: the
carrier of
x1
by A7, A8, GROUP_2:61;
1_ G1 in x2
by GROUP_2:55;
then A17:
1_ G1 in the
carrier of
x2
by STRUCT_0:def 5;
consider y being
Element of
G2 such that A18:
y = f . (1_ G1)
;
A19:
f .: the
carrier of
x2 <> {}
by A5, A17, A18, FUNCT_1:def 12;
A20:
for
g being
Element of
G2 st
g in f .: the
carrier of
x2 holds
g " in f .: the
carrier of
x2
for
g1,
g2 being
Element of
G2 st
g1 in f .: the
carrier of
x2 &
g2 in f .: the
carrier of
x2 holds
g1 * g2 in f .: the
carrier of
x2
then consider B2 being
strict Subgroup of
G2 such that A28:
the
carrier of
B2 = f .: the
carrier of
x2
by A19, A20, GROUP_2:61;
gr (f .: the carrier of x2) = B2
by A28, Th3;
then A29:
f .: the
carrier of
x1 = f .: the
carrier of
x2
by A2, A4, A16, A28, Th3;
( the
carrier of
x1 c= dom f & the
carrier of
x2 c= dom f )
by A5, GROUP_2:def 5;
then
( the
carrier of
x1 c= the
carrier of
x2 & the
carrier of
x2 c= the
carrier of
x1 )
by A1, A29, FUNCT_1:157;
then
the
carrier of
x1 = the
carrier of
x2
by XBOOLE_0:def 10;
hence
x1 = x2
by GROUP_2:68;
:: thesis: verum
end;
hence
FuncLatt f is one-to-one
by FUNCT_1:def 8; :: thesis: verum