let F be Field; :: thesis: for A, B being strict VectSp of F
for f being Function of A,B st f is linear holds
FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B
let A, B be strict VectSp of F; :: thesis: for f being Function of A,B st f is linear holds
FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B
let f be Function of A,B; :: thesis: ( f is linear implies FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B )
assume A1:
f is linear
; :: thesis: FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B
FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B
proof
let a,
b be
Element of
(lattice A);
:: according to VECTSP_8:def 9 :: thesis: (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
(FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
proof
consider A1 being
strict Subspace of
A such that A2:
A1 = a
by VECTSP_5:def 3;
consider B1 being
strict Subspace of
A such that A3:
B1 = b
by VECTSP_5:def 3;
A4:
(FuncLatt f) . (a "\/" b) = (FuncLatt f) . (A1 + B1)
by A2, A3, Th7;
reconsider a2 =
(FuncLatt f) . a as
Element of
(lattice B) ;
A5:
a2 = Lin (f .: the carrier of A1)
by A2, Def7;
reconsider b2 =
(FuncLatt f) . b as
Element of
(lattice B) ;
A6:
b2 = Lin (f .: the carrier of B1)
by A3, Def7;
A7:
(FuncLatt f) . (A1 + B1) = Lin (f .: the carrier of (A1 + B1))
by Def7;
A8:
dom f = the
carrier of
A
by FUNCT_2:def 1;
0. A in A1
by VECTSP_4:25;
then A9:
0. A in the
carrier of
A1
by STRUCT_0:def 5;
consider y being
Element of
B such that A10:
y = f . (0. A)
;
A11:
f .: the
carrier of
A1 <> {}
by A8, A9, A10, FUNCT_1:def 12;
A12:
f .: the
carrier of
A1 is
linearly-closed
then consider A3 being
strict Subspace of
B such that A19:
the
carrier of
A3 = f .: the
carrier of
A1
by A11, VECTSP_4:42;
A20:
Lin (f .: the carrier of A1) = A3
by A19, VECTSP_7:16;
0. A in B1
by VECTSP_4:25;
then A21:
0. A in the
carrier of
B1
by STRUCT_0:def 5;
consider y1 being
Element of
B such that A22:
y1 = f . (0. A)
;
A23:
f .: the
carrier of
B1 <> {}
by A8, A21, A22, FUNCT_1:def 12;
A24:
f .: the
carrier of
B1 is
linearly-closed
then consider B3 being
strict Subspace of
B such that A31:
the
carrier of
B3 = f .: the
carrier of
B1
by A23, VECTSP_4:42;
A32:
Lin (f .: the carrier of B1) = B3
by A31, VECTSP_7:16;
A33:
f .: the
carrier of
(A1 + B1) is
linearly-closed
reconsider P =
Lin (f .: the carrier of (A1 + B1)) as
Subspace of
B ;
reconsider AB =
A3 + B3 as
Subspace of
B ;
P = AB
proof
A40:
the
carrier of
P c= the
carrier of
AB
proof
let x be
set ;
:: 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 A41:
x in P
by STRUCT_0:def 5;
f .: the
carrier of
(A1 + B1) = the
carrier of
(A3 + B3)
proof
thus
f .: the
carrier of
(A1 + B1) c= the
carrier of
(A3 + B3)
:: according to XBOOLE_0:def 10 :: thesis: the carrier of (A3 + B3) c= f .: the carrier of (A1 + B1)proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in f .: the carrier of (A1 + B1) or x in the carrier of (A3 + B3) )
assume A42:
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 A43:
(
c in the
carrier of
(A1 + B1) &
x = f . c )
by A42, FUNCT_2:116;
c in A1 + B1
by A43, STRUCT_0:def 5;
then consider u,
v being
Element of
A such that A44:
(
u in A1 &
v in B1 &
c = u + v )
by VECTSP_5:5;
A45:
v in the
carrier of
B1
by A44, STRUCT_0:def 5;
A46:
x = (f . u) + (f . v)
by A1, A43, A44, MOD_2:def 5;
u in the
carrier of
A1
by A44, STRUCT_0:def 5;
then A47:
f . u in Lin (f .: the carrier of A1)
by FUNCT_2:43, VECTSP_7:13;
f . v in Lin (f .: the carrier of B1)
by A45, FUNCT_2:43, VECTSP_7:13;
then
x in (Lin (f .: the carrier of A1)) + (Lin (f .: the carrier of B1))
by A46, A47, VECTSP_5:5;
hence
x in the
carrier of
(A3 + B3)
by A20, A32, STRUCT_0:def 5;
:: thesis: verum
end;
thus
the
carrier of
(A3 + B3) c= f .: the
carrier of
(A1 + B1)
:: thesis: verumproof
let x be
set ;
:: 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 A48:
(
vb in A3 &
ub in B3 &
x = vb + ub )
by VECTSP_5:5;
vb in f .: the
carrier of
A1
by A11, A12, A20, A48, Th10;
then consider va being
Element of
A such that A49:
(
va in the
carrier of
A1 &
vb = f . va )
by FUNCT_2:116;
va in A1
by A49, STRUCT_0:def 5;
then A50:
va in A1 + B1
by VECTSP_5:6;
ub in f .: the
carrier of
B1
by A23, A24, A32, A48, Th10;
then consider ua being
Element of
A such that A51:
(
ua in the
carrier of
B1 &
ub = f . ua )
by FUNCT_2:116;
ua in B1
by A51, STRUCT_0:def 5;
then
ua in A1 + B1
by VECTSP_5:6;
then
ua + va in A1 + B1
by A50, VECTSP_4:28;
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:43;
hence
x in f .: the
carrier of
(A1 + B1)
by A1, A48, A49, A51, MOD_2:def 5;
:: thesis: verum
end;
end;
hence
x in the
carrier of
AB
by A33, A41, Th10;
:: thesis: verum
end;
the
carrier of
AB c= the
carrier of
P
then
the
carrier of
AB = the
carrier of
P
by A40, XBOOLE_0:def 10;
hence
P = AB
by VECTSP_4:37;
:: thesis: verum
end;
hence
(FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
by A4, A5, A6, A7, A20, A32, Th7;
:: thesis: verum
end;
hence
(FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
;
:: thesis: verum
end;
hence
FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B
; :: thesis: verum