let F be Field; :: thesis: for A being strict VectSp of F holds FuncLatt (id the carrier of A) = id the carrier of (lattice A)

let A be strict VectSp of F; :: thesis: FuncLatt (id the carrier of A) = id the carrier of (lattice A)

set f = id the carrier of A;

A1: for x being object st x in the carrier of (lattice A) holds

(FuncLatt (id the carrier of A)) . x = x

hence FuncLatt (id the carrier of A) = id the carrier of (lattice A) by A1, FUNCT_1:17; :: thesis: verum

let A be strict VectSp of F; :: thesis: FuncLatt (id the carrier of A) = id the carrier of (lattice A)

set f = id the carrier of A;

A1: for x being object st x in the carrier of (lattice A) holds

(FuncLatt (id the carrier of A)) . x = x

proof

dom (FuncLatt (id the carrier of A)) = the carrier of (lattice A)
by FUNCT_2:def 1;
let x be object ; :: thesis: ( x in the carrier of (lattice A) implies (FuncLatt (id the carrier of A)) . x = x )

assume x in the carrier of (lattice A) ; :: thesis: (FuncLatt (id the carrier of A)) . x = x

then consider X1 being strict Subspace of A such that

A2: X1 = x by VECTSP_5:def 3;

A3: the carrier of X1 c= (id the carrier of A) .: the carrier of X1

(id the carrier of A) .: the carrier of X1 c= the carrier of X1

hence (FuncLatt (id the carrier of A)) . x = x by A2, A5, VECTSP_7:11; :: thesis: verum

end;assume x in the carrier of (lattice A) ; :: thesis: (FuncLatt (id the carrier of A)) . x = x

then consider X1 being strict Subspace of A such that

A2: X1 = x by VECTSP_5:def 3;

A3: the carrier of X1 c= (id the carrier of A) .: the carrier of X1

proof

A5:
(FuncLatt (id the carrier of A)) . X1 = Lin ((id the carrier of A) .: the carrier of X1)
by Def7;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of X1 or z in (id the carrier of A) .: the carrier of X1 )

assume A4: z in the carrier of X1 ; :: thesis: z in (id the carrier of A) .: the carrier of X1

the carrier of X1 c= the carrier of A by VECTSP_4:def 2;

then reconsider z = z as Element of A by A4;

(id the carrier of A) . z = z ;

hence z in (id the carrier of A) .: the carrier of X1 by A4, FUNCT_2:35; :: thesis: verum

end;assume A4: z in the carrier of X1 ; :: thesis: z in (id the carrier of A) .: the carrier of X1

the carrier of X1 c= the carrier of A by VECTSP_4:def 2;

then reconsider z = z as Element of A by A4;

(id the carrier of A) . z = z ;

hence z in (id the carrier of A) .: the carrier of X1 by A4, FUNCT_2:35; :: thesis: verum

(id the carrier of A) .: the carrier of X1 c= the carrier of X1

proof

then
(id the carrier of A) .: the carrier of X1 = the carrier of X1
by A3, XBOOLE_0:def 10;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (id the carrier of A) .: the carrier of X1 or z in the carrier of X1 )

assume A6: z in (id the carrier of A) .: the carrier of X1 ; :: thesis: z in the carrier of X1

then reconsider z = z as Element of A ;

ex Z being Element of A st

( Z in the carrier of X1 & z = (id the carrier of A) . Z ) by A6, FUNCT_2:65;

hence z in the carrier of X1 ; :: thesis: verum

end;assume A6: z in (id the carrier of A) .: the carrier of X1 ; :: thesis: z in the carrier of X1

then reconsider z = z as Element of A ;

ex Z being Element of A st

( Z in the carrier of X1 & z = (id the carrier of A) . Z ) by A6, FUNCT_2:65;

hence z in the carrier of X1 ; :: thesis: verum

hence (FuncLatt (id the carrier of A)) . x = x by A2, A5, VECTSP_7:11; :: thesis: verum

hence FuncLatt (id the carrier of A) = id the carrier of (lattice A) by A1, FUNCT_1:17; :: thesis: verum