let G be Group; :: thesis: for a being Element of G holds { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G
let a be Element of G; :: thesis: { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G
reconsider X = { ((a -con_map) " {x}) where x is Element of con_class a : verum } as set ;
A1: for y being object st y in union X holds
y in the carrier of G
proof
let x be object ; :: thesis: ( x in union X implies x in the carrier of G )
assume x in union X ; :: thesis: x in the carrier of G
then consider Y being set such that
A2: x in Y and
A3: Y in X by TARSKI:def 4;
ex z being Element of con_class a st (a -con_map) " {z} = Y by A3;
hence x in the carrier of G by A2; :: thesis: verum
end;
for y being object st y in the carrier of G holds
y in union X
proof
let x be object ; :: thesis: ( x in the carrier of G implies x in union X )
assume x in the carrier of G ; :: thesis: x in union X
then reconsider y = x as Element of G ;
consider z being Element of G such that
A4: z in con_class a and
A5: z = a |^ y by GROUP_3:82;
(a -con_map) . y = z by A5, Def2;
then A6: (a -con_map) . y in {z} by TARSKI:def 1;
dom (a -con_map) = the carrier of G by FUNCT_2:def 1;
then A7: y in (a -con_map) " {z} by A6, FUNCT_1:def 7;
(a -con_map) " {z} in X by A4;
hence x in union X by A7, TARSKI:def 4; :: thesis: verum
end;
then A8: union X = the carrier of G by A1, TARSKI:2;
A9: for A being Subset of G st A in X holds
( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) )
proof
let A be Subset of G; :: thesis: ( A in X implies ( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) ) )
assume A in X ; :: thesis: ( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) )
then consider x being Element of con_class a such that
A10: A = (a -con_map) " {x} ;
a,x are_conjugated by GROUP_3:81;
then consider g being Element of G such that
A11: x = a |^ g by GROUP_3:74;
(a -con_map) . g = x by A11, Def2;
then A12: (a -con_map) . g in {x} by TARSKI:def 1;
A13: dom (a -con_map) = the carrier of G by FUNCT_2:def 1;
for B being Subset of G holds
( not B in X or A = B or A misses B )
proof
let B be Subset of G; :: thesis: ( not B in X or A = B or A misses B )
assume B in X ; :: thesis: ( A = B or A misses B )
then ex y being Element of con_class a st B = (a -con_map) " {y} ;
hence ( A = B or A misses B ) by A10, Th10; :: thesis: verum
end;
hence ( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) ) by A10, A12, A13, FUNCT_1:def 7; :: thesis: verum
end;
X c= bool (union X) by ZFMISC_1:82;
hence { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G by A8, A9, EQREL_1:def 4; :: thesis: verum