let F be Field; :: thesis: for A, B being strict VectSp of F
for f being Function of A,B st f is one-to-one & f is linear holds
FuncLatt f is 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 one-to-one & f is linear holds
FuncLatt f is Homomorphism of lattice A, lattice B
let f be Function of A,B; :: thesis: ( f is one-to-one & f is linear implies FuncLatt f is Homomorphism of lattice A, lattice B )
assume A1:
( f is one-to-one & f is linear )
; :: thesis: 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);
:: thesis: ( (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) & (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) )
A2:
FuncLatt f is
sup-Semilattice-Homomorphism of
lattice A,
lattice B
by A1, Th12;
(FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
proof
consider A1 being
strict Subspace of
A such that A3:
A1 = a
by VECTSP_5:def 3;
consider B1 being
strict Subspace of
A such that A4:
B1 = b
by VECTSP_5:def 3;
A5:
(FuncLatt f) . (a "/\" b) = (FuncLatt f) . (A1 /\ B1)
by A3, A4, Th8;
reconsider a2 =
(FuncLatt f) . a as
Element of
(lattice B) ;
A6:
a2 = Lin (f .: the carrier of A1)
by A3, Def7;
reconsider b2 =
(FuncLatt f) . b as
Element of
(lattice B) ;
A7:
b2 = Lin (f .: the carrier of B1)
by A4, Def7;
A8:
(FuncLatt f) . (A1 /\ B1) = Lin (f .: the carrier of (A1 /\ B1))
by Def7;
A9:
dom f = the
carrier of
A
by FUNCT_2:def 1;
0. A in A1
by VECTSP_4:25;
then A10:
0. A in the
carrier of
A1
by STRUCT_0:def 5;
consider y being
Element of
B such that A11:
y = f . (0. A)
;
A12:
f .: the
carrier of
A1 <> {}
by A9, A10, A11, FUNCT_1:def 12;
A13:
f .: the
carrier of
A1 is
linearly-closed
then consider A3 being
strict Subspace of
B such that A20:
the
carrier of
A3 = f .: the
carrier of
A1
by A12, VECTSP_4:42;
A21:
Lin (f .: the carrier of A1) = A3
by A20, VECTSP_7:16;
0. A in B1
by VECTSP_4:25;
then A22:
0. A in the
carrier of
B1
by STRUCT_0:def 5;
consider y1 being
Element of
B such that A23:
y1 = f . (0. A)
;
A24:
f .: the
carrier of
B1 <> {}
by A9, A22, A23, FUNCT_1:def 12;
A25:
f .: the
carrier of
B1 is
linearly-closed
then consider B3 being
strict Subspace of
B such that A32:
the
carrier of
B3 = f .: the
carrier of
B1
by A24, VECTSP_4:42;
A33:
Lin (f .: the carrier of B1) = B3
by A32, VECTSP_7:16;
A34:
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
A41:
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 A42:
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)
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 A47:
x in A3 /\ B3
by STRUCT_0:def 5;
then
x in Lin (f .: the carrier of A1)
by A21, VECTSP_5:7;
then A48:
x in f .: the
carrier of
A1
by A12, A13, Th10;
then reconsider x =
x as
Element of
B ;
consider xa being
Element of
A such that A49:
(
xa in the
carrier of
A1 &
x = f . xa )
by A48, FUNCT_2:116;
A50:
xa in A1
by A49, STRUCT_0:def 5;
x in Lin (f .: the carrier of B1)
by A33, A47, VECTSP_5:7;
then
x in f .: the
carrier of
B1
by A24, A25, Th10;
then consider xa1 being
Element of
A such that A51:
(
xa1 in the
carrier of
B1 &
x = f . xa1 )
by FUNCT_2:116;
A52:
xa1 in B1
by A51, STRUCT_0:def 5;
xa1 = xa
by A1, A49, A51, FUNCT_2:25;
then
xa in A1 /\ B1
by A50, A52, VECTSP_5:7;
then
xa in the
carrier of
(A1 /\ B1)
by STRUCT_0:def 5;
hence
x in f .: the
carrier of
(A1 /\ B1)
by A49, FUNCT_2:43;
:: thesis: verum
end;
end;
hence
x in the
carrier of
AB
by A34, A42, Th10;
:: thesis: verum
end;
the
carrier of
AB c= the
carrier of
P
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the carrier of AB or x in the carrier of P )
assume
x in the
carrier of
AB
;
:: thesis: x in the carrier of P
then A53:
x in A3 /\ B3
by STRUCT_0:def 5;
then
x in Lin (f .: the carrier of A1)
by A21, VECTSP_5:7;
then
x in f .: the
carrier of
A1
by A20, A21, STRUCT_0:def 5;
then consider xa being
Element of
A such that A54:
(
xa in the
carrier of
A1 &
x = f . xa )
by FUNCT_2:116;
A55:
xa in A1
by A54, STRUCT_0:def 5;
x in Lin (f .: the carrier of B1)
by A33, A53, VECTSP_5:7;
then
x in f .: the
carrier of
B1
by A24, A25, Th10;
then consider xa1 being
Element of
A such that A56:
(
xa1 in the
carrier of
B1 &
x = f . xa1 )
by FUNCT_2:116;
A57:
xa1 in B1
by A56, STRUCT_0:def 5;
xa1 = xa
by A1, A54, A56, FUNCT_2:25;
then
xa in A1 /\ B1
by A55, A57, VECTSP_5:7;
then
xa in the
carrier of
(A1 /\ B1)
by STRUCT_0:def 5;
then
x in P
by A54, FUNCT_2:43, VECTSP_7:13;
hence
x in the
carrier of
P
by STRUCT_0:def 5;
:: thesis: verum
end;
then
the
carrier of
AB = the
carrier of
P
by A41, 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 A5, A6, A7, A8, A21, A33, Th8;
:: thesis: verum
end;
hence
(
(FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) &
(FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) )
by A2, Def9;
:: thesis: verum
end;
hence
FuncLatt f is Homomorphism of lattice A, lattice B
by LATTICE4:def 1; :: thesis: verum