let K be Ring; :: thesis: for V, U being VectSp of K

for f being linear-transformation of V,U ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st

( T = CQFunctional f & T is bijective )

let V, U be VectSp of K; :: thesis: for f being linear-transformation of V,U ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st

( T = CQFunctional f & T is bijective )

let f be linear-transformation of V,U; :: thesis: ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st

( T = CQFunctional f & T is bijective )

set T = CQFunctional f;

set Vq = VectQuot (V,(ker f));

Q0: the carrier of (im f) = [#] (im f)

.= f .: ([#] V) by RANKNULL:def 2

.= f .: (dom f) by FUNCT_2:def 1

.= rng f by RELAT_1:113 ;

Q1: for x being object holds

( x in rng (CQFunctional f) iff x in rng f )

the carrier of (VectQuot (V,(ker f))) = dom (CQFunctional f) by FUNCT_2:def 1;

then reconsider T = CQFunctional f as Function of the carrier of (VectQuot (V,(ker f))), the carrier of (im f) by FUNCT_2:2, P1;

A1: T is onto by Q0, Q1, TARSKI:2;

set Tq = CQFunctional f;

then reconsider T = T as linear-transformation of (VectQuot (V,(ker f))),(im f) by AD;

take T ; :: thesis: ( T = CQFunctional f & T is bijective )

thus ( T = CQFunctional f & T is bijective ) by A1; :: thesis: verum

for f being linear-transformation of V,U ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st

( T = CQFunctional f & T is bijective )

let V, U be VectSp of K; :: thesis: for f being linear-transformation of V,U ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st

( T = CQFunctional f & T is bijective )

let f be linear-transformation of V,U; :: thesis: ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st

( T = CQFunctional f & T is bijective )

set T = CQFunctional f;

set Vq = VectQuot (V,(ker f));

Q0: the carrier of (im f) = [#] (im f)

.= f .: ([#] V) by RANKNULL:def 2

.= f .: (dom f) by FUNCT_2:def 1

.= rng f by RELAT_1:113 ;

Q1: for x being object holds

( x in rng (CQFunctional f) iff x in rng f )

proof

then P1:
rng (CQFunctional f) = the carrier of (im f)
by Q0, TARSKI:2;
let x be object ; :: thesis: ( x in rng (CQFunctional f) iff x in rng f )

then consider a being object such that

Q12: ( a in dom f & x = f . a ) by FUNCT_1:def 3;

reconsider a = a as Vector of V by Q12;

reconsider z = a + (ker f) as Vector of (VectQuot (V,(ker f))) by VECTSP10:23;

(CQFunctional f) . z = f . a by Def12;

hence x in rng (CQFunctional f) by Q12, FUNCT_2:4; :: thesis: verum

end;hereby :: thesis: ( x in rng f implies x in rng (CQFunctional f) )

assume
x in rng f
; :: thesis: x in rng (CQFunctional f)assume
x in rng (CQFunctional f)
; :: thesis: x in rng f

then consider z being object such that

Q12: ( z in dom (CQFunctional f) & x = (CQFunctional f) . z ) by FUNCT_1:def 3;

reconsider z = z as Vector of (VectQuot (V,(ker f))) by Q12;

consider a being Vector of V such that

A14: z = a + (ker f) by VECTSP10:22;

(CQFunctional f) . z = f . a by A14, Def12;

hence x in rng f by Q12, FUNCT_2:4; :: thesis: verum

end;then consider z being object such that

Q12: ( z in dom (CQFunctional f) & x = (CQFunctional f) . z ) by FUNCT_1:def 3;

reconsider z = z as Vector of (VectQuot (V,(ker f))) by Q12;

consider a being Vector of V such that

A14: z = a + (ker f) by VECTSP10:22;

(CQFunctional f) . z = f . a by A14, Def12;

hence x in rng f by Q12, FUNCT_2:4; :: thesis: verum

then consider a being object such that

Q12: ( a in dom f & x = f . a ) by FUNCT_1:def 3;

reconsider a = a as Vector of V by Q12;

reconsider z = a + (ker f) as Vector of (VectQuot (V,(ker f))) by VECTSP10:23;

(CQFunctional f) . z = f . a by Def12;

hence x in rng (CQFunctional f) by Q12, FUNCT_2:4; :: thesis: verum

the carrier of (VectQuot (V,(ker f))) = dom (CQFunctional f) by FUNCT_2:def 1;

then reconsider T = CQFunctional f as Function of the carrier of (VectQuot (V,(ker f))), the carrier of (im f) by FUNCT_2:2, P1;

A1: T is onto by Q0, Q1, TARSKI:2;

set Tq = CQFunctional f;

now :: thesis: for A, B being Vector of (VectQuot (V,(ker f))) holds T . (A + B) = (T . A) + (T . B)

then AD:
T is additive
;let A, B be Vector of (VectQuot (V,(ker f))); :: thesis: T . (A + B) = (T . A) + (T . B)

thus T . (A + B) = ((CQFunctional f) . A) + ((CQFunctional f) . B) by VECTSP_1:def 20

.= (T . A) + (T . B) by VECTSP_4:13 ; :: thesis: verum

end;thus T . (A + B) = ((CQFunctional f) . A) + ((CQFunctional f) . B) by VECTSP_1:def 20

.= (T . A) + (T . B) by VECTSP_4:13 ; :: thesis: verum

now :: thesis: for A being Vector of (VectQuot (V,(ker f)))

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 (VectQuot (V,(ker f))); :: 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)

thus T . (r * A) = r * ((CQFunctional f) . A) by MOD_2:def 2

.= r * (T . A) by VECTSP_4:14 ; :: thesis: verum

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

thus T . (r * A) = r * ((CQFunctional f) . A) by MOD_2:def 2

.= r * (T . A) by VECTSP_4:14 ; :: thesis: verum

then reconsider T = T as linear-transformation of (VectQuot (V,(ker f))),(im f) by AD;

take T ; :: thesis: ( T = CQFunctional f & T is bijective )

thus ( T = CQFunctional f & T is bijective ) by A1; :: thesis: verum