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 holds
FuncLatt f is sup-Semilattice-Homomorphism of (),()

let A, B be strict VectSp of F; :: thesis: for f being Function of A,B st f is additive & f is homogeneous holds
FuncLatt f is sup-Semilattice-Homomorphism of (),()

let f be Function of A,B; :: thesis: ( f is additive & f is homogeneous implies FuncLatt f is sup-Semilattice-Homomorphism of (),() )
assume A1: ( f is additive & f is homogeneous ) ; :: thesis: FuncLatt f is sup-Semilattice-Homomorphism of (),()
FuncLatt f is "\/"-preserving
proof
let a, b be Element of (); :: according to LATTICE4:def 1 :: thesis: () . (a "\/" b) = (() . a) "\/" (() . b)
(FuncLatt f) . (a "\/" b) = (() . a) "\/" (() . b)
proof
reconsider b2 = () . b as Element of () ;
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 ;
0. A in B1 by VECTSP_4:17;
then A4: 0. A in the carrier of B1 by STRUCT_0:def 5;
reconsider a2 = () . a as Element of () ;
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
proof
set BB = f .: the carrier of A1;
A7: for v, u being Element of B st v in f .: the carrier of A1 & u in f .: the carrier of A1 holds
v + u in f .: the carrier of A1
proof
let v, u be Element of B; :: thesis: ( v in f .: the carrier of A1 & u in f .: the carrier of A1 implies v + u in f .: the carrier of A1 )
assume that
A8: v in f .: the carrier of A1 and
A9: u in f .: the carrier of A1 ; :: thesis: v + u in f .: the carrier of A1
consider y being Element of A such that
A10: y in the carrier of A1 and
A11: u = f . y by ;
A12: y in A1 by ;
consider x being Element of A such that
A13: x in the carrier of A1 and
A14: v = f . x by ;
x in A1 by ;
then x + y in A1 by ;
then x + y in the carrier of A1 by STRUCT_0:def 5;
then f . (x + y) in f .: the carrier of A1 by FUNCT_2:35;
hence v + u in f .: the carrier of A1 by ; :: thesis: verum
end;
for a being Element of F
for v being Element of B st v in f .: the carrier of A1 holds
a * v in f .: the carrier of A1
proof
let a be Element of F; :: thesis: for v being Element of B st v in f .: the carrier of A1 holds
a * v in f .: the carrier of A1

let v be Element of B; :: thesis: ( v in f .: the carrier of A1 implies a * v in f .: the carrier of A1 )
assume v in f .: the carrier of A1 ; :: thesis: a * v in f .: the carrier of A1
then consider x being Element of A such that
A15: x in the carrier of A1 and
A16: v = f . x by FUNCT_2:65;
x in A1 by ;
then a * x in A1 by VECTSP_4:21;
then a * x in the carrier of A1 by STRUCT_0:def 5;
then f . (a * x) in f .: the carrier of A1 by FUNCT_2:35;
hence a * v in f .: the carrier of A1 by ; :: thesis: verum
end;
hence f .: the carrier of A1 is linearly-closed by ; :: thesis: verum
end;
A17: f .: the carrier of B1 is linearly-closed
proof
set BB = f .: the carrier of B1;
A18: for v, u being Element of B st v in f .: the carrier of B1 & u in f .: the carrier of B1 holds
v + u in f .: the carrier of B1
proof
let v, u be Element of B; :: thesis: ( v in f .: the carrier of B1 & u in f .: the carrier of B1 implies v + u in f .: the carrier of B1 )
assume that
A19: v in f .: the carrier of B1 and
A20: u in f .: the carrier of B1 ; :: thesis: v + u in f .: the carrier of B1
consider y being Element of A such that
A21: y in the carrier of B1 and
A22: u = f . y by ;
A23: y in B1 by ;
consider x being Element of A such that
A24: x in the carrier of B1 and
A25: v = f . x by ;
x in B1 by ;
then x + y in B1 by ;
then x + y in the carrier of B1 by STRUCT_0:def 5;
then f . (x + y) in f .: the carrier of B1 by FUNCT_2:35;
hence v + u in f .: the carrier of B1 by ; :: thesis: verum
end;
for a being Element of F
for v being Element of B st v in f .: the carrier of B1 holds
a * v in f .: the carrier of B1
proof
let a be Element of F; :: thesis: for v being Element of B st v in f .: the carrier of B1 holds
a * v in f .: the carrier of B1

let v be Element of B; :: thesis: ( v in f .: the carrier of B1 implies a * v in f .: the carrier of B1 )
assume v in f .: the carrier of B1 ; :: thesis: a * v in f .: the carrier of B1
then consider x being Element of A such that
A26: x in the carrier of B1 and
A27: v = f . x by FUNCT_2:65;
x in B1 by ;
then a * x in B1 by VECTSP_4:21;
then a * x in the carrier of B1 by STRUCT_0:def 5;
then f . (a * x) in f .: the carrier of B1 by FUNCT_2:35;
hence a * v in f .: the carrier of B1 by ; :: thesis: verum
end;
hence f .: the carrier of B1 is linearly-closed by ; :: thesis: verum
end;
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 ;
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 ;
then consider B3 being strict Subspace of B such that
A33: the carrier of B3 = f .: the carrier of B1 by ;
A34: Lin (f .: the carrier of B1) = B3 by ;
ex y being Element of B st y = f . (0. A) ;
then A35: f .: the carrier of A1 <> {} by ;
then consider A3 being strict Subspace of B such that
A36: the carrier of A3 = f .: the carrier of A1 by ;
reconsider AB = A3 + B3 as Subspace of B ;
A37: the carrier of AB c= the carrier of P
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of AB or x in the carrier of P )
A38: f .: the carrier of A1 c= f .: the carrier of (A1 + B1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: the carrier of A1 or x in f .: the carrier of (A1 + B1) )
A39: the carrier of A1 c= the carrier of (A1 + B1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of A1 or x in the carrier of (A1 + B1) )
assume A40: x in the carrier of A1 ; :: thesis: x in the carrier of (A1 + B1)
then A41: x in A1 by STRUCT_0:def 5;
the carrier of A1 c= the carrier of A by VECTSP_4:def 2;
then reconsider x = x as Element of A by A40;
x in A1 + B1 by ;
hence x in the carrier of (A1 + B1) by STRUCT_0:def 5; :: thesis: verum
end;
assume A42: x in f .: the carrier of A1 ; :: thesis: x in f .: the carrier of (A1 + B1)
then reconsider x = x as Element of B ;
ex c being Element of A st
( c in the carrier of A1 & x = f . c ) by ;
hence x in f .: the carrier of (A1 + B1) by ; :: thesis: verum
end;
A43: f .: the carrier of B1 c= f .: the carrier of (A1 + B1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: the carrier of B1 or x in f .: the carrier of (A1 + B1) )
A44: the carrier of B1 c= the carrier of (A1 + B1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of B1 or x in the carrier of (A1 + B1) )
assume A45: x in the carrier of B1 ; :: thesis: x in the carrier of (A1 + B1)
then A46: x in B1 by STRUCT_0:def 5;
the carrier of B1 c= the carrier of A by VECTSP_4:def 2;
then reconsider x = x as Element of A by A45;
x in A1 + B1 by ;
hence x in the carrier of (A1 + B1) by STRUCT_0:def 5; :: thesis: verum
end;
assume A47: x in f .: the carrier of B1 ; :: thesis: x in f .: the carrier of (A1 + B1)
then reconsider x = x as Element of B ;
ex c being Element of A st
( c in the carrier of B1 & x = f . c ) by ;
hence x in f .: the carrier of (A1 + B1) by ; :: thesis: verum
end;
assume x in the carrier of AB ; :: thesis: x in the carrier of P
then x in A3 + B3 by STRUCT_0:def 5;
then consider u, v being Element of B such that
A48: u in A3 and
A49: v in B3 and
A50: x = u + v by VECTSP_5:1;
v in f .: the carrier of B1 by ;
then A51: v in P by ;
u in f .: the carrier of A1 by ;
then u in P by ;
then x in P by ;
hence x in the carrier of P by STRUCT_0:def 5; :: thesis: verum
end;
A52: Lin (f .: the carrier of A1) = A3 by ;
A53: f .: the carrier of (A1 + B1) is linearly-closed
proof
set BB = f .: the carrier of (A1 + B1);
A54: for v, u being Element of B st v in f .: the carrier of (A1 + B1) & u in f .: the carrier of (A1 + B1) holds
v + u in f .: the carrier of (A1 + B1)
proof
let v, u be Element of B; :: thesis: ( v in f .: the carrier of (A1 + B1) & u in f .: the carrier of (A1 + B1) implies v + u in f .: the carrier of (A1 + B1) )
assume that
A55: v in f .: the carrier of (A1 + B1) and
A56: u in f .: the carrier of (A1 + B1) ; :: thesis: v + u in f .: the carrier of (A1 + B1)
consider y being Element of A such that
A57: y in the carrier of (A1 + B1) and
A58: u = f . y by ;
A59: y in A1 + B1 by ;
consider x being Element of A such that
A60: x in the carrier of (A1 + B1) and
A61: v = f . x by ;
x in A1 + B1 by ;
then x + y in A1 + B1 by ;
then x + y in the carrier of (A1 + B1) by STRUCT_0:def 5;
then f . (x + y) in f .: the carrier of (A1 + B1) by FUNCT_2:35;
hence v + u in f .: the carrier of (A1 + B1) by ; :: thesis: verum
end;
for a being Element of F
for v being Element of B st v in f .: the carrier of (A1 + B1) holds
a * v in f .: the carrier of (A1 + B1)
proof
let a be Element of F; :: thesis: for v being Element of B st v in f .: the carrier of (A1 + B1) holds
a * v in f .: the carrier of (A1 + B1)

let v be Element of B; :: thesis: ( v in f .: the carrier of (A1 + B1) implies a * v in f .: the carrier of (A1 + B1) )
assume v in f .: the carrier of (A1 + B1) ; :: thesis: a * v in f .: the carrier of (A1 + B1)
then consider x being Element of A such that
A62: x in the carrier of (A1 + B1) and
A63: v = f . x by FUNCT_2:65;
x in A1 + B1 by ;
then a * x in A1 + B1 by VECTSP_4:21;
then a * x in the carrier of (A1 + B1) by STRUCT_0:def 5;
then f . (a * x) in f .: the carrier of (A1 + B1) by FUNCT_2:35;
hence a * v in f .: the carrier of (A1 + B1) by ; :: thesis: verum
end;
hence f .: the carrier of (A1 + B1) is linearly-closed by ; :: thesis: verum
end;
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 ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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 ;
ua in B1 by ;
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 ;
va in A1 by ;
then va in A1 + B1 by VECTSP_5:2;
then ua + va in A1 + B1 by ;
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 ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of P or x in the carrier of AB )
assume x in the carrier of P ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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 ;
c in A1 + B1 by ;
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 ;
then A80: f . v in Lin (f .: the carrier of B1) by ;
u in the carrier of A1 by ;
then A81: f . u in Lin (f .: the carrier of A1) by ;
x = (f . u) + (f . v) by ;
then x in (Lin (f .: the carrier of A1)) + (Lin (f .: the carrier of B1)) by ;
hence x in the carrier of (A3 + B3) by ; :: thesis: verum
end;
then f .: the carrier of (A1 + B1) = the carrier of (A3 + B3) by ;
hence x in the carrier of AB by ; :: thesis: verum
end;
then the carrier of AB = the carrier of P by ;
then A82: P = AB by VECTSP_4:29;
(FuncLatt f) . (a "\/" b) = () . (A1 + B1) by A5, A2, Th7;
hence (FuncLatt f) . (a "\/" b) = (() . a) "\/" (() . b) by A30, A3, A28, A52, A34, A82, Th7; :: thesis: verum
end;
hence (FuncLatt f) . (a "\/" b) = (() . a) "\/" (() . b) ; :: thesis: verum
end;
hence FuncLatt f is sup-Semilattice-Homomorphism of (),() ; :: thesis: verum