let F be Field; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: FuncLatt f is one-to-one

for x1, x2 being object st x1 in dom (FuncLatt f) & x2 in dom (FuncLatt f) & (FuncLatt f) . x1 = (FuncLatt f) . x2 holds

x1 = x2

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: FuncLatt f is one-to-one

for x1, x2 being object st x1 in dom (FuncLatt f) & x2 in dom (FuncLatt f) & (FuncLatt f) . x1 = (FuncLatt f) . x2 holds

x1 = x2

proof

hence
FuncLatt f is one-to-one
by FUNCT_1:def 4; :: thesis: verum
let x1, x2 be object ; :: thesis: ( 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 ; :: thesis: 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

A18: A1 = f .: the carrier of X1 ;

0. A in X1 by VECTSP_4:17;

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 6;

then A21: ex B1 being strict Subspace of B st the carrier of B1 = f .: the carrier of X1 by A7, VECTSP_4:34;

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

A35: A2 = f .: the carrier of X2 ;

A36: (FuncLatt f) . X2 = Lin A2 by A35, Def7;

0. A in X2 by VECTSP_4:17;

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 6;

then consider B2 being strict Subspace of B such that

A38: the carrier of B2 = f .: the carrier of X2 by A24, VECTSP_4:34;

Lin (f .: the carrier of X2) = B2 by A38, VECTSP_7:11;

then A39: f .: the carrier of X1 = f .: the carrier of X2 by A5, A6, A23, A18, A35, A22, A36, A21, A38, VECTSP_7:11;

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:87;

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:87;

then the carrier of X1 = the carrier of X2 by A40, XBOOLE_0:def 10;

hence x1 = x2 by A6, A23, VECTSP_4:29; :: thesis: verum

end;assume that

A3: x1 in dom (FuncLatt f) and

A4: x2 in dom (FuncLatt f) and

A5: (FuncLatt f) . x1 = (FuncLatt f) . x2 ; :: thesis: 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

consider A1 being Subset of B such that
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

for v being Element of B st v in f .: the carrier of X1 holds

a * v in f .: the carrier of X1

end;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

for a being Element of F
let v, u be Element of B; :: thesis: ( 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 ; :: thesis: 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:65;

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:65;

x in X1 by A14, STRUCT_0:def 5;

then x + y in X1 by A13, VECTSP_4:20;

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:35;

hence v + u in f .: the carrier of X1 by A1, A15, A12, VECTSP_1:def 20; :: thesis: verum

end;assume that

A9: v in f .: the carrier of X1 and

A10: u in f .: the carrier of X1 ; :: thesis: 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:65;

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:65;

x in X1 by A14, STRUCT_0:def 5;

then x + y in X1 by A13, VECTSP_4:20;

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:35;

hence v + u in f .: the carrier of X1 by A1, A15, A12, VECTSP_1:def 20; :: thesis: verum

for v being Element of B st v in f .: the carrier of X1 holds

a * v in f .: the carrier of X1

proof

hence
f .: the carrier of X1 is linearly-closed
by A8, VECTSP_4:def 1; :: thesis: verum
let a be Element of F; :: thesis: for v being Element of B st v in f .: the carrier of X1 holds

a * v in f .: the carrier of X1

let v be Element of B; :: thesis: ( v in f .: the carrier of X1 implies a * v in f .: the carrier of X1 )

assume v in f .: the carrier of X1 ; :: thesis: a * v in f .: the carrier of X1

then consider x being Element of A such that

A16: x in the carrier of X1 and

A17: v = f . x by FUNCT_2:65;

x in X1 by A16, STRUCT_0:def 5;

then a * x in X1 by VECTSP_4:21;

then a * x in the carrier of X1 by STRUCT_0:def 5;

then f . (a * x) in f .: the carrier of X1 by FUNCT_2:35;

hence a * v in f .: the carrier of X1 by A1, A17, MOD_2:def 2; :: thesis: verum

end;a * v in f .: the carrier of X1

let v be Element of B; :: thesis: ( v in f .: the carrier of X1 implies a * v in f .: the carrier of X1 )

assume v in f .: the carrier of X1 ; :: thesis: a * v in f .: the carrier of X1

then consider x being Element of A such that

A16: x in the carrier of X1 and

A17: v = f . x by FUNCT_2:65;

x in X1 by A16, STRUCT_0:def 5;

then a * x in X1 by VECTSP_4:21;

then a * x in the carrier of X1 by STRUCT_0:def 5;

then f . (a * x) in f .: the carrier of X1 by FUNCT_2:35;

hence a * v in f .: the carrier of X1 by A1, A17, MOD_2:def 2; :: thesis: verum

A18: A1 = f .: the carrier of X1 ;

0. A in X1 by VECTSP_4:17;

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 6;

then A21: ex B1 being strict Subspace of B st the carrier of B1 = f .: the carrier of X1 by A7, VECTSP_4:34;

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

consider A2 being Subset of B such that
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

for v being Element of B st v in f .: the carrier of X2 holds

a * v in f .: the carrier of X2

end;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

for a being Element of F
let v, u be Element of B; :: thesis: ( 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 ; :: thesis: 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:65;

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:65;

x in X2 by A31, STRUCT_0:def 5;

then x + y in X2 by A30, VECTSP_4:20;

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:35;

hence v + u in f .: the carrier of X2 by A1, A32, A29, VECTSP_1:def 20; :: thesis: verum

end;assume that

A26: v in f .: the carrier of X2 and

A27: u in f .: the carrier of X2 ; :: thesis: 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:65;

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:65;

x in X2 by A31, STRUCT_0:def 5;

then x + y in X2 by A30, VECTSP_4:20;

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:35;

hence v + u in f .: the carrier of X2 by A1, A32, A29, VECTSP_1:def 20; :: thesis: verum

for v being Element of B st v in f .: the carrier of X2 holds

a * v in f .: the carrier of X2

proof

hence
f .: the carrier of X2 is linearly-closed
by A25, VECTSP_4:def 1; :: thesis: verum
let a be Element of F; :: thesis: for v being Element of B st v in f .: the carrier of X2 holds

a * v in f .: the carrier of X2

let v be Element of B; :: thesis: ( v in f .: the carrier of X2 implies a * v in f .: the carrier of X2 )

assume v in f .: the carrier of X2 ; :: thesis: a * v in f .: the carrier of X2

then consider x being Element of A such that

A33: x in the carrier of X2 and

A34: v = f . x by FUNCT_2:65;

x in X2 by A33, STRUCT_0:def 5;

then a * x in X2 by VECTSP_4:21;

then a * x in the carrier of X2 by STRUCT_0:def 5;

then f . (a * x) in f .: the carrier of X2 by FUNCT_2:35;

hence a * v in f .: the carrier of X2 by A1, A34, MOD_2:def 2; :: thesis: verum

end;a * v in f .: the carrier of X2

let v be Element of B; :: thesis: ( v in f .: the carrier of X2 implies a * v in f .: the carrier of X2 )

assume v in f .: the carrier of X2 ; :: thesis: a * v in f .: the carrier of X2

then consider x being Element of A such that

A33: x in the carrier of X2 and

A34: v = f . x by FUNCT_2:65;

x in X2 by A33, STRUCT_0:def 5;

then a * x in X2 by VECTSP_4:21;

then a * x in the carrier of X2 by STRUCT_0:def 5;

then f . (a * x) in f .: the carrier of X2 by FUNCT_2:35;

hence a * v in f .: the carrier of X2 by A1, A34, MOD_2:def 2; :: thesis: verum

A35: A2 = f .: the carrier of X2 ;

A36: (FuncLatt f) . X2 = Lin A2 by A35, Def7;

0. A in X2 by VECTSP_4:17;

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 6;

then consider B2 being strict Subspace of B such that

A38: the carrier of B2 = f .: the carrier of X2 by A24, VECTSP_4:34;

Lin (f .: the carrier of X2) = B2 by A38, VECTSP_7:11;

then A39: f .: the carrier of X1 = f .: the carrier of X2 by A5, A6, A23, A18, A35, A22, A36, A21, A38, VECTSP_7:11;

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:87;

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:87;

then the carrier of X1 = the carrier of X2 by A40, XBOOLE_0:def 10;

hence x1 = x2 by A6, A23, VECTSP_4:29; :: thesis: verum