let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K
for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1
for L being Scalar of K
for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
let f be linear-transformation of V1,V1; :: thesis: for L being Scalar of K
for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
let L be Scalar of K; :: thesis: for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
set V = V1;
set fi = f + ((- L) * (id V1));
let I be Linear_Compl of UnionKers (f + ((- L) * (id V1))); :: thesis: for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
let fI be linear-transformation of I,I; :: thesis: ( fI = f | I implies for v being Vector of I st fI . v = L * v holds
v = 0. V1 )
assume A1: fI = f | I ; :: thesis: for v being Vector of I st fI . v = L * v holds
v = 0. V1
let v be Vector of I; :: thesis: ( fI . v = L * v implies v = 0. V1 )
assume A2: fI . v = L * v ; :: thesis: v = 0. V1
reconsider v1 = v as Vector of V1 by VECTSP_4:10;
A3: f . v = fI . v by A1, FUNCT_1:49
.= L * v1 by A2, VECTSP_4:14 ;
((f + ((- L) * (id V1))) | I) . v1 = (f + ((- L) * (id V1))) . v1 by FUNCT_1:49
.= (f . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def 3
.= (f . v1) + ((- L) * ((id V1) . v1)) by MATRLIN:def 4
.= (L * v1) + ((- L) * v1) by A3
.= (L + (- L)) * v1 by VECTSP_1:def 15
.= (0. K) * v1 by VECTSP_1:19
.= 0. V1 by VECTSP_1:14 ;
then A4: v1 in ker ((f + ((- L) * (id V1))) | I) by RANKNULL:10;
(f + ((- L) * (id V1))) | I is one-to-one by Th36;
then ker ((f + ((- L) * (id V1))) | I) = (0). I by MATRLIN2:43;
hence v = 0. I by A4, VECTSP_4:35
.= 0. V1 by VECTSP_4:11 ;
:: thesis: verum