let V be free Z_Module; for A, B being Subset of V st A c= B & B is Basis of V holds
ex F being linear-transformation of V,V st
( ( for v being Vector of V ex vA, vB being Vector of V st
( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & F . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
F . v = vA ) )
let A, B be Subset of V; ( A c= B & B is Basis of V implies ex F being linear-transformation of V,V st
( ( for v being Vector of V ex vA, vB being Vector of V st
( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & F . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
F . v = vA ) ) )
assume
( A c= B & B is Basis of V )
; ex F being linear-transformation of V,V st
( ( for v being Vector of V ex vA, vB being Vector of V st
( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & F . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
F . v = vA ) )
then P0:
V is_the_direct_sum_of Lin A, Lin (B \ A)
by ZMODUL05:50;
defpred S1[ Element of V, object ] means ex vA, vB being Vector of V st
( vA in Lin A & vB in Lin (B \ A) & $1 = vA + vB & $2 = vA );
A1:
for v being Element of V ex vA being Element of V st S1[v,vA]
consider f being Function of V,V such that
A9:
for v being Vector of V holds S1[v,f . v]
from FUNCT_2:sch 3(A1);
A10:
for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
f . v = vA
A13:
f is additive
proof
let x,
y be
Element of
V;
VECTSP_1:def 19 f . (x + y) = (f . x) + (f . y)
consider xA,
xB being
Vector of
V such that A14:
(
xA in Lin A &
xB in Lin (B \ A) &
x = xA + xB &
f . x = xA )
by A9;
consider yA,
yB being
Vector of
V such that A15:
(
yA in Lin A &
yB in Lin (B \ A) &
y = yA + yB &
f . y = yA )
by A9;
consider xyA,
xyB being
Vector of
V such that A16:
(
xyA in Lin A &
xyB in Lin (B \ A) &
x + y = xyA + xyB &
f . (x + y) = xyA )
by A9;
A17:
xyA + xyB =
((xA + xB) + yA) + yB
by A14, A15, A16, RLVECT_1:def 3
.=
(xB + (xA + yA)) + yB
by RLVECT_1:def 3
.=
(xA + yA) + (xB + yB)
by RLVECT_1:def 3
;
A18:
xA + yA in Lin A
by A14, A15, ZMODUL01:36;
xB + yB in Lin (B \ A)
by A14, A15, ZMODUL01:36;
hence
f . (x + y) = (f . x) + (f . y)
by A14, A15, A16, A17, A18, P0, ZMODUL01:134;
verum
end;
for r being Element of INT.Ring
for x being Element of V holds f . (r * x) = r * (f . x)
proof
let r be
Element of
INT.Ring;
for x being Element of V holds f . (r * x) = r * (f . x)let x be
Element of
V;
f . (r * x) = r * (f . x)
consider xA,
xB being
Vector of
V such that A14:
(
xA in Lin A &
xB in Lin (B \ A) &
x = xA + xB &
f . x = xA )
by A9;
consider rxA,
rxB being
Vector of
V such that A15:
(
rxA in Lin A &
rxB in Lin (B \ A) &
r * x = rxA + rxB &
f . (r * x) = rxA )
by A9;
A16:
rxA + rxB = (r * xA) + (r * xB)
by A14, A15, VECTSP_1:def 14;
A18:
r * xA in Lin A
by A14, ZMODUL01:37;
r * xB in Lin (B \ A)
by A14, ZMODUL01:37;
hence
f . (r * x) = r * (f . x)
by A14, A15, A16, A18, P0, ZMODUL01:134;
verum
end;
then
f is homogeneous
;
then reconsider f = f as linear-transformation of V,V by A13;
take
f
; ( ( for v being Vector of V ex vA, vB being Vector of V st
( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & f . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
f . v = vA ) )
thus
( ( for v being Vector of V ex vA, vB being Vector of V st
( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & f . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
f . v = vA ) )
by A10, A9; verum