let K be Field; :: thesis: 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; :: thesis: 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; :: thesis: 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 S_{1}[ Vector of V, Vector of (VectQuot (V,W))] means $2 = $1 + W;

A7: for v being Vector of V holds S_{1}[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 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

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

( T is bijective & ( for v being Vector of V st v in the Linear_Compl of W holds

T . v = v + W ) )

take T ; :: thesis: ( 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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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 S

A2: now :: thesis: for v being Vector of V ex y being Vector of (VectQuot (V,W)) st S_{1}[v,y]

consider ff being Function of the carrier of V, the carrier of (VectQuot (V,W)) such that let v be Vector of V; :: thesis: ex y being Vector of (VectQuot (V,W)) st S_{1}[v,y]

reconsider y = v + W as Vector of (VectQuot (V,W)) by VECTSP10:23;

take y = y; :: thesis: S_{1}[v,y]

thus S_{1}[v,y]
; :: thesis: verum

end;reconsider y = v + W as Vector of (VectQuot (V,W)) by VECTSP10:23;

take y = y; :: thesis: S

thus S

A7: for v being Vector of V holds S

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

proof

let v be Vector of V; :: thesis: ( v in the Linear_Compl of W implies T . v = v + W )

assume v in the Linear_Compl of W ; :: thesis: T . v = v + W

hence T . v = ff . v by FUNCT_1:49

.= v + W by A7 ;

:: thesis: verum

end;assume v in the Linear_Compl of W ; :: thesis: T . v = v + W

hence T . v = ff . v by FUNCT_1:49

.= v + W by A7 ;

:: thesis: verum

now :: thesis: for a, b being Vector of the Linear_Compl of W holds T . (a + b) = (T . a) + (T . b)

then AD:
T is additive
;let a, b be Vector of the Linear_Compl of W; :: thesis: T . (a + b) = (T . a) + (T . b)

reconsider a1 = a, b1 = b as Vector of V by S1;

A91: ( a1 in the Linear_Compl of W & b1 in the Linear_Compl of W ) ;

a1 + b1 = a + b by VECTSP_4:13;

then A94: a1 + b1 in the Linear_Compl of W ;

A95: T . a = a1 + W by P1, A91;

A96: T . b = b1 + W by P1, A91;

thus T . (a + b) = T . (a1 + b1) by VECTSP_4:13

.= (a1 + b1) + W by A94, P1

.= (T . a) + (T . b) by A95, A96, VECTSP10:26 ; :: thesis: verum

end;reconsider a1 = a, b1 = b as Vector of V by S1;

A91: ( a1 in the Linear_Compl of W & b1 in the Linear_Compl of W ) ;

a1 + b1 = a + b by VECTSP_4:13;

then A94: a1 + b1 in the Linear_Compl of W ;

A95: T . a = a1 + W by P1, A91;

A96: T . b = b1 + W by P1, A91;

thus T . (a + b) = T . (a1 + b1) by VECTSP_4:13

.= (a1 + b1) + W by A94, P1

.= (T . a) + (T . b) by A95, A96, VECTSP10:26 ; :: thesis: verum

now :: thesis: for a being Vector of the Linear_Compl of W

for r being Element of K holds T . (r * a) = r * (T . a)

then
T is homogeneous
;for r being Element of K holds T . (r * a) = r * (T . a)

let a be Vector of the Linear_Compl of W; :: thesis: for r being Element of K holds T . (r * a) = r * (T . a)

let r be Element of K; :: thesis: T . (r * a) = r * (T . a)

reconsider a1 = a as Vector of V by S1;

A91: a1 in the Linear_Compl of W ;

r * a = r * a1 by VECTSP_4:14;

then A94: r * a1 in the Linear_Compl of W ;

A95: T . a = a1 + W by P1, A91;

thus T . (r * a) = T . (r * a1) by VECTSP_4:14

.= (r * a1) + W by A94, P1

.= r * (T . a) by A95, VECTSP10:25 ; :: thesis: verum

end;let r be Element of K; :: thesis: T . (r * a) = r * (T . a)

reconsider a1 = a as Vector of V by S1;

A91: a1 in the Linear_Compl of W ;

r * a = r * a1 by VECTSP_4:14;

then A94: r * a1 in the Linear_Compl of W ;

A95: T . a = a1 + W by P1, A91;

thus T . (r * a) = T . (r * a1) by VECTSP_4:14

.= (r * a1) + W by A94, P1

.= r * (T . a) by A95, VECTSP10:25 ; :: thesis: verum

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

then
rng T = the carrier of (VectQuot (V,W))
;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (VectQuot (V,W)) or y in rng T )

assume y in the carrier of (VectQuot (V,W)) ; :: thesis: 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; :: thesis: verum

end;assume y in the carrier of (VectQuot (V,W)) ; :: thesis: 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; :: thesis: verum

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

take
the Linear_Compl of W
; :: thesis: ex T being linear-transformation of the Linear_Compl of W,(VectQuot (V,W)) st
let x1, x2 be object ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum

end;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 ) ; :: thesis: 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; :: thesis: verum

( T is bijective & ( for v being Vector of V st v in the Linear_Compl of W holds

T . v = v + W ) )

take T ; :: thesis: ( 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; :: thesis: verum