let K be Field; for V being finite-dimensional VectSp of K
for W being Subspace of V ex S being Linear_Compl of W ex T being linear-transformation of S,(VectQuot (V,W)) st
( T is bijective & ( for v being Vector of V st v in S holds
T . v = v + W ) )
let V be finite-dimensional VectSp of K; for W being Subspace of V ex S being Linear_Compl of W ex T being linear-transformation of S,(VectQuot (V,W)) st
( T is bijective & ( for v being Vector of V st v in S holds
T . v = v + W ) )
let W be Subspace of V; ex S being Linear_Compl of W ex T being linear-transformation of S,(VectQuot (V,W)) st
( T is bijective & ( for v being Vector of V st v in S holds
T . v = v + W ) )
set S = the Linear_Compl of W;
set aC = addCoset (V,W);
set C = CosetSet (V,W);
set Vq = VectQuot (V,W);
defpred S1[ Vector of V, Vector of (VectQuot (V,W))] means $2 = $1 + W;
consider ff being Function of the carrier of V, the carrier of (VectQuot (V,W)) such that
A7:
for v being Vector of V holds S1[v,ff . v]
from FUNCT_2:sch 3(A2);
set T = ff | the carrier of the Linear_Compl of W;
S1:
the carrier of the Linear_Compl of W c= the carrier of V
by VECTSP_4:def 2;
then reconsider T = ff | the carrier of the Linear_Compl of W as Function of the carrier of the Linear_Compl of W, the carrier of (VectQuot (V,W)) by FUNCT_2:32;
P1:
for v being Vector of V st v in the Linear_Compl of W holds
T . v = v + W
then AD:
T is additive
;
then
T is homogeneous
;
then reconsider T = T as linear-transformation of the Linear_Compl of W,(VectQuot (V,W)) by AD;
A100:
V is_the_direct_sum_of the Linear_Compl of W,W
by VECTSP_5:def 5;
the carrier of (VectQuot (V,W)) c= rng T
proof
let y be
object ;
TARSKI:def 3 ( not y in the carrier of (VectQuot (V,W)) or y in rng T )
assume
y in the
carrier of
(VectQuot (V,W))
;
y in rng T
then consider a being
Vector of
V such that A10:
y = a + W
by VECTSP10:22;
ModuleStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
lmult of
V #)
= the
Linear_Compl of
W + W
by A100, VECTSP_5:def 4;
then
a in the
Linear_Compl of
W + W
;
then consider s,
w being
Element of
V such that A12:
(
s in the
Linear_Compl of
W &
w in W &
a = s + w )
by VECTSP_5:1;
reconsider s0 =
s as
Vector of the
Linear_Compl of
W by A12;
reconsider B =
s + W as
Vector of
(VectQuot (V,W)) by VECTSP10:23;
reconsider A =
a + W,
Z =
w + W as
Vector of
(VectQuot (V,W)) by VECTSP10:23;
Z =
zeroCoset (
V,
W)
by A12, VECTSP_4:49
.=
0. (VectQuot (V,W))
by VECTSP10:def 6
;
then A13:
B =
B + Z
.=
A
by A12, VECTSP10:26
;
T . s0 = y
by A10, A12, A13, P1;
hence
y in rng T
by FUNCT_2:4;
verum
end;
then
rng T = the carrier of (VectQuot (V,W))
;
then A14:
T is onto
;
X1:
for x1, x2 being object st x1 in the carrier of the Linear_Compl of W & x2 in the carrier of the Linear_Compl of W & T . x1 = T . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in the carrier of the Linear_Compl of W & x2 in the carrier of the Linear_Compl of W & T . x1 = T . x2 implies x1 = x2 )
assume A15:
(
x1 in the
carrier of the
Linear_Compl of
W &
x2 in the
carrier of the
Linear_Compl of
W &
T . x1 = T . x2 )
;
x1 = x2
then reconsider a1 =
x1,
a2 =
x2 as
Vector of
V by S1;
A16:
(
a1 in the
Linear_Compl of
W &
a2 in the
Linear_Compl of
W )
by A15;
A17:
T . x1 = a1 + W
by P1, A16;
T . x2 = a2 + W
by P1, A16;
then consider w being
Element of
V such that A19:
(
w in W &
a2 = a1 + w )
by A15, A17, VECTSP_4:42, VECTSP_4:55;
A20:
a2 - a1 =
w + (a1 - a1)
by A19, RLVECT_1:28
.=
w + (0. V)
by VECTSP_1:19
.=
w
;
a2 - a1 in the
Linear_Compl of
W
by A16, VECTSP_4:23;
then
a2 - a1 in the
Linear_Compl of
W /\ W
by A19, A20, VECTSP_5:3;
then
a2 - a1 in (0). V
by A100, VECTSP_5:def 4;
then
a2 - a1 = 0. V
by VECTSP_4:35;
hence
x1 = x2
by RLVECT_1:21;
verum
end;
take
the Linear_Compl of W
; ex T being linear-transformation of the Linear_Compl of W,(VectQuot (V,W)) st
( T is bijective & ( for v being Vector of V st v in the Linear_Compl of W holds
T . v = v + W ) )
take
T
; ( T is bijective & ( for v being Vector of V st v in the Linear_Compl of W holds
T . v = v + W ) )
thus
( T is bijective & ( for v being Vector of V st v in the Linear_Compl of W holds
T . v = v + W ) )
by A14, P1, X1, FUNCT_2:19; verum