let K be Field; for V1, V2, V3 being finite-dimensional VectSp of K
for f being linear-transformation of V1,V2
for g being linear-transformation of V2,V3 st g | (im f) is one-to-one holds
( rank (g * f) = rank f & nullity (g * f) = nullity f )
let V1, V2, V3 be finite-dimensional VectSp of K; for f being linear-transformation of V1,V2
for g being linear-transformation of V2,V3 st g | (im f) is one-to-one holds
( rank (g * f) = rank f & nullity (g * f) = nullity f )
let f be linear-transformation of V1,V2; for g being linear-transformation of V2,V3 st g | (im f) is one-to-one holds
( rank (g * f) = rank f & nullity (g * f) = nullity f )
let g be linear-transformation of V2,V3; ( g | (im f) is one-to-one implies ( rank (g * f) = rank f & nullity (g * f) = nullity f ) )
assume A1:
g | (im f) is one-to-one
; ( rank (g * f) = rank f & nullity (g * f) = nullity f )
the carrier of (im (g * f)) =
[#] (im (g * f))
.=
(g * f) .: ([#] V1)
by RANKNULL:def 2
.=
((g | (im f)) * f) .: ([#] V1)
by Lm8
.=
(g | (im f)) .: (f .: ([#] V1))
by RELAT_1:126
.=
(g | (im f)) .: ([#] (im f))
by RANKNULL:def 2
.=
[#] (im (g | (im f)))
by RANKNULL:def 2
.=
the carrier of (im (g | (im f)))
;
then A2: rank (g * f) =
rank (g | (im f))
by VECTSP_4:29
.=
rank f
by A1, RANKNULL:45
;
(nullity f) + (rank f) =
dim V1
by RANKNULL:44
.=
(nullity (g * f)) + (rank (g * f))
by RANKNULL:44
;
hence
( rank (g * f) = rank f & nullity (g * f) = nullity f )
by A2; verum