let K be Field; for A, B being Matrix of K st width A = len B & width B <> 0 holds
(A * B) @ = (B @) * (A @)
let A, B be Matrix of K; ( width A = len B & width B <> 0 implies (A * B) @ = (B @) * (A @) )
assume that
A1:
width A = len B
and
A2:
width B <> 0
; (A * B) @ = (B @) * (A @)
A3:
len (B @) = width B
by MATRIX_0:def 6;
len (A @) = width A
by MATRIX_0:def 6;
then A4:
width (B @) = len (A @)
by A1, A2, MATRIX_0:54;
then A5:
width ((B @) * (A @)) = width (A @)
by Def4;
width (A * B) > 0
by A1, A2, Def4;
then A6: width ((A * B) @) =
len (A * B)
by MATRIX_0:54
.=
len A
by A1, Def4
;
A7:
width ((B @) * (A @)) = width (A @)
by A4, Def4;
A8: len ((B @) * (A @)) =
len (B @)
by A4, Def4
.=
width B
by MATRIX_0:def 6
;
A9:
len ((B @) * (A @)) = len (B @)
by A4, Def4;
A10:
now for i, j being Nat st [i,j] in Indices ((B @) * (A @)) holds
((B @) * (A @)) * (i,j) = ((A * B) @) * (i,j)let i,
j be
Nat;
( [i,j] in Indices ((B @) * (A @)) implies ((B @) * (A @)) * (b1,b2) = ((A * B) @) * (b1,b2) )assume A11:
[i,j] in Indices ((B @) * (A @))
;
((B @) * (A @)) * (b1,b2) = ((A * B) @) * (b1,b2)
dom ((B @) * (A @)) = dom (B @)
by A9, FINSEQ_3:29;
then A12:
[i,j] in [:(dom (B @)),(Seg (width (A @))):]
by A5, A11;
per cases
( width A = 0 or width A > 0 )
;
suppose
width A > 0
;
((B @) * (A @)) * (b1,b2) = ((A * B) @) * (b1,b2)then
width (A @) = len A
by MATRIX_0:54;
then
Seg (width (A @)) = dom A
by FINSEQ_1:def 3;
then A13:
j in dom A
by A12, ZFMISC_1:87;
then A14:
Col (
(A @),
j)
= Line (
A,
j)
by MATRIX_0:58;
j in Seg (len A)
by A13, FINSEQ_1:def 3;
then
j in Seg (len (A * B))
by A1, Def4;
then A15:
j in dom (A * B)
by FINSEQ_1:def 3;
Seg (width B) = dom (B @)
by A3, FINSEQ_1:def 3;
then A16:
i in Seg (width B)
by A12, ZFMISC_1:87;
then
i in Seg (width (A * B))
by A1, Def4;
then
[j,i] in [:(dom (A * B)),(Seg (width (A * B))):]
by A15, ZFMISC_1:87;
then A17:
[j,i] in Indices (A * B)
;
Line (
(B @),
i)
= Col (
B,
i)
by A16, MATRIX_0:59;
hence ((B @) * (A @)) * (
i,
j) =
(Col (B,i)) "*" (Line (A,j))
by A4, A11, A14, Def4
.=
(Line (A,j)) "*" (Col (B,i))
by FVSUM_1:90
.=
(A * B) * (
j,
i)
by A1, A17, Def4
.=
((A * B) @) * (
i,
j)
by A17, MATRIX_0:def 6
;
verum end; end; end;
A18:
width (A @) = len A
len ((A * B) @) =
width (A * B)
by MATRIX_0:def 6
.=
width B
by A1, Def4
;
hence
(A * B) @ = (B @) * (A @)
by A6, A8, A7, A10, A18, MATRIX_0:21; verum