let V, W be RealLinearSpace; :: thesis: for L being LinearOperator of V,W ex QL being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st

( QL is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

let L be LinearOperator of V,W; :: thesis: ex QL being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st

( QL is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

A1: the carrier of (Im L) = rng L by IMX2, LCL1;

A2: the carrier of (Ker L) = L " {(0. W)} by KLXY1, LCL1;

defpred S_{1}[ object , object ] means ex v being VECTOR of V st

( $1 = v + (Ker L) & $2 = L . v );

A3: for x being Element of the carrier of (VectQuot (V,(Ker L))) ex y being Element of the carrier of (Im L) st S_{1}[x,y]

A5: for x being Element of (VectQuot (V,(Ker L))) holds S_{1}[x,QL . x]
from FUNCT_2:sch 3(A3);

A6: for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v

x1 = x2

ex s being object st

( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s )

A18: for v, w being Element of (VectQuot (V,(Ker L))) holds QL . (v + w) = (QL . v) + (QL . w)

for r being Real holds QL . (r * v) = r * (QL . v)

then reconsider QL = QL as LinearOperator of (VectQuot (V,(Ker L))),(Im L) ;

take QL ; :: thesis: ( QL is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

thus QL is isomorphism by A11, A17, FUNCT_2:19; :: thesis: for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v

thus for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v by A6; :: thesis: verum

( QL is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

let L be LinearOperator of V,W; :: thesis: ex QL being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st

( QL is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

A1: the carrier of (Im L) = rng L by IMX2, LCL1;

A2: the carrier of (Ker L) = L " {(0. W)} by KLXY1, LCL1;

defpred S

( $1 = v + (Ker L) & $2 = L . v );

A3: for x being Element of the carrier of (VectQuot (V,(Ker L))) ex y being Element of the carrier of (Im L) st S

proof

consider QL being Function of the carrier of (VectQuot (V,(Ker L))), the carrier of (Im L) such that
let x be Element of the carrier of (VectQuot (V,(Ker L))); :: thesis: ex y being Element of the carrier of (Im L) st S_{1}[x,y]

consider v being Point of V such that

A4: x = v + (Ker L) by LMQ07;

reconsider y = L . v as Element of the carrier of (Im L) by A1, FUNCT_2:4;

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

thus S_{1}[x,y]
by A4; :: thesis: verum

end;consider v being Point of V such that

A4: x = v + (Ker L) by LMQ07;

reconsider y = L . v as Element of the carrier of (Im L) by A1, FUNCT_2:4;

take y ; :: thesis: S

thus S

A5: for x being Element of (VectQuot (V,(Ker L))) holds S

A6: for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v

proof

A11:
for x1, x2 being object st x1 in the carrier of (VectQuot (V,(Ker L))) & x2 in the carrier of (VectQuot (V,(Ker L))) & QL . x1 = QL . x2 holds
let z be Point of (VectQuot (V,(Ker L))); :: thesis: for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v

let v be VECTOR of V; :: thesis: ( z = v + (Ker L) implies QL . z = L . v )

assume A7: z = v + (Ker L) ; :: thesis: QL . z = L . v

consider w being VECTOR of V such that

A8: ( z = w + (Ker L) & QL . z = L . w ) by A5;

consider v1 being Point of V such that

A9: ( v1 in Ker L & w = v + v1 ) by A7, A8, RLSUB_1:54, RLSUB_1:63;

w - v = v1 + (v - v) by A9, RLVECT_1:28

.= v1 + (0. V) by RLVECT_1:15

.= v1 by RLVECT_1:4 ;

then A10: ( w - v in the carrier of V & L . (w - v) in {(0. W)} ) by A2, A9, FUNCT_2:38;

L . (w - v) = L . (w + ((- 1) * v)) by RLVECT_1:16

.= (L . w) + (L . ((- 1) * v)) by VECTSP_1:def 20

.= (L . w) + ((- 1) * (L . v)) by LOPBAN_1:def 5

.= (L . w) + (- (L . v)) by RLVECT_1:16 ;

then (L . w) - (L . v) = 0. W by A10, TARSKI:def 1;

then L . v = ((L . w) - (L . v)) + (L . v) by RLVECT_1:4

.= (L . w) - ((L . v) - (L . v)) by RLVECT_1:29

.= (L . w) - (0. W) by RLVECT_1:15

.= L . w by RLVECT_1:13 ;

hence QL . z = L . v by A8; :: thesis: verum

end;QL . z = L . v

let v be VECTOR of V; :: thesis: ( z = v + (Ker L) implies QL . z = L . v )

assume A7: z = v + (Ker L) ; :: thesis: QL . z = L . v

consider w being VECTOR of V such that

A8: ( z = w + (Ker L) & QL . z = L . w ) by A5;

consider v1 being Point of V such that

A9: ( v1 in Ker L & w = v + v1 ) by A7, A8, RLSUB_1:54, RLSUB_1:63;

w - v = v1 + (v - v) by A9, RLVECT_1:28

.= v1 + (0. V) by RLVECT_1:15

.= v1 by RLVECT_1:4 ;

then A10: ( w - v in the carrier of V & L . (w - v) in {(0. W)} ) by A2, A9, FUNCT_2:38;

L . (w - v) = L . (w + ((- 1) * v)) by RLVECT_1:16

.= (L . w) + (L . ((- 1) * v)) by VECTSP_1:def 20

.= (L . w) + ((- 1) * (L . v)) by LOPBAN_1:def 5

.= (L . w) + (- (L . v)) by RLVECT_1:16 ;

then (L . w) - (L . v) = 0. W by A10, TARSKI:def 1;

then L . v = ((L . w) - (L . v)) + (L . v) by RLVECT_1:4

.= (L . w) - ((L . v) - (L . v)) by RLVECT_1:29

.= (L . w) - (0. W) by RLVECT_1:15

.= L . w by RLVECT_1:13 ;

hence QL . z = L . v by A8; :: thesis: verum

x1 = x2

proof

for v being object st v in the carrier of (Im L) holds
let x1, x2 be object ; :: thesis: ( x1 in the carrier of (VectQuot (V,(Ker L))) & x2 in the carrier of (VectQuot (V,(Ker L))) & QL . x1 = QL . x2 implies x1 = x2 )

assume A12: ( x1 in the carrier of (VectQuot (V,(Ker L))) & x2 in the carrier of (VectQuot (V,(Ker L))) & QL . x1 = QL . x2 ) ; :: thesis: x1 = x2

reconsider z1 = x1, z2 = x2 as Point of (VectQuot (V,(Ker L))) by A12;

consider v1 being VECTOR of V such that

A13: ( z1 = v1 + (Ker L) & QL . x1 = L . v1 ) by A5;

consider v2 being VECTOR of V such that

A14: ( z2 = v2 + (Ker L) & QL . x2 = L . v2 ) by A5;

(L . v1) - (L . v2) = (L . v1) + ((- 1) * (L . v2)) by RLVECT_1:16

.= (L . v1) + (L . ((- 1) * v2)) by LOPBAN_1:def 5

.= L . (v1 + ((- 1) * v2)) by VECTSP_1:def 20

.= L . (v1 - v2) by RLVECT_1:16 ;

then L . (v1 - v2) = 0. W by A12, A13, A14, RLVECT_1:15;

then L . (v1 - v2) in {(0. W)} by TARSKI:def 1;

then A15: v1 - v2 in Ker L by A2, FUNCT_2:38;

(v1 - v2) + v2 = v1 - (v2 - v2) by RLVECT_1:29

.= v1 - (0. V) by RLVECT_1:15

.= v1 by RLVECT_1:13 ;

then v1 in v2 + (Ker L) by A15;

hence x1 = x2 by A13, A14, RLSUB_1:54; :: thesis: verum

end;assume A12: ( x1 in the carrier of (VectQuot (V,(Ker L))) & x2 in the carrier of (VectQuot (V,(Ker L))) & QL . x1 = QL . x2 ) ; :: thesis: x1 = x2

reconsider z1 = x1, z2 = x2 as Point of (VectQuot (V,(Ker L))) by A12;

consider v1 being VECTOR of V such that

A13: ( z1 = v1 + (Ker L) & QL . x1 = L . v1 ) by A5;

consider v2 being VECTOR of V such that

A14: ( z2 = v2 + (Ker L) & QL . x2 = L . v2 ) by A5;

(L . v1) - (L . v2) = (L . v1) + ((- 1) * (L . v2)) by RLVECT_1:16

.= (L . v1) + (L . ((- 1) * v2)) by LOPBAN_1:def 5

.= L . (v1 + ((- 1) * v2)) by VECTSP_1:def 20

.= L . (v1 - v2) by RLVECT_1:16 ;

then L . (v1 - v2) = 0. W by A12, A13, A14, RLVECT_1:15;

then L . (v1 - v2) in {(0. W)} by TARSKI:def 1;

then A15: v1 - v2 in Ker L by A2, FUNCT_2:38;

(v1 - v2) + v2 = v1 - (v2 - v2) by RLVECT_1:29

.= v1 - (0. V) by RLVECT_1:15

.= v1 by RLVECT_1:13 ;

then v1 in v2 + (Ker L) by A15;

hence x1 = x2 by A13, A14, RLSUB_1:54; :: thesis: verum

ex s being object st

( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s )

proof

then A17:
QL is onto
by FUNCT_2:10;
let v be object ; :: thesis: ( v in the carrier of (Im L) implies ex s being object st

( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s ) )

assume v in the carrier of (Im L) ; :: thesis: ex s being object st

( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s )

then v in rng L by IMX2, LCL1;

then consider x being object such that

A16: ( x in the carrier of V & L . x = v ) by FUNCT_2:11;

reconsider x = x as Point of V by A16;

reconsider s = x + (Ker L) as Point of (VectQuot (V,(Ker L))) by LMQ07;

take s ; :: thesis: ( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s )

thus ( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s ) by A6, A16; :: thesis: verum

end;( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s ) )

assume v in the carrier of (Im L) ; :: thesis: ex s being object st

( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s )

then v in rng L by IMX2, LCL1;

then consider x being object such that

A16: ( x in the carrier of V & L . x = v ) by FUNCT_2:11;

reconsider x = x as Point of V by A16;

reconsider s = x + (Ker L) as Point of (VectQuot (V,(Ker L))) by LMQ07;

take s ; :: thesis: ( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s )

thus ( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s ) by A6, A16; :: thesis: verum

A18: for v, w being Element of (VectQuot (V,(Ker L))) holds QL . (v + w) = (QL . v) + (QL . w)

proof

for v being VECTOR of (VectQuot (V,(Ker L)))
let v, w be Element of (VectQuot (V,(Ker L))); :: thesis: QL . (v + w) = (QL . v) + (QL . w)

consider x being Point of V such that

A19: v = x + (Ker L) by LMQ07;

consider y being Point of V such that

A20: w = y + (Ker L) by LMQ07;

A21: v + w = (x + y) + (Ker L) by A19, A20, LMQ11;

A22: QL . v = L . x by A6, A19;

A23: QL . w = L . y by A6, A20;

thus QL . (v + w) = L . (x + y) by A6, A21

.= (L . x) + (L . y) by VECTSP_1:def 20

.= (QL . v) + (QL . w) by A22, A23, RLSUB_1:13 ; :: thesis: verum

end;consider x being Point of V such that

A19: v = x + (Ker L) by LMQ07;

consider y being Point of V such that

A20: w = y + (Ker L) by LMQ07;

A21: v + w = (x + y) + (Ker L) by A19, A20, LMQ11;

A22: QL . v = L . x by A6, A19;

A23: QL . w = L . y by A6, A20;

thus QL . (v + w) = L . (x + y) by A6, A21

.= (L . x) + (L . y) by VECTSP_1:def 20

.= (QL . v) + (QL . w) by A22, A23, RLSUB_1:13 ; :: thesis: verum

for r being Real holds QL . (r * v) = r * (QL . v)

proof

then
( QL is additive & QL is homogeneous )
by A18, LOPBAN_1:def 5;
let v be VECTOR of (VectQuot (V,(Ker L))); :: thesis: for r being Real holds QL . (r * v) = r * (QL . v)

let r be Real; :: thesis: QL . (r * v) = r * (QL . v)

consider x being Point of V such that

A24: v = x + (Ker L) by LMQ07;

r * v = (r * x) + (Ker L) by A24, LMQ09;

hence QL . (r * v) = L . (r * x) by A6

.= r * (L . x) by LOPBAN_1:def 5

.= r * (QL . v) by A6, A24, RLSUB_1:14 ;

:: thesis: verum

end;let r be Real; :: thesis: QL . (r * v) = r * (QL . v)

consider x being Point of V such that

A24: v = x + (Ker L) by LMQ07;

r * v = (r * x) + (Ker L) by A24, LMQ09;

hence QL . (r * v) = L . (r * x) by A6

.= r * (L . x) by LOPBAN_1:def 5

.= r * (QL . v) by A6, A24, RLSUB_1:14 ;

:: thesis: verum

then reconsider QL = QL as LinearOperator of (VectQuot (V,(Ker L))),(Im L) ;

take QL ; :: thesis: ( QL is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

thus QL is isomorphism by A11, A17, FUNCT_2:19; :: thesis: for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v

thus for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v by A6; :: thesis: verum