let K be Field; for V1, V2 being finite-dimensional VectSp of K
for f1, f2 being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))
let V1, V2 be finite-dimensional VectSp of K; for f1, f2 being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))
let f1, f2 be Function of V1,V2; for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))
let b1 be OrdBasis of V1; for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))
let b2 be OrdBasis of V2; AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))
A1: len (AutMt ((f1 + f2),b1,b2)) =
len b1
by Def8
.=
len (AutMt (f1,b1,b2))
by Def8
;
then A2:
dom (AutMt ((f1 + f2),b1,b2)) = dom (AutMt (f1,b1,b2))
by FINSEQ_3:29;
A3:
width (AutMt (f1,b1,b2)) = width (AutMt (f2,b1,b2))
A6:
width (AutMt ((f1 + f2),b1,b2)) = width (AutMt (f1,b1,b2))
then A9:
width (AutMt ((f1 + f2),b1,b2)) = width ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)))
by MATRIX_3:def 3;
len (AutMt (f1,b1,b2)) =
len b1
by Def8
.=
len (AutMt (f2,b1,b2))
by Def8
;
then A10:
dom (AutMt (f1,b1,b2)) = dom (AutMt (f2,b1,b2))
by FINSEQ_3:29;
A11:
for i, j being Nat st [i,j] in Indices (AutMt ((f1 + f2),b1,b2)) holds
(AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices (AutMt ((f1 + f2),b1,b2)) implies (AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) * (i,j) )
assume A12:
[i,j] in Indices (AutMt ((f1 + f2),b1,b2))
;
(AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) * (i,j)
then A13:
[i,j] in [:(dom (AutMt ((f1 + f2),b1,b2))),(Seg (width (AutMt ((f1 + f2),b1,b2)))):]
by MATRIX_0:def 4;
then A14:
[i,j] in Indices (AutMt (f1,b1,b2))
by A2, A6, MATRIX_0:def 4;
A15:
[i,j] in Indices (AutMt (f2,b1,b2))
by A10, A3, A2, A6, A13, MATRIX_0:def 4;
(AutMt ((f1 + f2),b1,b2)) * (
i,
j)
= ((AutMt (f1,b1,b2)) * (i,j)) + ((AutMt (f2,b1,b2)) * (i,j))
proof
consider KL3 being
Linear_Combination of
V2 such that A16:
(
f2 . (b1 /. i) = Sum KL3 &
Carrier KL3 c= rng b2 )
and A17:
for
t being
Nat st 1
<= t &
t <= len ((f2 . (b1 /. i)) |-- b2) holds
((f2 . (b1 /. i)) |-- b2) /. t = KL3 . (b2 /. t)
by Def7;
consider KL2 being
Linear_Combination of
V2 such that A18:
(
f1 . (b1 /. i) = Sum KL2 &
Carrier KL2 c= rng b2 )
and A19:
for
t being
Nat st 1
<= t &
t <= len ((f1 . (b1 /. i)) |-- b2) holds
((f1 . (b1 /. i)) |-- b2) /. t = KL2 . (b2 /. t)
by Def7;
A20:
i in dom (AutMt ((f1 + f2),b1,b2))
by A13, ZFMISC_1:87;
then A21:
i in dom b1
by Lm3;
reconsider b4 =
rng b2 as
Basis of
V2 by Def2;
consider p1 being
FinSequence of
K such that A22:
p1 = (AutMt ((f1 + f2),b1,b2)) . i
and A23:
(AutMt ((f1 + f2),b1,b2)) * (
i,
j)
= p1 . j
by A12, MATRIX_0:def 5;
consider KL1 being
Linear_Combination of
V2 such that A24:
(
(f1 + f2) . (b1 /. i) = Sum KL1 &
Carrier KL1 c= rng b2 )
and A25:
for
t being
Nat st 1
<= t &
t <= len (((f1 + f2) . (b1 /. i)) |-- b2) holds
(((f1 + f2) . (b1 /. i)) |-- b2) /. t = KL1 . (b2 /. t)
by Def7;
(
b4 is
linearly-independent &
(f1 + f2) . (b1 /. i) = (f1 . (b1 /. i)) + (f2 . (b1 /. i)) )
by Def3, VECTSP_7:def 3;
then A26:
KL1 . (b2 /. j) =
(KL2 + KL3) . (b2 /. j)
by A24, A18, A16, Th6
.=
(KL2 . (b2 /. j)) + (KL3 . (b2 /. j))
by VECTSP_6:22
;
A27:
p1 =
(AutMt ((f1 + f2),b1,b2)) /. i
by A22, A20, PARTFUN1:def 6
.=
((f1 + f2) . (b1 /. i)) |-- b2
by A21, Def8
;
consider p3 being
FinSequence of
K such that A28:
p3 = (AutMt (f2,b1,b2)) . i
and A29:
(AutMt (f2,b1,b2)) * (
i,
j)
= p3 . j
by A15, MATRIX_0:def 5;
consider p2 being
FinSequence of
K such that A30:
p2 = (AutMt (f1,b1,b2)) . i
and A31:
(AutMt (f1,b1,b2)) * (
i,
j)
= p2 . j
by A14, MATRIX_0:def 5;
A32:
j in Seg (width (AutMt ((f1 + f2),b1,b2)))
by A13, ZFMISC_1:87;
then A33:
1
<= j
by FINSEQ_1:1;
len b1 = len (AutMt ((f1 + f2),b1,b2))
by Def8;
then
dom b1 = dom (AutMt ((f1 + f2),b1,b2))
by FINSEQ_3:29;
then
dom b1 <> {}
by A13, ZFMISC_1:87;
then
Seg (len b1) <> {}
by FINSEQ_1:def 3;
then
len b1 > 0
;
then A34:
j in Seg (len b2)
by A32, Th39;
then A35:
j <= len b2
by FINSEQ_1:1;
then
j <= len (((f1 + f2) . (b1 /. i)) |-- b2)
by Def7;
then A36:
p1 /. j = KL1 . (b2 /. j)
by A33, A27, A25;
A37:
j in dom b2
by A34, FINSEQ_1:def 3;
i in dom (AutMt (f2,b1,b2))
by A21, Lm3;
then A38:
p3 =
(AutMt (f2,b1,b2)) /. i
by A28, PARTFUN1:def 6
.=
(f2 . (b1 /. i)) |-- b2
by A21, Def8
;
then
j in dom p3
by A37, Lm1;
then A39:
(AutMt (f2,b1,b2)) * (
i,
j)
= p3 /. j
by A29, PARTFUN1:def 6;
i in dom (AutMt (f1,b1,b2))
by A21, Lm3;
then A40:
p2 =
(AutMt (f1,b1,b2)) /. i
by A30, PARTFUN1:def 6
.=
(f1 . (b1 /. i)) |-- b2
by A21, Def8
;
then
j in dom p2
by A37, Lm1;
then A41:
(AutMt (f1,b1,b2)) * (
i,
j)
= p2 /. j
by A31, PARTFUN1:def 6;
j <= len ((f2 . (b1 /. i)) |-- b2)
by A35, Def7;
then A42:
p3 /. j = KL3 . (b2 /. j)
by A33, A38, A17;
j <= len ((f1 . (b1 /. i)) |-- b2)
by A35, Def7;
then A43:
p2 /. j = KL2 . (b2 /. j)
by A33, A40, A19;
j in dom p1
by A37, A27, Lm1;
hence
(AutMt ((f1 + f2),b1,b2)) * (
i,
j)
= ((AutMt (f1,b1,b2)) * (i,j)) + ((AutMt (f2,b1,b2)) * (i,j))
by A23, A41, A39, A36, A43, A42, A26, PARTFUN1:def 6;
verum
end;
hence
(AutMt ((f1 + f2),b1,b2)) * (
i,
j)
= ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) * (
i,
j)
by A14, MATRIX_3:def 3;
verum
end;
len (AutMt ((f1 + f2),b1,b2)) = len ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)))
by A1, MATRIX_3:def 3;
hence
AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))
by A9, A11, MATRIX_0:21; verum