let F be Field; for A, B being strict VectSp of F
for f being Function of A,B st f is one-to-one & f is additive & f is homogeneous holds
FuncLatt f is Homomorphism of (lattice A),(lattice B)
let A, B be strict VectSp of F; for f being Function of A,B st f is one-to-one & f is additive & f is homogeneous holds
FuncLatt f is Homomorphism of (lattice A),(lattice B)
let f be Function of A,B; ( f is one-to-one & f is additive & f is homogeneous implies FuncLatt f is Homomorphism of (lattice A),(lattice B) )
assume A1:
( f is one-to-one & f is additive & f is homogeneous )
; FuncLatt f is Homomorphism of (lattice A),(lattice B)
for a, b being Element of (lattice A) holds
( (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) & (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) )
proof
let a,
b be
Element of
(lattice A);
( (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) & (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) )
A2:
(FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
proof
reconsider b2 =
(FuncLatt f) . b as
Element of
(lattice B) ;
consider B1 being
strict Subspace of
A such that A3:
B1 = b
by VECTSP_5:def 3;
A4:
b2 = Lin (f .: the carrier of B1)
by A3, Def7;
0. A in B1
by VECTSP_4:17;
then A5:
0. A in the
carrier of
B1
by STRUCT_0:def 5;
reconsider a2 =
(FuncLatt f) . a as
Element of
(lattice B) ;
consider A1 being
strict Subspace of
A such that A6:
A1 = a
by VECTSP_5:def 3;
reconsider P =
Lin (f .: the carrier of (A1 /\ B1)) as
Subspace of
B ;
A7:
(FuncLatt f) . (A1 /\ B1) = Lin (f .: the carrier of (A1 /\ B1))
by Def7;
0. A in A1
by VECTSP_4:17;
then A8:
0. A in the
carrier of
A1
by STRUCT_0:def 5;
A9:
a2 = Lin (f .: the carrier of A1)
by A6, Def7;
A10:
dom f = the
carrier of
A
by FUNCT_2:def 1;
A11:
f .: the
carrier of
B1 is
linearly-closed
A22:
f .: the
carrier of
A1 is
linearly-closed
ex
y1 being
Element of
B st
y1 = f . (0. A)
;
then A33:
f .: the
carrier of
B1 <> {}
by A10, A5, FUNCT_1:def 6;
then consider B3 being
strict Subspace of
B such that A34:
the
carrier of
B3 = f .: the
carrier of
B1
by A11, VECTSP_4:34;
A35:
Lin (f .: the carrier of B1) = B3
by A34, VECTSP_7:11;
ex
y being
Element of
B st
y = f . (0. A)
;
then A36:
f .: the
carrier of
A1 <> {}
by A10, A8, FUNCT_1:def 6;
then consider A3 being
strict Subspace of
B such that A37:
the
carrier of
A3 = f .: the
carrier of
A1
by A22, VECTSP_4:34;
reconsider AB =
A3 /\ B3 as
Subspace of
B ;
A38:
Lin (f .: the carrier of A1) = A3
by A37, VECTSP_7:11;
A39:
f .: the
carrier of
(A1 /\ B1) is
linearly-closed
A50:
the
carrier of
P c= the
carrier of
AB
proof
A51:
the
carrier of
(A3 /\ B3) c= f .: the
carrier of
(A1 /\ B1)
proof
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (A3 /\ B3) or x in f .: the carrier of (A1 /\ B1) )
assume
x in the
carrier of
(A3 /\ B3)
;
x in f .: the carrier of (A1 /\ B1)
then A52:
x in A3 /\ B3
by STRUCT_0:def 5;
then A53:
x in Lin (f .: the carrier of A1)
by A38, VECTSP_5:3;
then
x in f .: the
carrier of
A1
by A36, A22, Th10;
then reconsider x =
x as
Element of
B ;
consider xa being
Element of
A such that A54:
xa in the
carrier of
A1
and A55:
x = f . xa
by A36, A22, A53, Th10, FUNCT_2:65;
A56:
xa in A1
by A54, STRUCT_0:def 5;
x in Lin (f .: the carrier of B1)
by A35, A52, VECTSP_5:3;
then consider xa1 being
Element of
A such that A57:
xa1 in the
carrier of
B1
and A58:
x = f . xa1
by A33, A11, Th10, FUNCT_2:65;
A59:
xa1 in B1
by A57, STRUCT_0:def 5;
xa1 = xa
by A1, A55, A58, FUNCT_2:19;
then
xa in A1 /\ B1
by A56, A59, VECTSP_5:3;
then
xa in the
carrier of
(A1 /\ B1)
by STRUCT_0:def 5;
hence
x in f .: the
carrier of
(A1 /\ B1)
by A55, FUNCT_2:35;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in the carrier of P or x in the carrier of AB )
assume
x in the
carrier of
P
;
x in the carrier of AB
then A60:
x in P
by STRUCT_0:def 5;
f .: the
carrier of
(A1 /\ B1) c= the
carrier of
(A3 /\ B3)
then
f .: the
carrier of
(A1 /\ B1) = the
carrier of
(A3 /\ B3)
by A51, XBOOLE_0:def 10;
hence
x in the
carrier of
AB
by A39, A60, Th10;
verum
end;
the
carrier of
AB c= the
carrier of
P
proof
let x be
object ;
TARSKI:def 3 ( not x in the carrier of AB or x in the carrier of P )
assume
x in the
carrier of
AB
;
x in the carrier of P
then A66:
x in A3 /\ B3
by STRUCT_0:def 5;
then
x in Lin (f .: the carrier of B1)
by A35, VECTSP_5:3;
then consider xa1 being
Element of
A such that A67:
xa1 in the
carrier of
B1
and A68:
x = f . xa1
by A33, A11, Th10, FUNCT_2:65;
A69:
xa1 in B1
by A67, STRUCT_0:def 5;
x in Lin (f .: the carrier of A1)
by A38, A66, VECTSP_5:3;
then
x in f .: the
carrier of
A1
by A37, A38, STRUCT_0:def 5;
then consider xa being
Element of
A such that A70:
xa in the
carrier of
A1
and A71:
x = f . xa
by FUNCT_2:65;
A72:
xa in A1
by A70, STRUCT_0:def 5;
xa1 = xa
by A1, A71, A68, FUNCT_2:19;
then
xa in A1 /\ B1
by A72, A69, VECTSP_5:3;
then
xa in the
carrier of
(A1 /\ B1)
by STRUCT_0:def 5;
then
x in P
by A71, FUNCT_2:35, VECTSP_7:8;
hence
x in the
carrier of
P
by STRUCT_0:def 5;
verum
end;
then
the
carrier of
AB = the
carrier of
P
by A50, XBOOLE_0:def 10;
then A73:
P = AB
by VECTSP_4:29;
(FuncLatt f) . (a "/\" b) = (FuncLatt f) . (A1 /\ B1)
by A6, A3, Th8;
hence
(FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
by A9, A4, A7, A38, A35, A73, Th8;
verum
end;
FuncLatt f is
sup-Semilattice-Homomorphism of
(lattice A),
(lattice B)
by A1, Th12;
hence
(
(FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) &
(FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) )
by A2, LATTICE4:def 1;
verum
end;
then
( FuncLatt f is "\/"-preserving & FuncLatt f is "/\"-preserving )
;
hence
FuncLatt f is Homomorphism of (lattice A),(lattice B)
; verum