set S = semidirect_product (G,A,phi);
thus
for x, y, z being Element of (semidirect_product (G,A,phi)) holds (x * y) * z = x * (y * z)
GROUP_1:def 3 semidirect_product (G,A,phi) is Group-like proof
let x,
y,
z be
Element of
(semidirect_product (G,A,phi));
(x * y) * z = x * (y * z)
consider g1 being
Element of
G,
a1 being
Element of
A such that A1:
x = <*g1,a1*>
by Th12;
consider g2 being
Element of
G,
a2 being
Element of
A such that A2:
y = <*g2,a2*>
by Th12;
consider g3 being
Element of
G,
a3 being
Element of
A such that A3:
z = <*g3,a3*>
by Th12;
reconsider phi1 =
phi . a1,
phi2 =
phi . a2,
phi12 =
phi . (a1 * a2) as
Homomorphism of
G,
G by AUTGROUP:def 1;
x * y = <*(g1 * (phi1 . g2)),(a1 * a2)*>
by A1, A2, Th14;
then A5:
(x * y) * z = <*((g1 * (phi1 . g2)) * (phi12 . g3)),((a1 * a2) * a3)*>
by A3, Th14;
y * z = <*(g2 * (phi2 . g3)),(a2 * a3)*>
by A2, A3, Th14;
then A6:
x * (y * z) = <*(g1 * (phi1 . (g2 * (phi2 . g3)))),(a1 * (a2 * a3))*>
by A1, Th14;
A7:
(a1 * a2) * a3 = a1 * (a2 * a3)
by GROUP_1:def 3;
phi1 . (phi2 . g3) = phi12 . g3
by Th18;
then
(phi1 . g2) * (phi12 . g3) = phi1 . (g2 * (phi2 . g3))
by GROUP_6:def 6;
hence
(x * y) * z = x * (y * z)
by A5, A6, A7, GROUP_1:def 3;
verum
end;
set S = semidirect_product (G,A,phi);
for h being Element of (semidirect_product (G,A,phi)) ex g being Element of (semidirect_product (G,A,phi)) st
( h * g = 1_ (semidirect_product (G,A,phi)) & g * h = 1_ (semidirect_product (G,A,phi)) )
proof
let h be
Element of
(semidirect_product (G,A,phi));
ex g being Element of (semidirect_product (G,A,phi)) st
( h * g = 1_ (semidirect_product (G,A,phi)) & g * h = 1_ (semidirect_product (G,A,phi)) )
consider g being
Element of
G,
a being
Element of
A such that B1:
h = <*g,a*>
by Th12;
reconsider phi1 =
phi . (a ") as
Homomorphism of
G,
G by AUTGROUP:def 1;
reconsider y =
<*(phi1 . (g ")),(a ")*> as
Element of
(semidirect_product (G,A,phi)) by Th9;
take
y
;
( h * y = 1_ (semidirect_product (G,A,phi)) & y * h = 1_ (semidirect_product (G,A,phi)) )
thus
h * y = 1_ (semidirect_product (G,A,phi))
by B1, Th20;
y * h = 1_ (semidirect_product (G,A,phi))
thus
y * h = 1_ (semidirect_product (G,A,phi))
by B1, Th20;
verum
end;
hence
semidirect_product (G,A,phi) is Group-like
by thUnitalMagmaIsGroupCond; verum