let n be Element of 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_1:25;
A2:
( width A = n & len B = n )
by MATRIX_1:25;
A3:
len (A * B) = n
by MATRIX_1:25;
A4:
width B = n
by MATRIX_1:25;
A5:
len (B @ ) = n
by MATRIX_1:25;
then A6:
len ((B @ ) * (A @ )) = len (B @ )
by MATRIX_1:25;
A7: width (B @ ) =
n
by MATRIX_1:25
.=
len (A @ )
by MATRIX_1:25
;
A8:
width (A * B) = n
by MATRIX_1:25;
A9:
width (A @ ) = n
by MATRIX_1:25;
then A10:
width ((B @ ) * (A @ )) = width (A @ )
by MATRIX_1:25;
A11:
now 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_1:25;
assume A13:
[i,j] in Indices ((A * B) @ )
;
((B @ ) * (A @ )) * i,j = ((A * B) @ ) * i,jthen
j in Seg (len (A * B))
by A3, A12, ZFMISC_1:106;
then A14:
j in dom (A * B)
by FINSEQ_1:def 3;
i in Seg (width (A * B))
by A8, A13, A12, ZFMISC_1:106;
then A15:
[j,i] in Indices (A * B)
by A14, ZFMISC_1:106;
Seg (width (A @ )) = dom A
by A1, A9, FINSEQ_1:def 3;
then
j in dom A
by A9, A13, A12, ZFMISC_1:106;
then A16:
Col (A @ ),
j = Line A,
j
by MATRIX_2:16;
reconsider i0 =
i,
j0 =
j as
Element of
NAT by ORDINAL1:def 13;
A17:
Seg (width B) = dom (B @ )
by A4, A5, FINSEQ_1:def 3;
A18:
Indices ((B @ ) * (A @ )) = [:(Seg n),(Seg n):]
by MATRIX_1:25;
then
[i,j] in [:(dom (B @ )),(Seg (width (A @ ))):]
by A6, A10, A13, A12, FINSEQ_3:31;
then
i in Seg (width B)
by A17, ZFMISC_1:106;
then
Line (B @ ),
i = Col B,
i
by MATRIX_2:17;
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_1:def 7
;
verum end;
A19:
( len ((B @ ) * (A @ )) = n & width ((B @ ) * (A @ )) = n )
by MATRIX_1:25;
( len ((A * B) @ ) = n & width ((A * B) @ ) = n )
by MATRIX_1:25;
hence
(A * B) @ = (B @ ) * (A @ )
by A19, A11, MATRIX_1:21; verum