let n be Nat; for A, B being Matrix of n,REAL holds (A * B) @ = (B @) * (A @)
let A, B be Matrix of n,REAL; (A * B) @ = (B @) * (A @)
A1:
len A = n
by MATRIX_0:24;
A2:
( width A = n & len B = n )
by MATRIX_0:24;
A3:
len (A * B) = n
by MATRIX_0:24;
A4:
width B = n
by MATRIX_0:24;
A5:
len (B @) = n
by MATRIX_0:24;
then A6:
len ((B @) * (A @)) = len (B @)
by MATRIX_0:24;
A7: width (B @) =
n
by MATRIX_0:24
.=
len (A @)
by MATRIX_0:24
;
A8:
width (A * B) = n
by MATRIX_0:24;
A9:
width (A @) = n
by MATRIX_0:24;
then A10:
width ((B @) * (A @)) = width (A @)
by MATRIX_0:24;
A11:
now for i, j being Nat st [i,j] in Indices ((A * B) @) holds
((B @) * (A @)) * (i,j) = ((A * B) @) * (i,j)let i,
j be
Nat;
( [i,j] in Indices ((A * B) @) implies ((B @) * (A @)) * (i,j) = ((A * B) @) * (i,j) )A12:
Indices ((A * B) @) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
assume A13:
[i,j] in Indices ((A * B) @)
;
((B @) * (A @)) * (i,j) = ((A * B) @) * (i,j)then
j in Seg (len (A * B))
by A3, A12, ZFMISC_1:87;
then A14:
j in dom (A * B)
by FINSEQ_1:def 3;
i in Seg (width (A * B))
by A8, A13, A12, ZFMISC_1:87;
then A15:
[j,i] in Indices (A * B)
by A14, ZFMISC_1:87;
Seg (width (A @)) = dom A
by A1, A9, FINSEQ_1:def 3;
then
j in dom A
by A9, A13, A12, ZFMISC_1:87;
then A16:
Col (
(A @),
j)
= Line (
A,
j)
by MATRIX_0:58;
reconsider i0 =
i,
j0 =
j as
Nat ;
A17:
Seg (width B) = dom (B @)
by A4, A5, FINSEQ_1:def 3;
A18:
Indices ((B @) * (A @)) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then
[i,j] in [:(dom (B @)),(Seg (width (A @))):]
by A6, A10, A13, A12, FINSEQ_3:29;
then
i in Seg (width B)
by A17, ZFMISC_1:87;
then
Line (
(B @),
i)
= Col (
B,
i)
by MATRIX_0:59;
hence ((B @) * (A @)) * (
i,
j) =
(Col (B,i0)) "*" (Line (A,j0))
by A7, A13, A12, A18, A16, MATRPROB:39
.=
(A * B) * (
j0,
i0)
by A2, A15, MATRPROB:39
.=
((A * B) @) * (
i,
j)
by A15, MATRIX_0:def 6
;
verum end;
A19:
( len ((B @) * (A @)) = n & width ((B @) * (A @)) = n )
by MATRIX_0:24;
( len ((A * B) @) = n & width ((A * B) @) = n )
by MATRIX_0:24;
hence
(A * B) @ = (B @) * (A @)
by A19, A11, MATRIX_0:21; verum