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 holds
FuncLatt f is sup-Semilattice-Homomorphism of (lattice A),(lattice B)
let A, B be strict VectSp of F; for f being Function of A,B st f is additive & f is homogeneous holds
FuncLatt f is sup-Semilattice-Homomorphism of (lattice A),(lattice B)
let f be Function of A,B; ( f is additive & f is homogeneous implies FuncLatt f is sup-Semilattice-Homomorphism of (lattice A),(lattice B) )
assume A1:
( f is additive & f is homogeneous )
; FuncLatt f is sup-Semilattice-Homomorphism of (lattice A),(lattice B)
FuncLatt f is "\/"-preserving
proof
let a,
b be
Element of
(lattice A);
LATTICE4:def 1 (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
(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 A2:
B1 = b
by VECTSP_5:def 3;
A3:
b2 = Lin (f .: the carrier of B1)
by A2, Def7;
0. A in B1
by VECTSP_4:17;
then A4:
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 A5:
A1 = a
by VECTSP_5:def 3;
A6:
f .: the
carrier of
A1 is
linearly-closed
A17:
f .: the
carrier of
B1 is
linearly-closed
reconsider P =
Lin (f .: the carrier of (A1 + B1)) as
Subspace of
B ;
A28:
(FuncLatt f) . (A1 + B1) = Lin (f .: the carrier of (A1 + B1))
by Def7;
0. A in A1
by VECTSP_4:17;
then A29:
0. A in the
carrier of
A1
by STRUCT_0:def 5;
A30:
a2 = Lin (f .: the carrier of A1)
by A5, Def7;
A31:
dom f = the
carrier of
A
by FUNCT_2:def 1;
ex
y1 being
Element of
B st
y1 = f . (0. A)
;
then A32:
f .: the
carrier of
B1 <> {}
by A31, A4, FUNCT_1:def 6;
then consider B3 being
strict Subspace of
B such that A33:
the
carrier of
B3 = f .: the
carrier of
B1
by A17, VECTSP_4:34;
A34:
Lin (f .: the carrier of B1) = B3
by A33, VECTSP_7:11;
ex
y being
Element of
B st
y = f . (0. A)
;
then A35:
f .: the
carrier of
A1 <> {}
by A31, A29, FUNCT_1:def 6;
then consider A3 being
strict Subspace of
B such that A36:
the
carrier of
A3 = f .: the
carrier of
A1
by A6, VECTSP_4:34;
reconsider AB =
A3 + B3 as
Subspace of
B ;
A37:
the
carrier of
AB c= the
carrier of
P
A52:
Lin (f .: the carrier of A1) = A3
by A36, VECTSP_7:11;
A53:
f .: the
carrier of
(A1 + B1) is
linearly-closed
the
carrier of
P c= the
carrier of
AB
proof
A64:
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
x in A3 + B3
by STRUCT_0:def 5;
then consider vb,
ub being
Element of
B such that A65:
vb in A3
and A66:
ub in B3
and A67:
x = vb + ub
by VECTSP_5:1;
consider ua being
Element of
A such that A68:
ua in the
carrier of
B1
and A69:
ub = f . ua
by A32, A17, A34, A66, Th10, FUNCT_2:65;
ua in B1
by A68, STRUCT_0:def 5;
then A70:
ua in A1 + B1
by VECTSP_5:2;
consider va being
Element of
A such that A71:
va in the
carrier of
A1
and A72:
vb = f . va
by A35, A6, A52, A65, Th10, FUNCT_2:65;
va in A1
by A71, STRUCT_0:def 5;
then
va in A1 + B1
by VECTSP_5:2;
then
ua + va in A1 + B1
by A70, VECTSP_4:20;
then
ua + va in the
carrier of
(A1 + B1)
by STRUCT_0:def 5;
then
f . (ua + va) in f .: the
carrier of
(A1 + B1)
by FUNCT_2:35;
hence
x in f .: the
carrier of
(A1 + B1)
by A1, A67, A72, A69, VECTSP_1:def 20;
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 A73:
x in P
by STRUCT_0:def 5;
f .: the
carrier of
(A1 + B1) c= the
carrier of
(A3 + B3)
proof
let x be
object ;
TARSKI:def 3 ( not x in f .: the carrier of (A1 + B1) or x in the carrier of (A3 + B3) )
assume A74:
x in f .: the
carrier of
(A1 + B1)
;
x in the carrier of (A3 + B3)
then reconsider x =
x as
Element of
B ;
consider c being
Element of
A such that A75:
c in the
carrier of
(A1 + B1)
and A76:
x = f . c
by A74, FUNCT_2:65;
c in A1 + B1
by A75, STRUCT_0:def 5;
then consider u,
v being
Element of
A such that A77:
u in A1
and A78:
v in B1
and A79:
c = u + v
by VECTSP_5:1;
v in the
carrier of
B1
by A78, STRUCT_0:def 5;
then A80:
f . v in Lin (f .: the carrier of B1)
by FUNCT_2:35, VECTSP_7:8;
u in the
carrier of
A1
by A77, STRUCT_0:def 5;
then A81:
f . u in Lin (f .: the carrier of A1)
by FUNCT_2:35, VECTSP_7:8;
x = (f . u) + (f . v)
by A1, A76, A79, VECTSP_1:def 20;
then
x in (Lin (f .: the carrier of A1)) + (Lin (f .: the carrier of B1))
by A81, A80, VECTSP_5:1;
hence
x in the
carrier of
(A3 + B3)
by A52, A34, STRUCT_0:def 5;
verum
end;
then
f .: the
carrier of
(A1 + B1) = the
carrier of
(A3 + B3)
by A64, XBOOLE_0:def 10;
hence
x in the
carrier of
AB
by A53, A73, Th10;
verum
end;
then
the
carrier of
AB = the
carrier of
P
by A37, XBOOLE_0:def 10;
then A82:
P = AB
by VECTSP_4:29;
(FuncLatt f) . (a "\/" b) = (FuncLatt f) . (A1 + B1)
by A5, A2, Th7;
hence
(FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
by A30, A3, A28, A52, A34, A82, Th7;
verum
end;
hence
(FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
;
verum
end;
hence
FuncLatt f is sup-Semilattice-Homomorphism of (lattice A),(lattice B)
; verum