let K be Field; for V1, V2, V3 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for B3 being FinSequence of V3
for A being Matrix of len b1, len b2,K
for B being Matrix of len b2, len B3,K st width A = len B holds
for AB being Matrix of len b1, len B3,K st AB = A * B holds
Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))
let V1, V2, V3 be finite-dimensional VectSp of K; for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for B3 being FinSequence of V3
for A being Matrix of len b1, len b2,K
for B being Matrix of len b2, len B3,K st width A = len B holds
for AB being Matrix of len b1, len B3,K st AB = A * B holds
Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))
let b1 be OrdBasis of V1; for b2 being OrdBasis of V2
for B3 being FinSequence of V3
for A being Matrix of len b1, len b2,K
for B being Matrix of len b2, len B3,K st width A = len B holds
for AB being Matrix of len b1, len B3,K st AB = A * B holds
Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))
let b2 be OrdBasis of V2; for B3 being FinSequence of V3
for A being Matrix of len b1, len b2,K
for B being Matrix of len b2, len B3,K st width A = len B holds
for AB being Matrix of len b1, len B3,K st AB = A * B holds
Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))
let B3 be FinSequence of V3; for A being Matrix of len b1, len b2,K
for B being Matrix of len b2, len B3,K st width A = len B holds
for AB being Matrix of len b1, len B3,K st AB = A * B holds
Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))
let A be Matrix of len b1, len b2,K; for B being Matrix of len b2, len B3,K st width A = len B holds
for AB being Matrix of len b1, len B3,K st AB = A * B holds
Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))
let B be Matrix of len b2, len B3,K; ( width A = len B implies for AB being Matrix of len b1, len B3,K st AB = A * B holds
Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2)) )
assume A1:
width A = len B
; for AB being Matrix of len b1, len B3,K st AB = A * B holds
Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))
set MB = Mx2Tran (B,b2,B3);
set MA = Mx2Tran (A,b1,b2);
let AB be Matrix of len b1, len B3,K; ( AB = A * B implies Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2)) )
assume A2:
AB = A * B
; Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))
set MAB = Mx2Tran (AB,b1,B3);
now for x being object st x in the carrier of V1 holds
((Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))) . x = (Mx2Tran (AB,b1,B3)) . xlet x be
object ;
( x in the carrier of V1 implies ((Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))) . x = (Mx2Tran (AB,b1,B3)) . x )assume
x in the
carrier of
V1
;
((Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))) . x = (Mx2Tran (AB,b1,B3)) . xthen reconsider v =
x as
Element of
V1 ;
set L =
LineVec2Mx (v |-- b1);
A3:
len A = len b1
by MATRIX_0:def 2;
A4:
(
width (LineVec2Mx (v |-- b1)) = len (v |-- b1) &
len (v |-- b1) = len b1 )
by MATRIX_0:23, MATRLIN:def 7;
then
(
len (LineVec2Mx (v |-- b1)) = 1 &
len ((LineVec2Mx (v |-- b1)) * A) = len (LineVec2Mx (v |-- b1)) )
by A3, MATRIX_0:23, MATRIX_3:def 4;
then A5:
dom ((LineVec2Mx (v |-- b1)) * A) = Seg 1
by FINSEQ_1:def 3;
A6:
width ((LineVec2Mx (v |-- b1)) * A) = width A
by A4, A3, MATRIX_3:def 4;
then A7:
(
len B = len b2 &
len (Line (((LineVec2Mx (v |-- b1)) * A),1)) = width A )
by CARD_1:def 7, MATRIX_0:def 2;
A8:
1
in Seg 1
;
dom ((Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))) = the
carrier of
V1
by FUNCT_2:def 1;
hence ((Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))) . x =
(Mx2Tran (B,b2,B3)) . ((Mx2Tran (A,b1,b2)) . v)
by FUNCT_1:12
.=
(Mx2Tran (B,b2,B3)) . (Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),b2)))
by Def3
.=
Sum (lmlt ((Line (((LineVec2Mx ((Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),b2))) |-- b2)) * B),1)),B3))
by Def3
.=
Sum (lmlt ((Line (((LineVec2Mx (Line (((LineVec2Mx (v |-- b1)) * A),1))) * B),1)),B3))
by A1, A7, MATRLIN:36
.=
Sum (lmlt ((Line ((LineVec2Mx (Line ((((LineVec2Mx (v |-- b1)) * A) * B),1))),1)),B3))
by A1, A6, A5, A8, Th35
.=
Sum (lmlt ((Line ((LineVec2Mx (Line (((LineVec2Mx (v |-- b1)) * AB),1))),1)),B3))
by A1, A2, A4, A3, MATRIX_3:33
.=
Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * AB),1)),B3))
by MATRIX15:25
.=
(Mx2Tran (AB,b1,B3)) . x
by Def3
;
verum end;
hence
Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))
by FUNCT_2:12; verum