let R be Ring; for V being LeftMod of R
for W1, W2 being Submodule of V
for U1 being Submodule of W1 + W2
for U2 being strict Submodule of W1 st U1 = W2 & U2 = W1 /\ W2 holds
ex F being linear-transformation of (VectQuot ((W1 + W2),U1)),(VectQuot (W1,U2)) st F is bijective
let V be LeftMod of R; for W1, W2 being Submodule of V
for U1 being Submodule of W1 + W2
for U2 being strict Submodule of W1 st U1 = W2 & U2 = W1 /\ W2 holds
ex F being linear-transformation of (VectQuot ((W1 + W2),U1)),(VectQuot (W1,U2)) st F is bijective
let W1, W2 be Submodule of V; for U1 being Submodule of W1 + W2
for U2 being strict Submodule of W1 st U1 = W2 & U2 = W1 /\ W2 holds
ex F being linear-transformation of (VectQuot ((W1 + W2),U1)),(VectQuot (W1,U2)) st F is bijective
let U1 be Submodule of W1 + W2; for U2 being strict Submodule of W1 st U1 = W2 & U2 = W1 /\ W2 holds
ex F being linear-transformation of (VectQuot ((W1 + W2),U1)),(VectQuot (W1,U2)) st F is bijective
let U2 be strict Submodule of W1; ( U1 = W2 & U2 = W1 /\ W2 implies ex F being linear-transformation of (VectQuot ((W1 + W2),U1)),(VectQuot (W1,U2)) st F is bijective )
assume A1:
( U1 = W2 & U2 = W1 /\ W2 )
; ex F being linear-transformation of (VectQuot ((W1 + W2),U1)),(VectQuot (W1,U2)) st F is bijective
set Z1 = VectQuot ((W1 + W2),U1);
set Z2 = VectQuot (W1,U2);
defpred S1[ object , object ] means ex v being Element of (W1 + W2) st
( $1 = v & $2 = v + U1 );
A2:
for z being Element of W1 ex y being Element of (VectQuot ((W1 + W2),U1)) st S1[z,y]
consider f being Function of the carrier of W1, the carrier of (VectQuot ((W1 + W2),U1)) such that
A3:
for z being Element of W1 holds S1[z,f . z]
from FUNCT_2:sch 3(A2);
f is linear-transformation of W1,(VectQuot ((W1 + W2),U1))
proof
for
x,
y being
Element of
W1 holds
f . (x + y) = (f . x) + (f . y)
proof
let x,
y be
Element of
W1;
f . (x + y) = (f . x) + (f . y)
consider xx being
Element of
(W1 + W2) such that C1:
(
x = xx &
f . x = xx + U1 )
by A3;
consider yy being
Element of
(W1 + W2) such that C2:
(
y = yy &
f . y = yy + U1 )
by A3;
consider xy being
Element of
(W1 + W2) such that C3:
(
x + y = xy &
f . (x + y) = xy + U1 )
by A3;
reconsider xv =
x,
yv =
y as
Element of
V by ZMODUL01:25;
(
xx + U1 is
Coset of
U1 &
yy + U1 is
Coset of
U1 )
by VECTSP_4:def 6;
then
(
xx + U1 in CosetSet (
(W1 + W2),
U1) &
yy + U1 in CosetSet (
(W1 + W2),
U1) )
;
then reconsider xU =
xx + U1,
yU =
yy + U1 as
Element of
CosetSet (
(W1 + W2),
U1) ;
C4:
xx + yy =
xv + yv
by C1, C2, ZMODUL01:28
.=
xy
by C3, ZMODUL01:28
;
thus (f . x) + (f . y) =
(addCoset ((W1 + W2),U1)) . (
xU,
yU)
by C1, C2, VECTSP10:def 6
.=
f . (x + y)
by C3, C4, VECTSP10:def 3
;
verum
end;
then B1:
f is
additive
;
for
a being
Element of
R for
x being
Element of
W1 holds
f . (a * x) = a * (f . x)
then
f is
homogeneous
;
hence
f is
linear-transformation of
W1,
(VectQuot ((W1 + W2),U1))
by B1;
verum
end;
then reconsider f = f as linear-transformation of W1,(VectQuot ((W1 + W2),U1)) ;
A4:
ker f = U2
A5:
im f = VectQuot ((W1 + W2),U1)
proof
for
y being
object st
y in the
carrier of
(VectQuot ((W1 + W2),U1)) holds
f " {y} <> {}
proof
let y be
object ;
( y in the carrier of (VectQuot ((W1 + W2),U1)) implies f " {y} <> {} )
assume C2:
y in the
carrier of
(VectQuot ((W1 + W2),U1))
;
f " {y} <> {}
y in CosetSet (
(W1 + W2),
U1)
by C2, VECTSP10:def 6;
then consider yy being
Coset of
U1 such that C8:
y = yy
;
consider z being
Element of
(W1 + W2) such that C3:
y = z + U1
by C8, VECTSP_4:def 6;
z in W1 + W2
;
then consider z1,
z2 being
Element of
V such that C4:
(
z1 in W1 &
z2 in W2 &
z = z1 + z2 )
by ZMODUL01:92;
reconsider zz1 =
z1 as
Element of
W1 by C4;
consider zzz1 being
Element of
(W1 + W2) such that C6:
(
zz1 = zzz1 &
f . zz1 = zzz1 + U1 )
by A3;
z2 in W1 + W2
by C4, ZMODUL01:93;
then reconsider zzz2 =
z2 as
Element of
(W1 + W2) ;
C7:
z = zzz1 + zzz2
by C4, C6, ZMODUL01:28;
y = f . zz1
by A1, C3, C4, C6, C7, ZMODUL01:65;
then
f . zz1 in {y}
by TARSKI:def 1;
hence
f " {y} <> {}
by FUNCT_2:38;
verum
end;
then B1:
rng f = the
carrier of
(VectQuot ((W1 + W2),U1))
by FUNCT_2:41;
B2:
dom f = the
carrier of
W1
by FUNCT_2:def 1;
the
carrier of
(im f) =
[#] (im f)
.=
f .: ([#] W1)
by RANKNULL:def 2
.=
the
carrier of
(VectQuot ((W1 + W2),U1))
by B1, B2, RELAT_1:113
;
hence
im f = VectQuot (
(W1 + W2),
U1)
by ZMODUL01:47;
verum
end;
reconsider F = Zdecom f as linear-transformation of (VectQuot (W1,U2)),(VectQuot ((W1 + W2),U1)) by A4, A5;
consider FI being linear-transformation of (VectQuot ((W1 + W2),U1)),(VectQuot (W1,U2)) such that
X1:
( FI = F " & FI is bijective )
by A4, A5, defdecom, ZMODUL06:42;
take
FI
; FI is bijective
thus
FI is bijective
by X1; verum