let G be Group; :: thesis: for H1, H2 being Subgroup of G

for N being normal Subgroup of G holds (N ~ H1) * (N ~ H2) = N ~ (H1 * H2)

let H1, H2 be Subgroup of G; :: thesis: for N being normal Subgroup of G holds (N ~ H1) * (N ~ H2) = N ~ (H1 * H2)

let N be normal Subgroup of G; :: thesis: (N ~ H1) * (N ~ H2) = N ~ (H1 * H2)

thus (N ~ H1) * (N ~ H2) c= N ~ (H1 * H2) :: according to XBOOLE_0:def 10 :: thesis: N ~ (H1 * H2) c= (N ~ H1) * (N ~ H2)

assume A8: x in N ~ (H1 * H2) ; :: thesis: x in (N ~ H1) * (N ~ H2)

then reconsider x = x as Element of G ;

x * N meets (carr H1) * (carr H2) by A8, Th28;

then consider x1 being object such that

A9: ( x1 in x * N & x1 in (carr H1) * (carr H2) ) 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 carr H1 & y2 in carr H2 ) 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 carr H1 & g2 * N meets carr H2 ) by A10, XBOOLE_0:3;

then ( g1 in N ~ H1 & g2 in N ~ H2 ) ;

hence x in (N ~ H1) * (N ~ H2) by A11; :: thesis: verum

for N being normal Subgroup of G holds (N ~ H1) * (N ~ H2) = N ~ (H1 * H2)

let H1, H2 be Subgroup of G; :: thesis: for N being normal Subgroup of G holds (N ~ H1) * (N ~ H2) = N ~ (H1 * H2)

let N be normal Subgroup of G; :: thesis: (N ~ H1) * (N ~ H2) = N ~ (H1 * H2)

thus (N ~ H1) * (N ~ H2) c= N ~ (H1 * H2) :: according to XBOOLE_0:def 10 :: thesis: N ~ (H1 * H2) c= (N ~ H1) * (N ~ H2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ~ (H1 * H2) or x in (N ~ H1) * (N ~ H2) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (N ~ H1) * (N ~ H2) or x in N ~ (H1 * H2) )

assume A1: x in (N ~ H1) * (N ~ H2) ; :: thesis: x in N ~ (H1 * H2)

then reconsider x = x as Element of G ;

consider x1, x2 being Element of G such that

A2: ( x = x1 * x2 & x1 in N ~ H1 & x2 in N ~ H2 ) by A1;

A3: x1 * N meets carr H1 by A2, Th51;

A4: x2 * N meets carr H2 by A2, Th51;

consider x19 being object such that

A5: ( x19 in x1 * N & x19 in carr H1 ) by A3, XBOOLE_0:3;

consider x29 being object such that

A6: ( x29 in x2 * N & x29 in carr H2 ) 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 (carr H1) * (carr H2) by A5, A6;

x19 * x29 in (x1 * N) * (x2 * N) by A5, A6;

then (x1 * N) * (x2 * N) meets (carr H1) * (carr H2) by A7, XBOOLE_0:3;

then (x1 * x2) * N meets (carr H1) * (carr H2) by Th1;

hence x in N ~ (H1 * H2) by A2; :: thesis: verum

end;assume A1: x in (N ~ H1) * (N ~ H2) ; :: thesis: x in N ~ (H1 * H2)

then reconsider x = x as Element of G ;

consider x1, x2 being Element of G such that

A2: ( x = x1 * x2 & x1 in N ~ H1 & x2 in N ~ H2 ) by A1;

A3: x1 * N meets carr H1 by A2, Th51;

A4: x2 * N meets carr H2 by A2, Th51;

consider x19 being object such that

A5: ( x19 in x1 * N & x19 in carr H1 ) by A3, XBOOLE_0:3;

consider x29 being object such that

A6: ( x29 in x2 * N & x29 in carr H2 ) 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 (carr H1) * (carr H2) by A5, A6;

x19 * x29 in (x1 * N) * (x2 * N) by A5, A6;

then (x1 * N) * (x2 * N) meets (carr H1) * (carr H2) by A7, XBOOLE_0:3;

then (x1 * x2) * N meets (carr H1) * (carr H2) by Th1;

hence x in N ~ (H1 * H2) by A2; :: thesis: verum

assume A8: x in N ~ (H1 * H2) ; :: thesis: x in (N ~ H1) * (N ~ H2)

then reconsider x = x as Element of G ;

x * N meets (carr H1) * (carr H2) by A8, Th28;

then consider x1 being object such that

A9: ( x1 in x * N & x1 in (carr H1) * (carr H2) ) 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 carr H1 & y2 in carr H2 ) 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 carr H1 & g2 * N meets carr H2 ) by A10, XBOOLE_0:3;

then ( g1 in N ~ H1 & g2 in N ~ H2 ) ;

hence x in (N ~ H1) * (N ~ H2) by A11; :: thesis: verum