let F be Field; :: thesis: for A, B being strict VectSp of F
for f being Function of A,B st f is linear & f is one-to-one holds
FuncLatt f is one-to-one
let A, B be strict VectSp of F; :: thesis: for f being Function of A,B st f is linear & f is one-to-one holds
FuncLatt f is one-to-one
let f be Function of A,B; :: thesis: ( f is linear & f is one-to-one implies FuncLatt f is one-to-one )
assume A1:
( f is linear & 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 consider X1 being
strict Subspace of
A such that A3:
X1 = x1
by VECTSP_5:def 3;
consider X2 being
strict Subspace of
A such that A4:
X2 = x2
by A2, VECTSP_5:def 3;
consider A1 being
Subset of
B such that A5:
A1 = f .: the
carrier of
X1
;
consider A2 being
Subset of
B such that A6:
A2 = f .: the
carrier of
X2
;
A7:
(
(FuncLatt f) . X1 = Lin A1 &
(FuncLatt f) . X2 = Lin A2 )
by A5, A6, Def7;
A8:
dom f = the
carrier of
A
by FUNCT_2:def 1;
0. A in X1
by VECTSP_4:25;
then A9:
0. A in the
carrier of
X1
by STRUCT_0:def 5;
consider y being
Element of
B such that A10:
y = f . (0. A)
;
A11:
f .: the
carrier of
X1 <> {}
by A8, A9, A10, FUNCT_1:def 12;
f .: the
carrier of
X1 is
linearly-closed
then consider B1 being
strict Subspace of
B such that A18:
the
carrier of
B1 = f .: the
carrier of
X1
by A11, VECTSP_4:42;
0. A in X2
by VECTSP_4:25;
then A19:
0. A in the
carrier of
X2
by STRUCT_0:def 5;
consider y being
Element of
B such that A20:
y = f . (0. A)
;
A21:
f .: the
carrier of
X2 <> {}
by A8, A19, A20, FUNCT_1:def 12;
f .: the
carrier of
X2 is
linearly-closed
then consider B2 being
strict Subspace of
B such that A28:
the
carrier of
B2 = f .: the
carrier of
X2
by A21, VECTSP_4:42;
Lin (f .: the carrier of X2) = B2
by A28, VECTSP_7:16;
then A29:
f .: the
carrier of
X1 = f .: the
carrier of
X2
by A2, A3, A4, A5, A6, A7, A18, A28, VECTSP_7:16;
( the
carrier of
X1 c= dom f & the
carrier of
X2 c= dom f )
by A8, VECTSP_4:def 2;
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 A3, A4, VECTSP_4:37;
:: thesis: verum
end;
hence
FuncLatt f is one-to-one
by FUNCT_1:def 8; :: thesis: verum