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