set X = { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } ;
consider T being strict StableSubgroup of F2() such that
A2: P1[T] by A1;
A3: carr T in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } by A2;
then reconsider Y = meet { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } as Subset of F2() by SETFAM_1:7;
A4: now :: thesis: for a being Element of F2() st a in Y holds
a " in Y
let a be Element of F2(); :: thesis: ( a in Y implies a " in Y )
assume A5: a in Y ; :: thesis: a " in Y
now :: thesis: for Z being set st Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } holds
a " in Z
let Z be set ; :: thesis: ( Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } implies a " in Z )
assume A6: Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } ; :: thesis: a " in Z
then consider A being Subset of F2() such that
A7: A = Z and
A8: ex H being strict StableSubgroup of F2() st
( A = the carrier of H & P1[H] ) ;
consider H being StableSubgroup of F2() such that
A9: A = the carrier of H and
P1[H] by A8;
a in the carrier of H by A5, A6, A7, A9, SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then a " in H by Lm19;
hence a " in Z by A7, A9, STRUCT_0:def 5; :: thesis: verum
end;
hence a " in Y by A3, SETFAM_1:def 1; :: thesis: verum
end;
A10: now :: thesis: for a, b being Element of F2() st a in Y & b in Y holds
a * b in Y
let a, b be Element of F2(); :: thesis: ( a in Y & b in Y implies a * b in Y )
assume that
A11: a in Y and
A12: b in Y ; :: thesis: a * b in Y
now :: thesis: for Z being set st Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } holds
a * b in Z
let Z be set ; :: thesis: ( Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } implies a * b in Z )
assume A13: Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } ; :: thesis: a * b in Z
then consider A being Subset of F2() such that
A14: A = Z and
A15: ex H being strict StableSubgroup of F2() st
( A = the carrier of H & P1[H] ) ;
consider H being StableSubgroup of F2() such that
A16: A = the carrier of H and
P1[H] by A15;
b in the carrier of H by A12, A13, A14, A16, SETFAM_1:def 1;
then A17: b in H by STRUCT_0:def 5;
a in the carrier of H by A11, A13, A14, A16, SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then a * b in H by A17, Lm18;
hence a * b in Z by A14, A16, STRUCT_0:def 5; :: thesis: verum
end;
hence a * b in Y by A3, SETFAM_1:def 1; :: thesis: verum
end;
A18: now :: thesis: for o being Element of F1()
for a being Element of F2() st a in Y holds
(F2() ^ o) . a in Y
let o be Element of F1(); :: thesis: for a being Element of F2() st a in Y holds
(F2() ^ o) . a in Y
let a be Element of F2(); :: thesis: ( a in Y implies (F2() ^ o) . a in Y )
assume A19: a in Y ; :: thesis: (F2() ^ o) . a in Y
now :: thesis: for Z being set st Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } holds
(F2() ^ o) . a in Z
let Z be set ; :: thesis: ( Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } implies (F2() ^ o) . a in Z )
assume A20: Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } ; :: thesis: (F2() ^ o) . a in Z
then consider A being Subset of F2() such that
A21: A = Z and
A22: ex H being strict StableSubgroup of F2() st
( A = the carrier of H & P1[H] ) ;
consider H being StableSubgroup of F2() such that
A23: A = the carrier of H and
P1[H] by A22;
a in the carrier of H by A19, A20, A21, A23, SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then (F2() ^ o) . a in H by Lm9;
hence (F2() ^ o) . a in Z by A21, A23, STRUCT_0:def 5; :: thesis: verum
end;
hence (F2() ^ o) . a in Y by A3, SETFAM_1:def 1; :: thesis: verum
end;
now :: thesis: for Z being set st Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } holds
1_ F2() in Z
let Z be set ; :: thesis: ( Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } implies 1_ F2() in Z )
assume Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } ; :: thesis: 1_ F2() in Z
then consider A being Subset of F2() such that
A24: Z = A and
A25: ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) ;
consider H being StableSubgroup of F2() such that
A26: A = the carrier of H and
P1[H] by A25;
1_ F2() in H by Lm17;
hence 1_ F2() in Z by A24, A26, STRUCT_0:def 5; :: thesis: verum
end;
then Y <> {} by A3, SETFAM_1:def 1;
hence ex H being strict StableSubgroup of F2() st the carrier of H = meet { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } by A10, A4, A18, Lm14; :: thesis: verum