set Id = { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } ;
set I = meet { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } ;
the carrier of L is LeftIdeal of L by Th11;
then A18: the carrier of L in { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } ;
A19: now :: thesis: for X being set st X in { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } holds
F c= X
let X be set ; :: thesis: ( X in { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } implies F c= X )
assume X in { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } ; :: thesis: F c= X
then ex X9 being Subset of L st
( X9 = X & F c= X9 & X9 is LeftIdeal of L ) ;
hence F c= X ; :: thesis: verum
end;
then F c= meet { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } by A18, SETFAM_1:5;
then reconsider I = meet { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } as non empty Subset of L by A1, A18, SETFAM_1:3;
A20: I is add-closed
proof
let x, y be Element of L; :: according to IDEAL_1:def 1 :: thesis: ( x in I & y in I implies x + y in I )
assume A21: ( x in I & y in I ) ; :: thesis: x + y in I
now :: thesis: for X being set st X in { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } holds
{(x + y)} c= X
let X be set ; :: thesis: ( X in { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } implies {(x + y)} c= X )
assume A22: X in { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } ; :: thesis: {(x + y)} c= X
then consider X9 being Subset of L such that
A23: X9 = X and
F c= X9 and
A24: X9 is LeftIdeal of L ;
( x in X & y in X ) by A21, A22, SETFAM_1:def 1;
then x + y in X9 by A23, A24, Def1;
hence {(x + y)} c= X by A23, ZFMISC_1:31; :: thesis: verum
end;
then {(x + y)} c= I by A18, SETFAM_1:5;
hence x + y in I by ZFMISC_1:31; :: thesis: verum
end;
I is left-ideal
proof
let p, x be Element of L; :: according to IDEAL_1:def 2 :: thesis: ( x in I implies p * x in I )
assume A25: x in I ; :: thesis: p * x in I
now :: thesis: for X being set st X in { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } holds
{(p * x)} c= X
let X be set ; :: thesis: ( X in { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } implies {(p * x)} c= X )
assume A26: X in { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } ; :: thesis: {(p * x)} c= X
then consider X9 being Subset of L such that
A27: X9 = X and
F c= X9 and
A28: X9 is LeftIdeal of L ;
x in X by A25, A26, SETFAM_1:def 1;
then p * x in X9 by A27, A28, Def2;
hence {(p * x)} c= X by A27, ZFMISC_1:31; :: thesis: verum
end;
then {(p * x)} c= I by A18, SETFAM_1:5;
hence p * x in I by ZFMISC_1:31; :: thesis: verum
end;
then reconsider I = I as LeftIdeal of L by A20;
take I ; :: thesis: ( F c= I & ( for I being LeftIdeal of L st F c= I holds
I c= I ) )
now :: thesis: for X being LeftIdeal of L st F c= X holds
I c= X
let X be LeftIdeal of L; :: thesis: ( F c= X implies I c= X )
assume F c= X ; :: thesis: I c= X
then X in { I where I is Subset of L : ( F c= I & I is LeftIdeal of L ) } ;
hence I c= X by SETFAM_1:3; :: thesis: verum
end;
hence ( F c= I & ( for I being LeftIdeal of L st F c= I holds
I c= I ) ) by A18, A19, SETFAM_1:5; :: thesis: verum