let F be Field; for A, B being strict VectSp of F
for f being Function of A,B st f is additive & f is homogeneous & f is one-to-one holds
FuncLatt f is one-to-one
let A, B be strict VectSp of F; for f being Function of A,B st f is additive & f is homogeneous & f is one-to-one holds
FuncLatt f is one-to-one
let f be Function of A,B; ( f is additive & f is homogeneous & f is one-to-one implies FuncLatt f is one-to-one )
assume that
A1:
( f is additive & f is homogeneous )
and
A2:
f is one-to-one
; 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 ;
( x1 in dom (FuncLatt f) & x2 in dom (FuncLatt f) & (FuncLatt f) . x1 = (FuncLatt f) . x2 implies x1 = x2 )
assume that A3:
x1 in dom (FuncLatt f)
and A4:
x2 in dom (FuncLatt f)
and A5:
(FuncLatt f) . x1 = (FuncLatt f) . x2
;
x1 = x2
consider X1 being
strict Subspace of
A such that A6:
X1 = x1
by A3, VECTSP_5:def 3;
A7:
f .: the
carrier of
X1 is
linearly-closed
proof
set BB =
f .: the
carrier of
X1;
A8:
for
v,
u being
Element of
B st
v in f .: the
carrier of
X1 &
u in f .: the
carrier of
X1 holds
v + u in f .: the
carrier of
X1
proof
let v,
u be
Element of
B;
( v in f .: the carrier of X1 & u in f .: the carrier of X1 implies v + u in f .: the carrier of X1 )
assume that A9:
v in f .: the
carrier of
X1
and A10:
u in f .: the
carrier of
X1
;
v + u in f .: the carrier of X1
consider y being
Element of
A such that A11:
y in the
carrier of
X1
and A12:
u = f . y
by A10, FUNCT_2:116;
A13:
y in X1
by A11, STRUCT_0:def 5;
consider x being
Element of
A such that A14:
x in the
carrier of
X1
and A15:
v = f . x
by A9, FUNCT_2:116;
x in X1
by A14, STRUCT_0:def 5;
then
x + y in X1
by A13, VECTSP_4:28;
then
x + y in the
carrier of
X1
by STRUCT_0:def 5;
then
f . (x + y) in f .: the
carrier of
X1
by FUNCT_2:43;
hence
v + u in f .: the
carrier of
X1
by A1, A15, A12, MOD_2:def 3, GRCAT_1:def 13;
verum
end;
for
a being
Element of
F for
v being
Element of
B st
v in f .: the
carrier of
X1 holds
a * v in f .: the
carrier of
X1
hence
f .: the
carrier of
X1 is
linearly-closed
by A8, VECTSP_4:def 1;
verum
end;
consider A1 being
Subset of
B such that A18:
A1 = f .: the
carrier of
X1
;
0. A in X1
by VECTSP_4:25;
then A19:
0. A in the
carrier of
X1
by STRUCT_0:def 5;
A20:
dom f = the
carrier of
A
by FUNCT_2:def 1;
ex
y being
Element of
B st
y = f . (0. A)
;
then
f .: the
carrier of
X1 <> {}
by A20, A19, FUNCT_1:def 12;
then A21:
ex
B1 being
strict Subspace of
B st the
carrier of
B1 = f .: the
carrier of
X1
by A7, VECTSP_4:42;
A22:
(FuncLatt f) . X1 = Lin A1
by A18, Def7;
consider X2 being
strict Subspace of
A such that A23:
X2 = x2
by A4, VECTSP_5:def 3;
A24:
f .: the
carrier of
X2 is
linearly-closed
proof
set BB =
f .: the
carrier of
X2;
A25:
for
v,
u being
Element of
B st
v in f .: the
carrier of
X2 &
u in f .: the
carrier of
X2 holds
v + u in f .: the
carrier of
X2
proof
let v,
u be
Element of
B;
( v in f .: the carrier of X2 & u in f .: the carrier of X2 implies v + u in f .: the carrier of X2 )
assume that A26:
v in f .: the
carrier of
X2
and A27:
u in f .: the
carrier of
X2
;
v + u in f .: the carrier of X2
consider y being
Element of
A such that A28:
y in the
carrier of
X2
and A29:
u = f . y
by A27, FUNCT_2:116;
A30:
y in X2
by A28, STRUCT_0:def 5;
consider x being
Element of
A such that A31:
x in the
carrier of
X2
and A32:
v = f . x
by A26, FUNCT_2:116;
x in X2
by A31, STRUCT_0:def 5;
then
x + y in X2
by A30, VECTSP_4:28;
then
x + y in the
carrier of
X2
by STRUCT_0:def 5;
then
f . (x + y) in f .: the
carrier of
X2
by FUNCT_2:43;
hence
v + u in f .: the
carrier of
X2
by A1, A32, A29, MOD_2:def 3, GRCAT_1:def 13;
verum
end;
for
a being
Element of
F for
v being
Element of
B st
v in f .: the
carrier of
X2 holds
a * v in f .: the
carrier of
X2
hence
f .: the
carrier of
X2 is
linearly-closed
by A25, VECTSP_4:def 1;
verum
end;
consider A2 being
Subset of
B such that A35:
A2 = f .: the
carrier of
X2
;
A36:
(FuncLatt f) . X2 = Lin A2
by A35, Def7;
0. A in X2
by VECTSP_4:25;
then A37:
0. A in the
carrier of
X2
by STRUCT_0:def 5;
ex
y being
Element of
B st
y = f . (0. A)
;
then
f .: the
carrier of
X2 <> {}
by A20, A37, FUNCT_1:def 12;
then consider B2 being
strict Subspace of
B such that A38:
the
carrier of
B2 = f .: the
carrier of
X2
by A24, VECTSP_4:42;
Lin (f .: the carrier of X2) = B2
by A38, VECTSP_7:16;
then A39:
f .: the
carrier of
X1 = f .: the
carrier of
X2
by A5, A6, A23, A18, A35, A22, A36, A21, A38, VECTSP_7:16;
the
carrier of
X2 c= dom f
by A20, VECTSP_4:def 2;
then A40:
the
carrier of
X2 c= the
carrier of
X1
by A2, A39, FUNCT_1:157;
the
carrier of
X1 c= dom f
by A20, VECTSP_4:def 2;
then
the
carrier of
X1 c= the
carrier of
X2
by A2, A39, FUNCT_1:157;
then
the
carrier of
X1 = the
carrier of
X2
by A40, XBOOLE_0:def 10;
hence
x1 = x2
by A6, A23, VECTSP_4:37;
verum
end;
hence
FuncLatt f is one-to-one
by FUNCT_1:def 8; verum