let n be Element of NAT ; :: thesis: for A, B being Matrix of n, REAL holds (A * B) @ = (B @ ) * (A @ )
let A, B be Matrix of n, REAL ; :: thesis: (A * B) @ = (B @ ) * (A @ )
A1:
( len A = n & width A = n )
by MATRIX_1:25;
A2:
( len B = n & width B = n )
by MATRIX_1:25;
A3:
( len (A @ ) = n & width (A @ ) = n )
by MATRIX_1:25;
A4:
( len (B @ ) = n & len (B @ ) = n )
by MATRIX_1:25;
A5:
( len (A * B) = n & width (A * B) = n )
by MATRIX_1:25;
A6:
( len ((A * B) @ ) = n & width ((A * B) @ ) = n )
by MATRIX_1:25;
A7: width (B @ ) =
n
by MATRIX_1:25
.=
len (A @ )
by MATRIX_1:25
;
A8:
( len ((B @ ) * (A @ )) = n & width ((B @ ) * (A @ )) = n )
by MATRIX_1:25;
A9:
( len ((B @ ) * (A @ )) = len (B @ ) & width ((B @ ) * (A @ )) = width (A @ ) )
by A3, A4, MATRIX_1:25;
now let i,
j be
Nat;
:: thesis: ( [i,j] in Indices ((A * B) @ ) implies ((B @ ) * (A @ )) * i,j = ((A * B) @ ) * i,j )assume A10:
[i,j] in Indices ((A * B) @ )
;
:: thesis: ((B @ ) * (A @ )) * i,j = ((A * B) @ ) * i,jA11:
Indices ((A * B) @ ) = [:(Seg n),(Seg n):]
by MATRIX_1:25;
A12:
Indices ((B @ ) * (A @ )) = [:(Seg n),(Seg n):]
by MATRIX_1:25;
reconsider i0 =
i,
j0 =
j as
Element of
NAT by ORDINAL1:def 13;
A13:
[i,j] in [:(dom (B @ )),(Seg (width (A @ ))):]
by A9, A10, A11, A12, FINSEQ_3:31;
(
Seg (width B) = dom (B @ ) &
Seg (width (A @ )) = dom A )
by A1, A2, A3, A4, FINSEQ_1:def 3;
then A14:
(
i in Seg (width B) &
j in dom A )
by A13, ZFMISC_1:106;
then A15:
(
Line (B @ ),
i = Col B,
i &
Col (A @ ),
j = Line A,
j )
by MATRIX_2:16, MATRIX_2:17;
j in Seg (len (A * B))
by A1, A5, A14, FINSEQ_1:def 3;
then A16:
j in dom (A * B)
by FINSEQ_1:def 3;
i in Seg (width (A * B))
by A5, A10, A11, ZFMISC_1:106;
then A17:
[j,i] in Indices (A * B)
by A16, ZFMISC_1:106;
thus ((B @ ) * (A @ )) * i,
j =
(Col B,i0) "*" (Line A,j0)
by A7, A10, A11, A12, A15, MATRPROB:39
.=
(A * B) * j0,
i0
by A1, A2, A17, MATRPROB:39
.=
((A * B) @ ) * i,
j
by A17, MATRIX_1:def 7
;
:: thesis: verum end;
hence
(A * B) @ = (B @ ) * (A @ )
by A6, A8, MATRIX_1:21; :: thesis: verum