:: On the Lattice of Subspaces of Vector Space
:: by Andrzej Iwaniuk
::
:: Received May 23, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies VECTSP_1, STRUCT_0, GROUP_4, XXREAL_2, LATTICES, RLSUB_2,
RLSUB_1, XBOOLE_0, SUBSET_1, GROUP_2, FUNCT_1, ZFMISC_1, RELAT_1,
SUPINF_2, SETFAM_1, ARYTM_3, PBOOLE, TARSKI, EQREL_1, REWRITE1, LATTICE3,
RLVECT_3, GROUP_6, VECTSP_8, MSSUBFAM, UNIALG_1, LATTICE4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, LATTICE4, SETFAM_1, RLVECT_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, VECTSP_1,
LATTICES, VECTSP_5, LATTICE3, VECTSP_4, VECTSP_7, GRCAT_1, MOD_2;
constructors SETFAM_1, BINOP_1, REALSET1, VECTSP_5, VECTSP_7, MOD_2, LATTICE3,
LATTICE4, RELSET_1, GRCAT_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES,
VECTSP_2, VECTSP_4, VECTSP_5, RELSET_1, LATTICE4;
requirements BOOLE, SUBSET;
definitions LATTICE3, TARSKI, LATTICE4;
expansions LATTICE3, LATTICE4;
theorems TARSKI, VECTSP_5, LATTICES, LATTICE4, VECTSP_4, SETFAM_1, VECTSP_7,
MOD_2, SUBSET_1, FUNCT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, STRUCT_0,
VECTSP_1;
schemes FUNCT_2, DOMAIN_1;
begin
reserve F for Field;
reserve VS for strict VectSp of F;
definition
let F, VS;
func lattice VS -> strict bounded Lattice equals
LattStr (# Subspaces(VS),
SubJoin(VS), SubMeet(VS) #);
coherence by VECTSP_5:60;
end;
definition
let F,VS;
mode SubVS-Family of VS -> set means
:Def2:
for x be set st x in it holds x is Subspace of VS;
existence
proof
take {};
thus thesis;
end;
end;
registration
let F,VS;
cluster non empty for SubVS-Family of VS;
existence
proof
set A = the Subspace of VS;
for X be set st X in {A} holds X is Subspace of VS by TARSKI:def 1;
then reconsider B = {A} as SubVS-Family of VS by Def2;
take B;
thus thesis;
end;
end;
definition
let F,VS;
redefine func Subspaces(VS) -> non empty SubVS-Family of VS; :: redefines Subspaces (VECTSP_5, definition)
coherence
proof
Subspaces(VS) is SubVS-Family of VS
proof
let x be set;
assume x in Subspaces(VS);
then ex W being strict Subspace of VS st x = W by VECTSP_5:def 3;
hence thesis;
end;
hence thesis;
end;
let X be non empty SubVS-Family of VS;
redefine mode Element of X -> Subspace of VS; :: redefines Element (SUBSET_1, definition)
coherence by Def2;
end;
definition
let F,VS;
let x be Element of Subspaces VS;
func carr(x) -> Subset of VS means
:Def3:
ex X being Subspace of VS st x=X & it = the carrier of X;
existence
proof
reconsider A = the carrier of x as Subset of VS by VECTSP_4:def 2;
consider X being Subspace of VS such that
A1: X=x;
take A,X;
thus thesis by A1;
end;
uniqueness;
end;
reserve u,e for set;
definition
let F,VS;
func carr VS -> Function of Subspaces(VS),bool the carrier of VS means
:Def4
:
for h being Element of Subspaces(VS), H being Subspace of VS st h = H holds
it.h = the carrier of H;
existence
proof
defpred P[object,object] means
for h being Element of Subspaces(VS) st h = $1
holds $2 = the carrier of h;
A1: for e being object st e in Subspaces(VS)
ex u being object st u in bool the carrier of VS & P[e, u]
proof
let e be object;
assume
A2: e in Subspaces(VS);
then consider E being strict Subspace of VS such that
A3: E = e by VECTSP_5:def 3;
reconsider u = E as Element of Subspaces VS by A2,A3;
reconsider u1 = carr u as Subset of VS;
take u1;
ex X being Subspace of VS st u=X & u1 = the carrier of X by Def3;
hence thesis by A3;
end;
consider f being Function of Subspaces(VS),bool the carrier of VS such
that
A4: for e being object st e in Subspaces(VS) holds P[e,f.e]
from FUNCT_2:sch 1(A1);
take f;
thus thesis by A4;
end;
uniqueness
proof
let F1,F2 be Function of Subspaces(VS),bool the carrier of VS such that
A5: for h1 being Element of Subspaces(VS), H1 being Subspace of VS st
h1 = H1 holds F1.h1 = the carrier of H1 and
A6: for h2 being Element of Subspaces(VS), H2 being Subspace of VS st
h2 = H2 holds F2.h2 = the carrier of H2;
for h being object st h in Subspaces(VS) holds F1.h = F2.h
proof
let h be object;
assume
A7: h in Subspaces(VS);
then h is Element of Subspaces(VS);
then consider H being Subspace of VS such that
A8: H=h;
F1.h = the carrier of H by A5,A7,A8;
hence thesis by A6,A7,A8;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th1:
for VS being strict VectSp of F for H being non empty Subset of
Subspaces VS holds (carr VS).:H is non empty
proof
let VS be strict VectSp of F;
let H be non empty Subset of Subspaces VS;
consider x being Element of Subspaces VS such that
A1: x in H by SUBSET_1:4;
(carr VS).x in ((carr VS).:H) by A1,FUNCT_2:35;
hence thesis;
end;
theorem
for VS being strict VectSp of F for H being strict Subspace of VS
holds 0.VS in (carr VS).H
proof
let VS be strict VectSp of F;
let H be strict Subspace of VS;
H in Subspaces VS by VECTSP_5:def 3;
then
A1: (carr VS).H = the carrier of H by Def4;
0.H = 0.VS by VECTSP_4:11;
hence thesis by A1;
end;
reserve x for set;
definition
let F,VS;
let G be non empty Subset of Subspaces(VS);
func meet G -> strict Subspace of VS means
:Def5:
the carrier of it = meet ( (carr VS).:G);
existence
proof
reconsider cG = (carr VS).:G as Subset-Family of VS;
set C0 = meet cG;
A1: for X being set st X in (carr VS).:G holds 0.VS in X
proof
let X be set;
assume
A2: X in (carr VS).:G;
then reconsider X as Subset of VS;
consider X1 being Element of Subspaces VS such that
X1 in G and
A3: X =(carr VS).X1 by A2,FUNCT_2:65;
A4: 0.VS in X1 by VECTSP_4:17;
X = the carrier of X1 by A3,Def4;
hence thesis by A4,STRUCT_0:def 5;
end;
(carr VS).:G <> {} by Th1;
then
A5: C0 <> {} by A1,SETFAM_1:def 1;
reconsider C0 as Subset of VS;
A6: for v,u being Element of VS st v in C0 & u in C0 holds v + u in C0
proof
let v,u be Element of VS such that
A7: v in C0 and
A8: u in C0;
A9: for X being set st X in (carr VS).:G holds v + u in X
proof
reconsider v1 = v, u1 = u as Element of VS;
let X be set;
reconsider vu = v1 + u1 as Element of VS;
assume
A10: X in (carr VS).:G;
then
A11: v in X by A7,SETFAM_1:def 1;
A12: u in X by A8,A10,SETFAM_1:def 1;
reconsider X as Subset of VS by A10;
consider X1 being Element of Subspaces VS such that
X1 in G and
A13: X =(carr VS).X1 by A10,FUNCT_2:65;
A14: X = the carrier of X1 by A13,Def4;
then
A15: u1 in X1 by A12,STRUCT_0:def 5;
consider X2 being strict Subspace of VS such that
A16: X2 = X1 by VECTSP_5:def 3;
v1 in X1 by A11,A14,STRUCT_0:def 5;
then vu in X1 + X1 by A15,VECTSP_5:1;
then vu in X2 by A16,VECTSP_5:4;
hence thesis by A14,A16,STRUCT_0:def 5;
end;
(carr VS).:G <> {} by Th1;
hence thesis by A9,SETFAM_1:def 1;
end;
for a being Element of F, v being Element of VS st v in C0 holds a *
v in C0
proof
let a be Element of F;
let v be Element of VS;
assume
A17: v in C0;
A18: for X being set st X in (carr VS).:G holds a * v in X
proof
reconsider v1 = v as Element of VS;
let X be set;
assume
A19: X in (carr VS).:G;
then
A20: v in X by A17,SETFAM_1:def 1;
reconsider X as Subset of VS by A19;
consider X1 being Element of Subspaces VS such that
X1 in G and
A21: X =(carr VS).X1 by A19,FUNCT_2:65;
A22: X = the carrier of X1 by A21,Def4;
then v1 in X1 by A20,STRUCT_0:def 5;
then a * v1 in X1 by VECTSP_4:21;
hence thesis by A22,STRUCT_0:def 5;
end;
(carr VS).:G <> {} by Th1;
hence thesis by A18,SETFAM_1:def 1;
end;
then C0 is linearly-closed by A6,VECTSP_4:def 1;
hence thesis by A5,VECTSP_4:34;
end;
uniqueness by VECTSP_4:29;
end;
theorem
Subspaces(VS) = the carrier of lattice VS;
theorem
the L_meet of lattice VS = SubMeet(VS);
theorem
the L_join of lattice VS = SubJoin(VS);
theorem Th6:
for VS being strict VectSp of F, p,q being Element of lattice VS,
H1,H2 being strict Subspace of VS st p=H1 & q=H2 holds p [= q iff the carrier
of H1 c= the carrier of H2
proof
let VS be strict VectSp of F;
let p,q be Element of lattice VS;
let H1,H2 be strict Subspace of VS;
consider A1 being strict Subspace of VS such that
A1: A1=p by VECTSP_5:def 3;
consider A2 being strict Subspace of VS such that
A2: A2=q by VECTSP_5:def 3;
A3: the carrier of A1 c= the carrier of A2 implies p [= q
proof
assume the carrier of A1 c= the carrier of A2;
then (the carrier of A1) /\ the carrier of A2 = the carrier of A1 by
XBOOLE_1:28;
then
A4: A1 /\ A2 = A1 by VECTSP_5:def 2;
A1 /\ A2 = (the L_meet of lattice VS).(p,q) by A1,A2,VECTSP_5:def 8
.= p"/\"q by LATTICES:def 2;
hence thesis by A1,A4,LATTICES:4;
end;
p [= q implies the carrier of A1 c= the carrier of A2
proof
assume p [= q;
then
A5: p"/\"q = p by LATTICES:4;
p"/\"q= SubMeet(VS).(p,q) by LATTICES:def 2
.= A1 /\ A2 by A1,A2,VECTSP_5:def 8;
then
(the carrier of A1) /\ the carrier of A2 = the carrier of A1 by A1,A5,
VECTSP_5:def 2;
hence thesis by XBOOLE_1:17;
end;
hence thesis by A1,A2,A3;
end;
theorem Th7:
for VS being strict VectSp of F, p,q being Element of lattice VS,
H1,H2 being Subspace of VS st p=H1 & q=H2 holds p"\/"q = H1+H2
proof
let VS be strict VectSp of F;
let p,q be Element of lattice VS;
let H1,H2 be Subspace of VS;
consider H1 being strict Subspace of VS such that
A1: H1=p by VECTSP_5:def 3;
consider H2 being strict Subspace of VS such that
A2: H2=q by VECTSP_5:def 3;
p"\/"q = SubJoin(VS).(p,q) by LATTICES:def 1
.= H1 + H2 by A1,A2,VECTSP_5:def 7;
hence thesis by A1,A2;
end;
theorem Th8:
for VS being strict VectSp of F, p,q being Element of lattice VS,
H1,H2 being Subspace of VS st p=H1 & q=H2 holds p"/\"q = H1 /\ H2
proof
let VS be strict VectSp of F;
let p,q be Element of lattice VS;
let H1,H2 be Subspace of VS;
consider H1 being strict Subspace of VS such that
A1: H1=p by VECTSP_5:def 3;
consider H2 being strict Subspace of VS such that
A2: H2=q by VECTSP_5:def 3;
p"/\"q = SubMeet(VS).(p,q) by LATTICES:def 2
.= H1 /\ H2 by A1,A2,VECTSP_5:def 8;
hence thesis by A1,A2;
end;
definition
let L be non empty LattStr;
redefine attr L is complete means :: redefines complete (LATTICE3, definition)
for X being Subset of L ex a being Element
of L st a is_less_than X & for b being Element of L st b is_less_than X holds b
[= a;
compatibility
proof
hereby
assume
A1: L is complete;
let X be Subset of L;
set Y = { c where c is Element of L: c is_less_than X };
consider p being Element of L such that
A2: Y is_less_than p and
A3: for r being Element of L st Y is_less_than r holds p [= r by A1;
take p;
thus p is_less_than X
proof
let q be Element of L;
assume
A4: q in X;
Y is_less_than q
proof
let s be Element of L;
assume s in Y;
then ex t being Element of L st s = t & t is_less_than X;
hence thesis by A4;
end;
hence thesis by A3;
end;
let b be Element of L;
assume b is_less_than X;
then b in Y;
hence b [= p by A2;
end;
assume
A5: for X being Subset of L ex a being Element of L st a is_less_than
X & for b being Element of L st b is_less_than X holds b [= a;
let X be set;
defpred P[Element of L] means X is_less_than $1;
set Y = { c where c is Element of L: P[c] };
Y is Subset of L from DOMAIN_1:sch 7;
then consider p being Element of L such that
A6: p is_less_than Y and
A7: for r being Element of L st r is_less_than Y holds r [= p by A5;
take p;
thus X is_less_than p
proof
let q be Element of L;
assume
A8: q in X;
q is_less_than Y
proof
let s be Element of L;
assume s in Y;
then ex t being Element of L st s = t & X is_less_than t;
hence thesis by A8;
end;
hence thesis by A7;
end;
let r be Element of L;
assume X is_less_than r;
then r in Y;
hence thesis by A6;
end;
end;
reserve Z1 for set;
theorem
for VS holds lattice VS is complete
proof
let VS;
let Y be Subset of lattice VS;
per cases;
suppose
A1: Y = {};
thus thesis
proof
take Top lattice VS;
thus Top lattice VS is_less_than Y
by A1;
let b be Element of lattice VS;
assume b is_less_than Y;
thus thesis by LATTICES:19;
end;
end;
suppose
Y <> {};
then reconsider X = Y as non empty Subset of Subspaces(VS);
reconsider p = meet X as Element of lattice VS by VECTSP_5:def 3;
take p;
set x = the Element of X;
thus p is_less_than Y
proof
let q be Element of lattice VS;
consider H being strict Subspace of VS such that
A2: H=q by VECTSP_5:def 3;
reconsider h = q as Element of Subspaces(VS);
assume
A3: q in Y;
(carr VS).h = the carrier of H by A2,Def4;
then meet ((carr VS).:X) c= the carrier of H by A3,FUNCT_2:35,SETFAM_1:3;
then the carrier of meet X c= the carrier of H by Def5;
hence p [= q by A2,Th6;
end;
let r be Element of lattice VS;
consider H being strict Subspace of VS such that
A4: H=r by VECTSP_5:def 3;
assume
A5: r is_less_than Y;
A6: for Z1 st Z1 in (carr VS).:X holds the carrier of H c= Z1
proof
let Z1;
assume
A7: Z1 in (carr VS).:X;
then reconsider Z2=Z1 as Subset of VS;
consider z1 being Element of Subspaces(VS) such that
A8: z1 in X and
A9: Z2=(carr VS).z1 by A7,FUNCT_2:65;
reconsider z1 as Element of lattice VS;
A10: r [= z1 by A5,A8;
consider z3 being strict Subspace of VS such that
A11: z3=z1 by VECTSP_5:def 3;
Z1 = the carrier of z3 by A9,A11,Def4;
hence thesis by A4,A11,A10,Th6;
end;
(carr VS).x in (carr VS).:X by FUNCT_2:35;
then the carrier of H c= meet ((carr VS).:X) by A6,SETFAM_1:5;
then the carrier of H c= the carrier of meet X by Def5;
hence r [= p by A4,Th6;
end;
end;
theorem Th10:
for x being object for VS being strict VectSp of F for S being
Subset of VS st S is non empty & S is linearly-closed holds x in Lin S implies
x in S
proof
let x be object, VS be strict VectSp of F, S be Subset of VS;
assume S is non empty & S is linearly-closed;
then consider W being strict Subspace of VS such that
A1: S = the carrier of W by VECTSP_4:34;
assume
A2: x in Lin S;
Lin S = W by A1,VECTSP_7:11;
hence thesis by A2,A1,STRUCT_0:def 5;
end;
definition
let F be Field;
let A,B be strict VectSp of F;
let f be Function of the carrier of A,the carrier of B;
func FuncLatt f -> Function of the carrier of lattice A, the carrier of
lattice B means
:Def7:
for S being strict Subspace of A, B0 being Subset of B
st B0 = f.:the carrier of S holds it.S = Lin B0;
existence
proof
defpred P[object,object] means
for S being Subspace of A st S = $1 holds $2 =
Lin(f.: the carrier of S);
A1: for x being object st x in the carrier of lattice A
ex y be object st y in the carrier
of lattice B & P[x,y]
proof
let x be object;
assume x in the carrier of lattice A;
then consider X being strict Subspace of A such that
A2: X = x by VECTSP_5:def 3;
reconsider y=f.:the carrier of X as Subset of B;
consider Y being strict Subspace of B such that
A3: Y =Lin(y);
take Y;
thus thesis by A2,A3,VECTSP_5:def 3;
end;
consider f1 being Function of the carrier of lattice A, the carrier of
lattice B such that
A4: for x being object st x in the carrier of lattice A holds P[x,f1.x] from
FUNCT_2:sch 1 (A1);
take f1;
thus thesis
proof
let S be strict Subspace of A;
let B0 be Subset of B;
A5: S is Element of Subspaces A by VECTSP_5:def 3;
assume B0 = f.:the carrier of S;
hence thesis by A4,A5;
end;
end;
uniqueness
proof
let F1,F2 be Function of the carrier of lattice A, the carrier of lattice
B such that
A6: for S being strict Subspace of A, B0 being Subset of B st B0 = f.:
the carrier of S holds F1.S = Lin B0 and
A7: for S being strict Subspace of A, B0 being Subset of B st B0 = f.:
the carrier of S holds F2.S = Lin B0;
for h being object st h in the carrier of lattice A holds F1.h = F2.h
proof
let h be object;
assume h in the carrier of lattice A;
then consider S being strict Subspace of A such that
A8: S = h by VECTSP_5:def 3;
reconsider B0 = f.:(the carrier of S) as Subset of B;
F1.h = Lin B0 by A6,A8;
hence thesis by A7,A8;
end;
hence thesis by FUNCT_2:12;
end;
end;
definition
let L1, L2 be Lattice;
mode Semilattice-Homomorphism of L1,L2
is "/\"-preserving Function of L1,L2;
mode sup-Semilattice-Homomorphism of L1,L2
is "\/"-preserving Function of L1,L2;
end;
theorem
for L1,L2 being Lattice for f being Function of the carrier of L1, the
carrier of L2 holds f is Homomorphism of L1, L2 iff f is
sup-Semilattice-Homomorphism of L1, L2 & f is Semilattice-Homomorphism of L1,
L2;
theorem Th12:
for F being Field for A,B being strict VectSp of F for f be
Function of A, B st f is additive homogeneous holds FuncLatt f is
sup-Semilattice-Homomorphism of lattice A, lattice B
proof
let F be Field;
let A,B be strict VectSp of F;
let f be Function of A,B such that
A1: f is additive homogeneous;
FuncLatt f is "\/"-preserving
proof
let a,b be Element of lattice A;
(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
proof
set BB = f.:the carrier of A1;
A7: for v,u being Element of B st v in BB & u in BB holds v + u in BB
proof
let v,u be Element of B;
assume that
A8: v in BB and
A9: u in BB;
consider y being Element of A such that
A10: y in the carrier of A1 and
A11: u = f.y by A9,FUNCT_2:65;
A12: y in A1 by A10,STRUCT_0:def 5;
consider x being Element of A such that
A13: x in the carrier of A1 and
A14: v = f.x by A8,FUNCT_2:65;
x in A1 by A13,STRUCT_0:def 5;
then x + y in A1 by A12,VECTSP_4:20;
then x + y in the carrier of A1 by STRUCT_0:def 5;
then f.(x + y) in BB by FUNCT_2:35;
hence thesis by A1,A14,A11,VECTSP_1:def 20;
end;
for a being Element of F, v being Element of B st v in BB holds a
* v in BB
proof
let a be Element of F;
let v be Element of B;
assume v in BB;
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 A15,STRUCT_0:def 5;
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 BB by FUNCT_2:35;
hence thesis by A1,A16,MOD_2:def 2;
end;
hence thesis by A7,VECTSP_4:def 1;
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 BB & u in BB holds v + u in BB
proof
let v,u be Element of B;
assume that
A19: v in BB and
A20: u in BB;
consider y being Element of A such that
A21: y in the carrier of B1 and
A22: u = f.y by A20,FUNCT_2:65;
A23: y in B1 by A21,STRUCT_0:def 5;
consider x being Element of A such that
A24: x in the carrier of B1 and
A25: v = f.x by A19,FUNCT_2:65;
x in B1 by A24,STRUCT_0:def 5;
then x + y in B1 by A23,VECTSP_4:20;
then x + y in the carrier of B1 by STRUCT_0:def 5;
then f.(x + y) in BB by FUNCT_2:35;
hence thesis by A1,A25,A22,VECTSP_1:def 20;
end;
for a being Element of F, v being Element of B st v in BB holds a
* v in BB
proof
let a be Element of F;
let v be Element of B;
assume v in BB;
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 A26,STRUCT_0:def 5;
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 BB by FUNCT_2:35;
hence thesis by A1,A27,MOD_2:def 2;
end;
hence thesis by A18,VECTSP_4:def 1;
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 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
proof
let x be object;
A38: f.:the carrier of A1 c= f.:the carrier of (A1+B1)
proof
let x be object;
A39: the carrier of A1 c= the carrier of A1+B1
proof
let x be object;
assume
A40: x in the carrier of A1;
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 as Element of A by A40;
x in A1+B1 by A41,VECTSP_5:2;
hence thesis by STRUCT_0:def 5;
end;
assume
A42: x in f.:the carrier of A1;
then reconsider x as Element of B;
ex c being Element of A st c in the carrier of A1 & x=f.c by A42,
FUNCT_2:65;
hence thesis by A39,FUNCT_2:35;
end;
A43: f.:the carrier of B1 c= f.:the carrier of (A1+B1)
proof
let x be object;
A44: the carrier of B1 c= the carrier of A1+B1
proof
let x be object;
assume
A45: x in the carrier of 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 as Element of A by A45;
x in A1+B1 by A46,VECTSP_5:2;
hence thesis by STRUCT_0:def 5;
end;
assume
A47: x in f.:the carrier of B1;
then reconsider x as Element of B;
ex c being Element of A st c in the carrier of B1 & x=f.c by A47,
FUNCT_2:65;
hence thesis by A44,FUNCT_2:35;
end;
assume x in the carrier of AB;
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 A33,A49,STRUCT_0:def 5;
then
A51: v in P by A43,VECTSP_7:8;
u in f.:the carrier of A1 by A36,A48,STRUCT_0:def 5;
then u in P by A38,VECTSP_7:8;
then x in P by A50,A51,VECTSP_4:20;
hence thesis by STRUCT_0:def 5;
end;
A52: Lin(f.:the carrier of A1) = A3 by A36,VECTSP_7:11;
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 BB & u in BB holds v + u in BB
proof
let v,u be Element of B;
assume that
A55: v in BB and
A56: u in BB;
consider y being Element of A such that
A57: y in the carrier of A1+B1 and
A58: u = f.y by A56,FUNCT_2:65;
A59: y in A1+B1 by A57,STRUCT_0:def 5;
consider x being Element of A such that
A60: x in the carrier of (A1+B1) and
A61: v = f.x by A55,FUNCT_2:65;
x in A1+B1 by A60,STRUCT_0:def 5;
then x + y in A1+B1 by A59,VECTSP_4:20;
then x + y in the carrier of A1+B1 by STRUCT_0:def 5;
then f.(x + y) in BB by FUNCT_2:35;
hence thesis by A1,A61,A58,VECTSP_1:def 20;
end;
for a being Element of F, v being Element of B st v in BB holds a
* v in BB
proof
let a be Element of F;
let v be Element of B;
assume v in BB;
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 A62,STRUCT_0:def 5;
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 BB by FUNCT_2:35;
hence thesis by A1,A63,MOD_2:def 2;
end;
hence thesis by A54,VECTSP_4:def 1;
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;
assume x in the carrier of (A3+B3);
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 thesis by A1,A67,A72,A69,VECTSP_1:def 20;
end;
let x be object;
assume x in the carrier of P;
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;
assume
A74: x in f.:the carrier of (A1+B1);
then reconsider 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 thesis by A52,A34,STRUCT_0:def 5;
end;
then f.:the carrier of (A1+B1) = the carrier of (A3+B3) by A64,
XBOOLE_0:def 10;
hence thesis by A53,A73,Th10;
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 thesis by A30,A3,A28,A52,A34,A82,Th7;
end;
hence thesis;
end;
hence thesis;
end;
theorem
for F being Field for A,B being strict VectSp of F for f be Function
of A,B st f is one-to-one additive homogeneous
holds FuncLatt f is Homomorphism of lattice A,
lattice B
proof
let F be Field, A,B be strict VectSp of F, f be Function of A, B such that
A1: f is one-to-one additive homogeneous;
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;
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
proof
set BB = f.:the carrier of B1;
A12: for v,u being Element of B st v in BB & u in BB holds v + u in BB
proof
let v,u be Element of B;
assume that
A13: v in BB and
A14: u in BB;
consider y being Element of A such that
A15: y in the carrier of B1 and
A16: u = f.y by A14,FUNCT_2:65;
A17: y in B1 by A15,STRUCT_0:def 5;
consider x being Element of A such that
A18: x in the carrier of B1 and
A19: v = f.x by A13,FUNCT_2:65;
x in B1 by A18,STRUCT_0:def 5;
then x + y in B1 by A17,VECTSP_4:20;
then x + y in the carrier of B1 by STRUCT_0:def 5;
then f.(x + y) in BB by FUNCT_2:35;
hence thesis by A1,A19,A16,VECTSP_1:def 20;
end;
for a being Element of F, v being Element of B st v in BB holds a
* v in BB
proof
let a be Element of F;
let v be Element of B;
assume v in BB;
then consider x being Element of A such that
A20: x in the carrier of B1 and
A21: v = f.x by FUNCT_2:65;
x in B1 by A20,STRUCT_0:def 5;
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 BB by FUNCT_2:35;
hence thesis by A1,A21,MOD_2:def 2;
end;
hence thesis by A12,VECTSP_4:def 1;
end;
A22: f.:the carrier of A1 is linearly-closed
proof
set BB = f.:the carrier of A1;
A23: for v,u being Element of B st v in BB & u in BB holds v + u in BB
proof
let v,u be Element of B;
assume that
A24: v in BB and
A25: u in BB;
consider y being Element of A such that
A26: y in the carrier of A1 and
A27: u = f.y by A25,FUNCT_2:65;
A28: y in A1 by A26,STRUCT_0:def 5;
consider x being Element of A such that
A29: x in the carrier of A1 and
A30: v = f.x by A24,FUNCT_2:65;
x in A1 by A29,STRUCT_0:def 5;
then x + y in A1 by A28,VECTSP_4:20;
then x + y in the carrier of A1 by STRUCT_0:def 5;
then f.(x + y) in BB by FUNCT_2:35;
hence thesis by A1,A30,A27,VECTSP_1:def 20;
end;
for a being Element of F, v being Element of B st v in BB holds a
* v in BB
proof
let a be Element of F;
let v be Element of B;
assume v in BB;
then consider x being Element of A such that
A31: x in the carrier of A1 and
A32: v = f.x by FUNCT_2:65;
x in A1 by A31,STRUCT_0:def 5;
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 BB by FUNCT_2:35;
hence thesis by A1,A32,MOD_2:def 2;
end;
hence thesis by A23,VECTSP_4:def 1;
end;
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
proof
set BB = f.:the carrier of A1 /\ B1;
A40: for v,u being Element of B st v in BB & u in BB holds v + u in BB
proof
let v,u be Element of B;
assume that
A41: v in BB and
A42: u in BB;
consider y being Element of A such that
A43: y in the carrier of A1 /\ B1 and
A44: u = f.y by A42,FUNCT_2:65;
A45: y in A1 /\ B1 by A43,STRUCT_0:def 5;
consider x being Element of A such that
A46: x in the carrier of A1 /\ B1 and
A47: v = f.x by A41,FUNCT_2:65;
x in A1 /\ B1 by A46,STRUCT_0:def 5;
then x + y in A1 /\ B1 by A45,VECTSP_4:20;
then x + y in the carrier of A1 /\ B1 by STRUCT_0:def 5;
then f.(x + y) in BB by FUNCT_2:35;
hence thesis by A1,A47,A44,VECTSP_1:def 20;
end;
for a being Element of F, v being Element of B st v in BB holds a
* v in BB
proof
let a be Element of F;
let v be Element of B;
assume v in BB;
then consider x being Element of A such that
A48: x in the carrier of A1 /\ B1 and
A49: v = f.x by FUNCT_2:65;
x in A1 /\ B1 by A48,STRUCT_0:def 5;
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 BB by FUNCT_2:35;
hence thesis by A1,A49,MOD_2:def 2;
end;
hence thesis by A40,VECTSP_4:def 1;
end;
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;
assume x in the carrier of A3 /\ B3;
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 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 thesis by A55,FUNCT_2:35;
end;
let x be object;
assume x in the carrier of P;
then
A60: 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;
assume
A61: x in f.:the carrier of A1 /\ B1;
then reconsider x as Element of B;
consider c being Element of A such that
A62: c in the carrier of A1 /\ B1 and
A63: x = f.c by A61,FUNCT_2:65;
A64: c in A1 /\ B1 by A62,STRUCT_0:def 5;
then c in B1 by VECTSP_5:3;
then c in the carrier of B1 by STRUCT_0:def 5;
then
A65: f.c in Lin(f.:the carrier of B1) by FUNCT_2:35,VECTSP_7:8;
c in A1 by A64,VECTSP_5:3;
then c in the carrier of A1 by STRUCT_0:def 5;
then f.c in Lin(f.:the carrier of A1) by FUNCT_2:35,VECTSP_7:8;
then x in Lin(f.:the carrier of A1) /\ Lin(f.:the carrier of B1) by
A63,A65,VECTSP_5:3;
hence thesis by A38,A35,STRUCT_0:def 5;
end;
then f.:the carrier of A1 /\ B1 = the carrier of A3 /\ B3 by A51,
XBOOLE_0:def 10;
hence thesis by A39,A60,Th10;
end;
the carrier of AB c= the carrier of P
proof
let x be object;
assume x in the carrier of AB;
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 thesis by STRUCT_0:def 5;
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 thesis by A9,A4,A7,A38,A35,A73,Th8;
end;
FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B by A1
,Th12;
hence thesis by A2,LATTICE4:def 1;
end;
then FuncLatt f is "\/"-preserving "/\"-preserving;
hence thesis;
end;
theorem
for A,B being strict VectSp of F for f being Function of A, B st f is
additive homogeneous & f is one-to-one holds FuncLatt f is one-to-one
proof
let A,B be strict VectSp of F;
let f be Function of A, B such that
A1: f is additive homogeneous and
A2: f is one-to-one;
for x1, x2 being object st x1 in dom FuncLatt f & x2 in dom FuncLatt f & (
FuncLatt f).x1 = (FuncLatt f).x2 holds x1 = x2
proof
let x1, x2 be object;
assume that
A3: x1 in dom FuncLatt f and
A4: x2 in dom FuncLatt f and
A5: (FuncLatt f).x1 = (FuncLatt f).x2;
consider X1 being strict Subspace of A such that
A6: X1 = x1 by A3,VECTSP_5:def 3;
A7: f.:the carrier of X1 is linearly-closed
proof
set BB = f.:the carrier of X1;
A8: for v,u being Element of B st v in BB & u in BB holds v + u in BB
proof
let v,u be Element of B;
assume that
A9: v in BB and
A10: u in BB;
consider y being Element of A such that
A11: y in the carrier of X1 and
A12: u = f.y by A10,FUNCT_2:65;
A13: y in X1 by A11,STRUCT_0:def 5;
consider x being Element of A such that
A14: x in the carrier of X1 and
A15: v = f.x by A9,FUNCT_2:65;
x in X1 by A14,STRUCT_0:def 5;
then x + y in X1 by A13,VECTSP_4:20;
then x + y in the carrier of X1 by STRUCT_0:def 5;
then f.(x + y) in BB by FUNCT_2:35;
hence thesis by A1,A15,A12,VECTSP_1:def 20;
end;
for a being Element of F, v being Element of B st v in BB holds a *
v in BB
proof
let a be Element of F;
let v be Element of B;
assume v in BB;
then consider x being Element of A such that
A16: x in the carrier of X1 and
A17: v = f.x by FUNCT_2:65;
x in X1 by A16,STRUCT_0:def 5;
then a * x in X1 by VECTSP_4:21;
then a * x in the carrier of X1 by STRUCT_0:def 5;
then f.(a * x) in BB by FUNCT_2:35;
hence thesis by A1,A17,MOD_2:def 2;
end;
hence thesis by A8,VECTSP_4:def 1;
end;
consider A1 being Subset of B such that
A18: A1 = f.:the carrier of X1;
0.A in X1 by VECTSP_4:17;
then
A19: 0.A in the carrier of X1 by STRUCT_0:def 5;
A20: dom f = the carrier of A by FUNCT_2:def 1;
ex y being Element of B st y = f.(0.A);
then f.:the carrier of X1 <> {} by A20,A19,FUNCT_1:def 6;
then
A21: ex B1 being strict Subspace of B st the carrier of B1 = f .:the
carrier of X1 by A7,VECTSP_4:34;
A22: (FuncLatt f).X1 = Lin A1 by A18,Def7;
consider X2 being strict Subspace of A such that
A23: X2 = x2 by A4,VECTSP_5:def 3;
A24: f.:the carrier of X2 is linearly-closed
proof
set BB = f.:the carrier of X2;
A25: for v,u being Element of B st v in BB & u in BB holds v + u in BB
proof
let v,u be Element of B;
assume that
A26: v in BB and
A27: u in BB;
consider y being Element of A such that
A28: y in the carrier of X2 and
A29: u = f.y by A27,FUNCT_2:65;
A30: y in X2 by A28,STRUCT_0:def 5;
consider x being Element of A such that
A31: x in the carrier of X2 and
A32: v = f.x by A26,FUNCT_2:65;
x in X2 by A31,STRUCT_0:def 5;
then x + y in X2 by A30,VECTSP_4:20;
then x + y in the carrier of X2 by STRUCT_0:def 5;
then f.(x + y) in BB by FUNCT_2:35;
hence thesis by A1,A32,A29,VECTSP_1:def 20;
end;
for a being Element of F, v being Element of B st v in BB holds a *
v in BB
proof
let a be Element of F;
let v be Element of B;
assume v in BB;
then consider x being Element of A such that
A33: x in the carrier of X2 and
A34: v = f.x by FUNCT_2:65;
x in X2 by A33,STRUCT_0:def 5;
then a * x in X2 by VECTSP_4:21;
then a * x in the carrier of X2 by STRUCT_0:def 5;
then f.(a * x) in BB by FUNCT_2:35;
hence thesis by A1,A34,MOD_2:def 2;
end;
hence thesis by A25,VECTSP_4:def 1;
end;
consider A2 being Subset of B such that
A35: A2 = f.:the carrier of X2;
A36: (FuncLatt f).X2 = Lin A2 by A35,Def7;
0.A in X2 by VECTSP_4:17;
then
A37: 0.A in the carrier of X2 by STRUCT_0:def 5;
ex y being Element of B st y = f.(0.A);
then f.:the carrier of X2 <> {} by A20,A37,FUNCT_1:def 6;
then consider B2 being strict Subspace of B such that
A38: the carrier of B2 = f.:the carrier of X2 by A24,VECTSP_4:34;
Lin (f.:the carrier of X2) = B2 by A38,VECTSP_7:11;
then
A39: f.:the carrier of X1 = f.:the carrier of X2 by A5,A6,A23,A18,A35,A22,A36
,A21,A38,VECTSP_7:11;
the carrier of X2 c= dom f by A20,VECTSP_4:def 2;
then
A40: the carrier of X2 c= the carrier of X1 by A2,A39,FUNCT_1:87;
the carrier of X1 c= dom f by A20,VECTSP_4:def 2;
then the carrier of X1 c= the carrier of X2 by A2,A39,FUNCT_1:87;
then the carrier of X1 = the carrier of X2 by A40,XBOOLE_0:def 10;
hence thesis by A6,A23,VECTSP_4:29;
end;
hence thesis by FUNCT_1:def 4;
end;
theorem
for A being strict VectSp of F holds FuncLatt id the carrier of A = id
the carrier of lattice A
proof
let A be strict VectSp of F;
set f = id the carrier of A;
A1: for x being object st x in the carrier of lattice A
holds (FuncLatt f). x = x
proof
let x be object;
assume x in the carrier of lattice A;
then consider X1 being strict Subspace of A such that
A2: X1 = x by VECTSP_5:def 3;
A3: the carrier of X1 c= f.:the carrier of X1
proof
let z be object;
assume
A4: z in the carrier of X1;
the carrier of X1 c= the carrier of A by VECTSP_4:def 2;
then reconsider z as Element of A by A4;
f.z = z;
hence thesis by A4,FUNCT_2:35;
end;
A5: (FuncLatt f).X1 = Lin(f.:the carrier of X1) by Def7;
f.:the carrier of X1 c= the carrier of X1
proof
let z be object;
assume
A6: z in f.:the carrier of X1;
then reconsider z as Element of A;
ex Z being Element of A st Z in the carrier of X1 & z = f.Z by A6,
FUNCT_2:65;
hence thesis;
end;
then f.:the carrier of X1 = the carrier of X1 by A3,XBOOLE_0:def 10;
hence thesis by A2,A5,VECTSP_7:11;
end;
dom FuncLatt f = the carrier of lattice A by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:17;
end;