let G1, G2 be Group; ( G1 is trivial implies product <*G1,G2*>,G2 are_isomorphic )
assume A1:
G1 is trivial
; product <*G1,G2*>,G2 are_isomorphic
ex f being Homomorphism of (product <*G1,G2*>),G2 st f is bijective
proof
set I =
{1,2};
reconsider i = 2 as
Element of
{1,2} by TARSKI:def 2;
set F =
<*G1,G2*>;
deffunc H1()
-> set = the
carrier of
(product <*G1,G2*>);
deffunc H2()
-> set = the
carrier of
G2;
defpred S1[
Element of
H1(),
Element of
H2()]
means $2
= $1
. i;
AA1:
for
x being
Element of
H1() ex
y being
Element of
H2() st
S1[
x,
y]
proof
let x be
Element of
H1();
ex y being Element of H2() st S1[x,y]
(
x . 1
in G1 &
x . 2
in G2 &
dom x = {1,2} )
by Th6;
then reconsider y =
x . i as
Element of
G2 ;
take
y
;
S1[x,y]
thus
S1[
x,
y]
;
verum
end;
consider f being
Function of
H1(),
H2()
such that A2:
for
g being
Element of
H1() holds
S1[
g,
f . g]
from FUNCT_2:sch 3(AA1);
for
a,
b being
Element of
(product <*G1,G2*>) holds
f . (a * b) = (f . a) * (f . b)
proof
let a,
b be
Element of
(product <*G1,G2*>);
f . (a * b) = (f . a) * (f . b)
(
a . 1
in G1 &
a . 2
in G2 &
dom a = {1,2} )
by Th6;
then B1a:
(
a . 1
in G1 &
a . 2
in G2 &
len a = 2 )
by FINSEQ_1:2, FINSEQ_1:def 3;
then reconsider a1 =
a . 1 as
Element of
G1 ;
reconsider a2 =
a . 2 as
Element of
G2 by B1a;
B1:
a = <*a1,a2*>
by B1a, FINSEQ_1:44;
(
b . 1
in G1 &
b . 2
in G2 &
dom b = {1,2} )
by Th6;
then B2a:
(
b . 1
in G1 &
b . 2
in G2 &
len b = 2 )
by FINSEQ_1:2, FINSEQ_1:def 3;
then reconsider b1 =
b . 1 as
Element of
G1 ;
reconsider b2 =
b . 2 as
Element of
G2 by B2a;
b = <*b1,b2*>
by B2a, FINSEQ_1:44;
hence f . (a * b) =
f . <*(a1 * b1),(a2 * b2)*>
by B1, GROUP_7:29
.=
<*(a1 * b1),(a2 * b2)*> . i
by A2
.=
(f . a) * b2
by A2
.=
(f . a) * (f . b)
by A2
;
verum
end;
then reconsider f =
f as
Homomorphism of
(product <*G1,G2*>),
G2 by GROUP_6:def 6;
take
f
;
f is bijective
for
a,
b being
object st
a in H1() &
b in H1() &
f . a = f . b holds
a = b
proof
let a,
b be
object ;
( a in H1() & b in H1() & f . a = f . b implies a = b )
assume
a in H1()
;
( not b in H1() or not f . a = f . b or a = b )
then reconsider aa =
a as
Element of
(product <*G1,G2*>) ;
assume
b in H1()
;
( not f . a = f . b or a = b )
then reconsider bb =
b as
Element of
(product <*G1,G2*>) ;
assume B2:
f . a = f . b
;
a = b
(
aa . 1
in G1 &
aa . 2
in G2 &
dom aa = {1,2} )
by Th6;
then B3:
(
aa . 1
in G1 &
aa . 2
in G2 &
len aa = 2 )
by FINSEQ_1:2, FINSEQ_1:def 3;
then reconsider a1 =
aa . 1 as
Element of
G1 ;
reconsider a2 =
aa . 2 as
Element of
G2 by B3;
B4:
a = <*a1,a2*>
by B3, FINSEQ_1:44;
(
bb . 1
in G1 &
bb . 2
in G2 &
dom bb = {1,2} )
by Th6;
then B5:
(
bb . 1
in G1 &
bb . 2
in G2 &
len bb = 2 )
by FINSEQ_1:2, FINSEQ_1:def 3;
then reconsider b1 =
bb . 1 as
Element of
G1 ;
reconsider b2 =
bb . 2 as
Element of
G2 by B5;
B6:
b = <*b1,b2*>
by B5, FINSEQ_1:44;
B7:
(
a1 = 1_ G1 &
b1 = 1_ G1 )
by A1;
B8:
(
a2 = f . a &
b2 = f . b )
by A2;
hence a =
<*(1_ G1),(f . a)*>
by B4, B7
.=
<*(1_ G1),(f . b)*>
by B2
.=
<*b1,(f . b)*>
by B7
.=
<*b1,b2*>
by B8
.=
b
by B6
;
verum
end;
then A3:
f is
one-to-one
by FUNCT_2:19;
for
y being
object st
y in the
carrier of
G2 holds
ex
x being
object st
(
x in the
carrier of
(product <*G1,G2*>) &
y = f . x )
then
rng f = the
carrier of
G2
by FUNCT_2:10;
then
f is
onto
by FUNCT_2:def 3;
hence
f is
bijective
by A3;
verum
end;
hence
product <*G1,G2*>,G2 are_isomorphic
by GROUP_6:def 11; verum