let G, A be Group; semidirect_product (G,A,(1: (A,(AutGroup G)))) = product <*G,A*>
set S = semidirect_product (G,A,(1: (A,(AutGroup G))));
A1:
the carrier of (semidirect_product (G,A,(1: (A,(AutGroup G))))) = the carrier of (product <*G,A*>)
by Th9;
set B1 = the multF of (semidirect_product (G,A,(1: (A,(AutGroup G)))));
set B2 = the multF of (product <*G,A*>);
set U = product (Carrier <*G,A*>);
A2:
( the multF of (semidirect_product (G,A,(1: (A,(AutGroup G))))) is BinOp of (product (Carrier <*G,A*>)) & the multF of (product <*G,A*>) is BinOp of (product (Carrier <*G,A*>)) )
proof
( the
carrier of
(semidirect_product (G,A,(1: (A,(AutGroup G))))) = product (Carrier <*G,A*>) & the
multF of
(semidirect_product (G,A,(1: (A,(AutGroup G))))) is
BinOp of the
carrier of
(semidirect_product (G,A,(1: (A,(AutGroup G))))) )
by Def1;
hence
the
multF of
(semidirect_product (G,A,(1: (A,(AutGroup G))))) is
BinOp of
(product (Carrier <*G,A*>))
;
the multF of (product <*G,A*>) is BinOp of (product (Carrier <*G,A*>))
( the
carrier of
(product <*G,A*>) = product (Carrier <*G,A*>) & the
multF of
(product <*G,A*>) is
BinOp of the
carrier of
(product <*G,A*>) )
by GROUP_7:def 2;
hence
the
multF of
(product <*G,A*>) is
BinOp of
(product (Carrier <*G,A*>))
;
verum
end;
for x, y being Element of product (Carrier <*G,A*>) holds the multF of (semidirect_product (G,A,(1: (A,(AutGroup G))))) . (x,y) = the multF of (product <*G,A*>) . (x,y)
proof
let x,
y be
Element of
product (Carrier <*G,A*>);
the multF of (semidirect_product (G,A,(1: (A,(AutGroup G))))) . (x,y) = the multF of (product <*G,A*>) . (x,y)
x is
Element of
(semidirect_product (G,A,(1: (A,(AutGroup G)))))
by Def1;
then consider g1 being
Element of
G,
a1 being
Element of
A such that A4:
x = <*g1,a1*>
by Th12;
y is
Element of
(semidirect_product (G,A,(1: (A,(AutGroup G)))))
by Def1;
then consider g2 being
Element of
G,
a2 being
Element of
A such that A5:
y = <*g2,a2*>
by Th12;
1: (
A,
(AutGroup G))
= A --> (1_ (AutGroup G))
by GROUP_6:def 7;
then
(1: (A,(AutGroup G))) . a1 = id the
carrier of
G
by AUTGROUP:9;
then A6:
((1: (A,(AutGroup G))) . a1) . g2 = g2
;
reconsider x0 =
x,
y0 =
y as
Element of
(semidirect_product (G,A,(1: (A,(AutGroup G))))) by Def1;
A8:
x0 * y0 = <*(g1 * g2),(a1 * a2)*>
by A4, A5, A6, Th14;
the
multF of
(product <*G,A*>) . (
x,
y) =
<*g1,a1*> * <*g2,a2*>
by A4, A5
.=
<*(g1 * g2),(a1 * a2)*>
by GROUP_7:29
;
hence
the
multF of
(semidirect_product (G,A,(1: (A,(AutGroup G))))) . (
x,
y)
= the
multF of
(product <*G,A*>) . (
x,
y)
by A8;
verum
end;
hence
semidirect_product (G,A,(1: (A,(AutGroup G)))) = product <*G,A*>
by A1, A2, BINOP_1:2; verum