let M be Matrix of COMPLEX; ( width M > 0 implies (M @) *' = (M *') @ )
assume A1:
width M > 0
; (M @) *' = (M *') @
width (M *') = width M
by Def1;
then A2: width ((M *') @) =
len (M *')
by A1, MATRIX_0:54
.=
len M
by Def1
;
A3:
width ((M @) *') = width (M @)
by Def1;
A4: len ((M @) *') =
len (M @)
by Def1
.=
width M
by MATRIX_0:def 6
;
A5: width ((M @) *') =
width (M @)
by Def1
.=
len M
by A1, MATRIX_0:54
;
A6:
len ((M @) *') = len (M @)
by Def1;
A7:
for i, j being Nat st [i,j] in Indices ((M @) *') holds
((M @) *') * (i,j) = ((M *') @) * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices ((M @) *') implies ((M @) *') * (i,j) = ((M *') @) * (i,j) )
assume A8:
[i,j] in Indices ((M @) *')
;
((M @) *') * (i,j) = ((M *') @) * (i,j)
then A9:
1
<= i
by Th1;
A10:
1
<= j
by A8, Th1;
A11:
j <= width (M @)
by A3, A8, Th1;
i <= len (M @)
by A6, A8, Th1;
then A12:
[i,j] in Indices (M @)
by A9, A10, A11, Th1;
then A13:
[j,i] in Indices M
by MATRIX_0:def 6;
j <= width ((M @) *')
by A8, Th1;
then A14:
j <= len (M *')
by A5, Def1;
i <= len ((M @) *')
by A8, Th1;
then A15:
i <= width (M *')
by A4, Def1;
A16:
1
<= i
by A8, Th1;
1
<= j
by A8, Th1;
then A17:
[j,i] in Indices (M *')
by A14, A16, A15, Th1;
((M @) *') * (
i,
j) =
((M @) * (i,j)) *'
by A12, Def1
.=
(M * (j,i)) *'
by A13, MATRIX_0:def 6
.=
(M *') * (
j,
i)
by A13, Def1
.=
((M *') @) * (
i,
j)
by A17, MATRIX_0:def 6
;
hence
((M @) *') * (
i,
j)
= ((M *') @) * (
i,
j)
;
verum
end;
len ((M *') @) =
width (M *')
by MATRIX_0:def 6
.=
width M
by Def1
;
hence
(M @) *' = (M *') @
by A4, A5, A2, A7, MATRIX_0:21; verum