let G be Group; :: thesis: for A, B being non empty Subset of G
for N being normal Subgroup of G holds (N ~ A) * (N ~ B) = N ~ (A * B)
let A, B be non empty Subset of G; :: thesis: for N being normal Subgroup of G holds (N ~ A) * (N ~ B) = N ~ (A * B)
let N be normal Subgroup of G; :: thesis: (N ~ A) * (N ~ B) = N ~ (A * B)
thus (N ~ A) * (N ~ B) c= N ~ (A * B) :: according to XBOOLE_0:def 10 :: thesis: N ~ (A * B) c= (N ~ A) * (N ~ B)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (N ~ A) * (N ~ B) or x in N ~ (A * B) )
assume A1: x in (N ~ A) * (N ~ B) ; :: thesis: x in N ~ (A * B)
then reconsider x = x as Element of G ;
consider x1, x2 being Element of G such that
A2: ( x = x1 * x2 & x1 in N ~ A & x2 in N ~ B ) by A1;
A3: x1 * N meets A by A2, Th14;
A4: x2 * N meets B by A2, Th14;
consider x19 being object such that
A5: ( x19 in x1 * N & x19 in A ) by A3, XBOOLE_0:3;
consider x29 being object such that
A6: ( x29 in x2 * N & x29 in B ) by A4, XBOOLE_0:3;
reconsider x19 = x19 as Element of G by A5;
reconsider x29 = x29 as Element of G by A6;
A7: x19 * x29 in A * B by A5, A6;
x19 * x29 in (x1 * N) * (x2 * N) by A5, A6;
then (x1 * N) * (x2 * N) meets A * B by A7, XBOOLE_0:3;
then (x1 * x2) * N meets A * B by Th1;
hence x in N ~ (A * B) by A2; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ~ (A * B) or x in (N ~ A) * (N ~ B) )
assume A8: x in N ~ (A * B) ; :: thesis: x in (N ~ A) * (N ~ B)
then reconsider x = x as Element of G ;
x * N meets A * B by A8, Th28;
then consider x1 being object such that
A9: ( x1 in x * N & x1 in A * B ) by XBOOLE_0:3;
reconsider x1 = x1 as Element of G by A9;
consider y1, y2 being Element of G such that
A10: ( x1 = y1 * y2 & y1 in A & y2 in B ) by A9;
x * N = (y1 * y2) * N by A9, A10, Th2
.= (y1 * N) * (y2 * N) by Th1 ;
then x in (y1 * N) * (y2 * N) by GROUP_2:108;
then consider g1, g2 being Element of G such that
A11: ( x = g1 * g2 & g1 in y1 * N & g2 in y2 * N ) ;
( y1 * N = g1 * N & y2 * N = g2 * N ) by A11, Th2;
then ( y1 in g1 * N & y2 in g2 * N ) by GROUP_2:108;
then ( g1 * N meets A & g2 * N meets B ) by A10, XBOOLE_0:3;
then ( g1 in N ~ A & g2 in N ~ B ) ;
hence x in (N ~ A) * (N ~ B) by A11; :: thesis: verum