let X, Y be AbGroup; ex I being Homomorphism of [:X,Y:],[:X,(product <*Y*>):] st
( I is bijective & ( for x being Element of X
for y being Element of Y holds I . (x,y) = [x,<*y*>] ) )
consider J being Homomorphism of Y,(product <*Y*>) such that
A1:
( J is bijective & ( for y being Element of Y holds J . y = <*y*> ) )
by Th1;
defpred S1[ object , object , object ] means $3 = [$1,<*$2*>];
A2:
for x, y being object st x in the carrier of X & y in the carrier of Y holds
ex z being object st
( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] )
proof
let x,
y be
object ;
( x in the carrier of X & y in the carrier of Y implies ex z being object st
( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) )
assume A3:
(
x in the
carrier of
X &
y in the
carrier of
Y )
;
ex z being object st
( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] )
then reconsider y0 =
y as
Element of
Y ;
reconsider z =
[x,<*y0*>] as
set by TARSKI:1;
take
z
;
( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] )
J . y0 = <*y0*>
by A1;
hence
(
z in the
carrier of
[:X,(product <*Y*>):] &
S1[
x,
y,
z] )
by A3, ZFMISC_1:87;
verum
end;
consider I being Function of [: the carrier of X, the carrier of Y:], the carrier of [:X,(product <*Y*>):] such that
A4:
for x, y being object st x in the carrier of X & y in the carrier of Y holds
S1[x,y,I . (x,y)]
from BINOP_1:sch 1(A2);
reconsider I = I as Function of [:X,Y:],[:X,(product <*Y*>):] ;
for v, w being Element of [:X,Y:] holds I . (v + w) = (I . v) + (I . w)
proof
let v,
w be
Element of
[:X,Y:];
I . (v + w) = (I . v) + (I . w)
consider x1 being
Element of
X,
x2 being
Element of
Y such that A5:
v = [x1,x2]
by SUBSET_1:43;
consider y1 being
Element of
X,
y2 being
Element of
Y such that A6:
w = [y1,y2]
by SUBSET_1:43;
A7:
I . (v + w) =
I . (
(x1 + y1),
(x2 + y2))
by A5, A6, PRVECT_3:def 1
.=
[(x1 + y1),<*(x2 + y2)*>]
by A4
;
(
I . v = I . (
x1,
x2) &
I . w = I . (
y1,
y2) )
by A5, A6;
then A8:
(
I . v = [x1,<*x2*>] &
I . w = [y1,<*y2*>] )
by A4;
A9:
(
J . x2 = <*x2*> &
J . y2 = <*y2*> )
by A1;
then reconsider xx2 =
<*x2*> as
Element of
(product <*Y*>) ;
reconsider yy2 =
<*y2*> as
Element of
(product <*Y*>) by A9;
<*(x2 + y2)*> =
J . (x2 + y2)
by A1
.=
xx2 + yy2
by A9, VECTSP_1:def 20
;
hence
(I . v) + (I . w) = I . (v + w)
by A7, A8, PRVECT_3:def 1;
verum
end;
then reconsider I = I as Homomorphism of [:X,Y:],[:X,(product <*Y*>):] by VECTSP_1:def 20;
take
I
; ( I is bijective & ( for x being Element of X
for y being Element of Y holds I . (x,y) = [x,<*y*>] ) )
now for z1, z2 being object st z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 holds
z1 = z2let z1,
z2 be
object ;
( z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 implies z1 = z2 )assume A10:
(
z1 in the
carrier of
[:X,Y:] &
z2 in the
carrier of
[:X,Y:] &
I . z1 = I . z2 )
;
z1 = z2consider x1,
y1 being
object such that A11:
(
x1 in the
carrier of
X &
y1 in the
carrier of
Y &
z1 = [x1,y1] )
by A10, ZFMISC_1:def 2;
consider x2,
y2 being
object such that A12:
(
x2 in the
carrier of
X &
y2 in the
carrier of
Y &
z2 = [x2,y2] )
by A10, ZFMISC_1:def 2;
[x1,<*y1*>] =
I . (
x1,
y1)
by A4, A11
.=
I . (
x2,
y2)
by A10, A11, A12
.=
[x2,<*y2*>]
by A4, A12
;
then
(
x1 = x2 &
<*y1*> = <*y2*> )
by XTUPLE_0:1;
hence
z1 = z2
by A11, A12, FINSEQ_1:76;
verum end;
then A13:
I is one-to-one
by FUNCT_2:19;
now for w being object st w in the carrier of [:X,(product <*Y*>):] holds
w in rng Ilet w be
object ;
( w in the carrier of [:X,(product <*Y*>):] implies w in rng I )assume
w in the
carrier of
[:X,(product <*Y*>):]
;
w in rng Ithen consider x,
y1 being
object such that A14:
(
x in the
carrier of
X &
y1 in the
carrier of
(product <*Y*>) &
w = [x,y1] )
by ZFMISC_1:def 2;
y1 in rng J
by A1, A14, FUNCT_2:def 3;
then consider y being
object such that A15:
(
y in the
carrier of
Y &
y1 = J . y )
by FUNCT_2:11;
reconsider z =
[x,y] as
Element of
[: the carrier of X, the carrier of Y:] by A14, A15, ZFMISC_1:87;
J . y = <*y*>
by A15, A1;
then
w = I . (
x,
y)
by A4, A14, A15;
then
w = I . z
;
hence
w in rng I
by FUNCT_2:4;
verum end;
then
the carrier of [:X,(product <*Y*>):] c= rng I
by TARSKI:def 3;
then
I is onto
by FUNCT_2:def 3, XBOOLE_0:def 10;
hence
I is bijective
by A13; for x being Element of X
for y being Element of Y holds I . (x,y) = [x,<*y*>]
thus
for x being Element of X
for y being Element of Y holds I . (x,y) = [x,<*y*>]
by A4; verum