let G be Group; for A being non empty Subset of G
for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )
let A be non empty Subset of G; for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )
let N1, N2 be strict normal Subgroup of G; ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )
consider N being strict normal Subgroup of G such that
A1:
the carrier of N = N1 * N2
by Th8;
N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1)
proof
let x be
object ;
TARSKI:def 3 ( not x in N ~ A or x in ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )
assume A2:
x in N ~ A
;
x in ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1)
then reconsider x =
x as
Element of
G ;
x * N meets A
by A2, Th14;
then consider x1 being
object such that A3:
(
x1 in x * N &
x1 in A )
by XBOOLE_0:3;
reconsider x1 =
x1 as
Element of
G by A3;
consider y being
Element of
G such that A4:
(
x1 = x * y &
y in N )
by A3, GROUP_2:103;
A5:
y in N1 * N2
by A1, A4, STRUCT_0:def 5;
then consider a,
b being
Element of
G such that A6:
(
y = a * b &
a in N1 &
b in N2 )
by Th6;
A7:
x1 = (x * a) * b
by A4, A6, GROUP_1:def 3;
a in carr N1
by A6, STRUCT_0:def 5;
then A8:
(x * a) * b in (x * N1) * b
by GROUP_8:15;
(x * N1) * b =
x * (N1 * b)
by GROUP_2:106
.=
x * (b * N1)
by GROUP_3:117
.=
(x * b) * N1
by GROUP_2:105
;
then
(x * b) * N1 meets A
by A3, A7, A8, XBOOLE_0:3;
then A9:
x * b in N1 ~ A
;
A10:
(x * b) * (b ") =
x * (b * (b "))
by GROUP_1:def 3
.=
x * (1_ G)
by GROUP_1:def 5
.=
x
by GROUP_1:def 4
;
b " in N2
by A6, GROUP_2:51;
then A11:
x in (N1 ~ A) * N2
by A9, A10, GROUP_2:94;
y in N2 * N1
by A5, GROUP_3:125;
then consider a,
b being
Element of
G such that A12:
(
y = a * b &
a in N2 &
b in N1 )
by Th6;
A13:
x1 = (x * a) * b
by A4, A12, GROUP_1:def 3;
a in carr N2
by A12, STRUCT_0:def 5;
then A14:
(x * a) * b in (x * N2) * b
by GROUP_8:15;
(x * N2) * b =
x * (N2 * b)
by GROUP_2:106
.=
x * (b * N2)
by GROUP_3:117
.=
(x * b) * N2
by GROUP_2:105
;
then
(x * b) * N2 meets A
by A3, A13, A14, XBOOLE_0:3;
then A15:
x * b in N2 ~ A
;
A16:
(x * b) * (b ") =
x * (b * (b "))
by GROUP_1:def 3
.=
x * (1_ G)
by GROUP_1:def 5
.=
x
by GROUP_1:def 4
;
b " in N1
by A12, GROUP_2:51;
then
x in (N2 ~ A) * N1
by A15, A16, GROUP_2:94;
hence
x in ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1)
by A11, XBOOLE_0:def 4;
verum
end;
hence
ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )
by A1; verum