let G be strict Group; for x, y being Element of G
for H, K being strict Subgroup of G holds
( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )
let x, y be Element of G; for H, K being strict Subgroup of G holds
( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )
let H, K be strict Subgroup of G; ( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )
per cases
( for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) or ex z being Element of G st
( z in (H * x) * K & z in (H * y) * K ) )
;
suppose
for
z being
Element of
G holds
( not
z in (H * x) * K or not
z in (H * y) * K )
;
( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )hence
(
(H * x) * K = (H * y) * K or for
z being
Element of
G holds
( not
z in (H * x) * K or not
z in (H * y) * K ) )
;
verum end; suppose
ex
z being
Element of
G st
(
z in (H * x) * K &
z in (H * y) * K )
;
( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )then consider z being
Element of
G such that A1:
z in (H * x) * K
and A2:
z in (H * y) * K
;
consider h1,
k1 being
Element of
G such that A3:
z = (h1 * x) * k1
and A4:
h1 in H
and A5:
k1 in K
by A1, Th17;
consider h2,
k2 being
Element of
G such that A6:
z = (h2 * y) * k2
and A7:
h2 in H
and A8:
k2 in K
by A2, Th17;
for
a being
object st
a in (H * x) * K holds
a in (H * y) * K
proof
let a be
object ;
( a in (H * x) * K implies a in (H * y) * K )
assume
a in (H * x) * K
;
a in (H * y) * K
then consider h,
k being
Element of
G such that A9:
a = (h * x) * k
and A10:
h in H
and A11:
k in K
by Th17;
ex
c,
d being
Element of
G st
(
a = (c * y) * d &
c in H &
d in K )
proof
h = h * (1_ G)
by GROUP_1:def 4;
then A12:
(h * x) * k = (((h * (1_ G)) * x) * (1_ G)) * k
by GROUP_1:def 4;
1_ G = (h1 ") * h1
by GROUP_1:def 5;
then A13:
(h * x) * k =
(((h * ((h1 ") * h1)) * x) * (k1 * (k1 "))) * k
by A12, GROUP_1:def 5
.=
((((h * ((h1 ") * h1)) * x) * k1) * (k1 ")) * k
by GROUP_1:def 3
.=
(((((h * (h1 ")) * h1) * x) * k1) * (k1 ")) * k
by GROUP_1:def 3
.=
((((h * (h1 ")) * (h1 * x)) * k1) * (k1 ")) * k
by GROUP_1:def 3
.=
(((h * (h1 ")) * ((h2 * y) * k2)) * (k1 ")) * k
by A3, A6, GROUP_1:def 3
.=
((((h * (h1 ")) * (h2 * y)) * k2) * (k1 ")) * k
by GROUP_1:def 3
.=
(((((h * (h1 ")) * h2) * y) * k2) * (k1 ")) * k
by GROUP_1:def 3
.=
((((h * (h1 ")) * h2) * y) * (k2 * (k1 "))) * k
by GROUP_1:def 3
.=
(((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k)
by GROUP_1:def 3
;
take
(h * (h1 ")) * h2
;
ex d being Element of G st
( a = (((h * (h1 ")) * h2) * y) * d & (h * (h1 ")) * h2 in H & d in K )
take
(k2 * (k1 ")) * k
;
( a = (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) & (h * (h1 ")) * h2 in H & (k2 * (k1 ")) * k in K )
h1 " in H
by A4, GROUP_2:51;
then A14:
h * (h1 ") in H
by A10, GROUP_2:50;
k1 " in K
by A5, GROUP_2:51;
then
k2 * (k1 ") in K
by A8, GROUP_2:50;
hence
(
a = (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) &
(h * (h1 ")) * h2 in H &
(k2 * (k1 ")) * k in K )
by A7, A9, A11, A13, A14, GROUP_2:50;
verum
end;
hence
a in (H * y) * K
by Th17;
verum
end; then A15:
(H * x) * K c= (H * y) * K
;
for
a being
object st
a in (H * y) * K holds
a in (H * x) * K
proof
let a be
object ;
( a in (H * y) * K implies a in (H * x) * K )
assume
a in (H * y) * K
;
a in (H * x) * K
then consider h,
k being
Element of
G such that A16:
a = (h * y) * k
and A17:
h in H
and A18:
k in K
by Th17;
ex
c,
d being
Element of
G st
(
a = (c * x) * d &
c in H &
d in K )
proof
h = h * (1_ G)
by GROUP_1:def 4;
then A19:
(h * y) * k = (((h * (1_ G)) * y) * (1_ G)) * k
by GROUP_1:def 4;
1_ G = (h2 ") * h2
by GROUP_1:def 5;
then A20:
(h * y) * k =
(((h * ((h2 ") * h2)) * y) * (k2 * (k2 "))) * k
by A19, GROUP_1:def 5
.=
((((h * ((h2 ") * h2)) * y) * k2) * (k2 ")) * k
by GROUP_1:def 3
.=
(((((h * (h2 ")) * h2) * y) * k2) * (k2 ")) * k
by GROUP_1:def 3
.=
((((h * (h2 ")) * (h2 * y)) * k2) * (k2 ")) * k
by GROUP_1:def 3
.=
(((h * (h2 ")) * ((h1 * x) * k1)) * (k2 ")) * k
by A3, A6, GROUP_1:def 3
.=
((((h * (h2 ")) * (h1 * x)) * k1) * (k2 ")) * k
by GROUP_1:def 3
.=
(((((h * (h2 ")) * h1) * x) * k1) * (k2 ")) * k
by GROUP_1:def 3
.=
((((h * (h2 ")) * h1) * x) * (k1 * (k2 "))) * k
by GROUP_1:def 3
.=
(((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k)
by GROUP_1:def 3
;
take
(h * (h2 ")) * h1
;
ex d being Element of G st
( a = (((h * (h2 ")) * h1) * x) * d & (h * (h2 ")) * h1 in H & d in K )
take
(k1 * (k2 ")) * k
;
( a = (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) & (h * (h2 ")) * h1 in H & (k1 * (k2 ")) * k in K )
h2 " in H
by A7, GROUP_2:51;
then A21:
h * (h2 ") in H
by A17, GROUP_2:50;
k2 " in K
by A8, GROUP_2:51;
then
k1 * (k2 ") in K
by A5, GROUP_2:50;
hence
(
a = (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) &
(h * (h2 ")) * h1 in H &
(k1 * (k2 ")) * k in K )
by A4, A16, A18, A20, A21, GROUP_2:50;
verum
end;
hence
a in (H * x) * K
by Th17;
verum
end; then
(H * y) * K c= (H * x) * K
;
hence
(
(H * x) * K = (H * y) * K or for
z being
Element of
G holds
( not
z in (H * x) * K or not
z in (H * y) * K ) )
by A15, XBOOLE_0:def 10;
verum end;