let V1, V2, V3 be free finite-rank Z_Module; for f being Function of V1,V2
for g being Function of V2,V3
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds
AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))
let f be Function of V1,V2; for g being Function of V2,V3
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds
AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))
let g be Function of V2,V3; for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds
AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))
let b1 be OrdBasis of V1; for b2 being OrdBasis of V2
for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds
AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))
let b2 be OrdBasis of V2; for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds
AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))
let b3 be OrdBasis of V3; ( g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 implies AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) )
assume A1:
( g is additive & g is homogeneous )
; ( not len b1 > 0 or not len b2 > 0 or AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) )
assume that
A2:
len b1 > 0
and
A3:
len b2 > 0
; AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))
A4: width (AutMt (f,b1,b2)) =
len b2
by A2, Th39
.=
len (AutMt (g,b2,b3))
by Def8
;
A5: width (AutMt ((g * f),b1,b3)) =
len b3
by A2, Th39
.=
width (AutMt (g,b2,b3))
by A3, Th39
;
A6:
width (AutMt ((g * f),b1,b3)) = width ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3)))
by A5, A4, MATRIX_3:def 4;
A7: len (AutMt ((g * f),b1,b3)) =
len b1
by Def8
.=
len (AutMt (f,b1,b2))
by Def8
.=
len ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3)))
by A4, MATRIX_3:def 4
;
for i, j being Nat st [i,j] in Indices (AutMt ((g * f),b1,b3)) holds
(AutMt ((g * f),b1,b3)) * (i,j) = ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices (AutMt ((g * f),b1,b3)) implies (AutMt ((g * f),b1,b3)) * (i,j) = ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) * (i,j) )
deffunc H1(
Nat)
-> Element of the
carrier of
INT.Ring =
((g . (b2 /. $1)) |-- b3) /. j;
consider d being
FinSequence of
INT.Ring such that A9:
(
len d = len b2 & ( for
k being
Nat st
k in dom d holds
d . k = H1(
k) ) )
from FINSEQ_2:sch 1();
assume A10:
[i,j] in Indices (AutMt ((g * f),b1,b3))
;
(AutMt ((g * f),b1,b3)) * (i,j) = ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) * (i,j)
then A12:
j in Seg (width (AutMt ((g * f),b1,b3)))
by ZFMISC_1:87;
A13:
len (Col ((AutMt (g,b2,b3)),j)) =
len (AutMt (g,b2,b3))
by MATRIX_0:def 8
.=
len d
by A9, Def8
;
A14:
dom d = Seg (len b2)
by A9, FINSEQ_1:def 3;
A15:
[i,j] in Indices ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3)))
by A6, A7, A10, FINSEQ_3:29;
A16:
i in dom (AutMt ((g * f),b1,b3))
by A10, ZFMISC_1:87;
A17:
width (AutMt ((g * f),b1,b3)) <> {}
by A10;
len b1 = len (AutMt ((g * f),b1,b3))
by Def8;
then
len b1 > 0
by A17, MATRIX_0:def 3;
then A18:
j in Seg (len b3)
by A12, Th39;
then A19:
j in dom b3
by FINSEQ_1:def 3;
A20:
now for k being Nat st 1 <= k & k <= len d holds
(Col ((AutMt (g,b2,b3)),j)) . k = d . klet k be
Nat;
( 1 <= k & k <= len d implies (Col ((AutMt (g,b2,b3)),j)) . k = d . k )assume A21:
( 1
<= k &
k <= len d )
;
(Col ((AutMt (g,b2,b3)),j)) . k = d . kA23:
k in dom b2
by A9, A21, FINSEQ_3:25;
A24:
len (AutMt (g,b2,b3)) = len b2
by Def8;
then A25:
k in dom (AutMt (g,b2,b3))
by A9, A21, FINSEQ_3:25;
j in Seg (width (AutMt (g,b2,b3)))
by A5, A10, ZFMISC_1:87;
then
[k,j] in Indices (AutMt (g,b2,b3))
by A25, ZFMISC_1:87;
then consider p2 being
FinSequence of
INT such that A26:
p2 = (AutMt (g,b2,b3)) . k
and A27:
(AutMt (g,b2,b3)) * (
k,
j)
= p2 . j
by MATRIX_0:def 5;
A28:
p2 =
(AutMt (g,b2,b3)) /. k
by A25, A26, PARTFUN1:def 6
.=
(g . (b2 /. k)) |-- b3
by A23, Def8
;
then
j in Seg (len p2)
by A18, Def7;
then A29:
j in dom p2
by FINSEQ_1:def 3;
k in dom (AutMt (g,b2,b3))
by A9, A21, A24, FINSEQ_3:25;
hence (Col ((AutMt (g,b2,b3)),j)) . k =
p2 . j
by A27, MATRIX_0:def 8
.=
((g . (b2 /. k)) |-- b3) /. j
by A28, A29, PARTFUN1:def 6
.=
d . k
by A9, A21, FINSEQ_3:25
;
verum end;
b1 /. i in the
carrier of
V1
;
then A30:
b1 /. i in dom f
by FUNCT_2:def 1;
consider p1 being
FinSequence of
INT such that A31:
p1 = (AutMt ((g * f),b1,b3)) . i
and A32:
(AutMt ((g * f),b1,b3)) * (
i,
j)
= p1 . j
by A10, MATRIX_0:def 5;
A33:
len ((f . (b1 /. i)) |-- b2) = len b2
by Def7;
A34:
len (AutMt ((g * f),b1,b3)) = len b1
by Def8;
then A35:
i in dom b1
by A16, FINSEQ_3:29;
A36:
p1 =
(AutMt ((g * f),b1,b3)) /. i
by A16, A31, PARTFUN1:def 6
.=
((g * f) . (b1 /. i)) |-- b3
by A35, Def8
;
len (AutMt (f,b1,b2)) = len b1
by Def8;
then A37:
i in dom (AutMt (f,b1,b2))
by A16, A34, FINSEQ_3:29;
then A38:
Line (
(AutMt (f,b1,b2)),
i) =
(AutMt (f,b1,b2)) . i
by MATRIX_0:60
.=
(AutMt (f,b1,b2)) /. i
by A37, PARTFUN1:def 6
.=
(f . (b1 /. i)) |-- b2
by A35, Def8
;
A39:
Seg (len b2) = dom b2
by FINSEQ_1:def 3;
j in Seg (len (((g * f) . (b1 /. i)) |-- b3))
by A18, Def7;
then A40:
j in dom p1
by A36, FINSEQ_1:def 3;
thus (AutMt ((g * f),b1,b3)) * (
i,
j) =
(((g * f) . (b1 /. i)) |-- b3) /. j
by A32, A36, A40, PARTFUN1:def 6
.=
((g . (f . (b1 /. i))) |-- b3) /. j
by A30, FUNCT_1:13
.=
((g . (Sum (lmlt (((f . (b1 /. i)) |-- b2),b2)))) |-- b3) /. j
by Th35
.=
((Sum (lmlt (((f . (b1 /. i)) |-- b2),(g * b2)))) |-- b3) /. j
by A1, A33, Th18
.=
Sum (mlt (((f . (b1 /. i)) |-- b2),d))
by A3, A19, A9, A14, A39, A33, Th37
.=
(Line ((AutMt (f,b1,b2)),i)) "*" (Col ((AutMt (g,b2,b3)),j))
by A38, A13, A20, FINSEQ_1:14
.=
((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) * (
i,
j)
by A4, A15, MATRIX_3:def 4
;
verum
end;
hence
AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))
by A7, A6, MATRIX_0:21; verum