let M, M1, M2 be Matrix of REAL; ( width M1 = len M2 implies ( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) ) ) )
assume A1:
width M1 = len M2
; ( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) ) )
set MM = MXR2MXF M;
set M4 = MXR2MXF M2;
set M3 = MXR2MXF M1;
A2:
MXR2MXF M1 = M1
by MATRIXR1:def 1;
A3:
MXR2MXF M2 = M2
by MATRIXR1:def 1;
MXF2MXR ((MXR2MXF M1) * (MXR2MXF M2)) = M1 * M2
by MATRIXR1:def 6;
then A4:
(MXR2MXF M1) * (MXR2MXF M2) = M1 * M2
by MATRIXR1:def 2;
hereby ( len M = len M1 & width M = width M2 & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) implies M = M1 * M2 )
assume A5:
M = M1 * M2
;
( len M = len M1 & width M = width M2 & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) )hence A6:
len M = len M1
by A1, A2, A3, A4, MATRIX_3:def 4;
( width M = width M2 & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) )thus A7:
width M = width M2
by A1, A2, A3, A4, A5, MATRIX_3:def 4;
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))thus
for
i,
j being
Nat st
[i,j] in Indices M holds
M * (
i,
j)
= (Line (M1,i)) "*" (Col (M2,j))
verumproof
let i,
j be
Nat;
( [i,j] in Indices M implies M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) )
assume A8:
[i,j] in Indices M
;
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))
j in Seg (width M2)
by A7, A8, Th12;
then A9:
Col (
(MXR2MXF M2),
j)
= Col (
M2,
j)
by A3, Th17;
i in Seg (len M1)
by A6, A8, Th12;
then
i in dom M1
by FINSEQ_1:def 3;
then A10:
Line (
(MXR2MXF M1),
i)
= Line (
M1,
i)
by A2, Th16;
A11:
len (Line (M1,i)) =
width M1
by MATRIX_0:def 7
.=
len (Col (M2,j))
by A1, MATRIX_0:def 8
;
M = MXF2MXR ((MXR2MXF M1) * (MXR2MXF M2))
by A5, MATRIXR1:def 6;
then
(
[i,j] in Indices ((MXR2MXF M1) * (MXR2MXF M2)) &
M * (
i,
j)
= ((MXR2MXF M1) * (MXR2MXF M2)) * (
i,
j) )
by A8, MATRIXR1:23, MATRIXR1:def 2;
hence M * (
i,
j) =
(Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j))
by A1, A2, A3, MATRIX_3:def 4
.=
(Line (M1,i)) "*" (Col (M2,j))
by A10, A9, A11, Th38
;
verum
end;
end;
assume that
A12:
len M = len M1
and
A13:
width M = width M2
and
A14:
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))
; M = M1 * M2
A15: width (MXR2MXF M) =
width M
by MATRIXR1:def 1
.=
width (MXR2MXF M2)
by A13, MATRIXR1:def 1
;
A16: len (MXR2MXF M) =
len M
by MATRIXR1:def 1
.=
len (MXR2MXF M1)
by A12, MATRIXR1:def 1
;
for i, j being Nat st [i,j] in Indices (MXR2MXF M) holds
(MXR2MXF M) * (i,j) = (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j))
proof
let i,
j be
Nat;
( [i,j] in Indices (MXR2MXF M) implies (MXR2MXF M) * (i,j) = (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j)) )
assume A17:
[i,j] in Indices (MXR2MXF M)
;
(MXR2MXF M) * (i,j) = (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j))
j in Seg (width (MXR2MXF M2))
by A15, A17, Th12;
then A18:
Col (
(MXR2MXF M2),
j)
= Col (
M2,
j)
by Th17, MATRIXR1:def 1;
i in Seg (len (MXR2MXF M1))
by A16, A17, Th12;
then
i in dom (MXR2MXF M1)
by FINSEQ_1:def 3;
then A19:
Line (
(MXR2MXF M1),
i)
= Line (
M1,
i)
by Th16, MATRIXR1:def 1;
A20:
len (Line (M1,i)) =
width M1
by MATRIX_0:def 7
.=
len (Col (M2,j))
by A1, MATRIX_0:def 8
;
(
[i,j] in Indices M &
(MXR2MXF M) * (
i,
j)
= M * (
i,
j) )
by A17, MATRIXR1:23, MATRIXR1:def 1;
hence (MXR2MXF M) * (
i,
j) =
(Line (M1,i)) "*" (Col (M2,j))
by A14
.=
(Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j))
by A19, A18, A20, Th38
;
verum
end;
then
( MXR2MXF M = M & MXR2MXF M = (MXR2MXF M1) * (MXR2MXF M2) )
by A1, A2, A3, A16, A15, MATRIXR1:def 1, MATRIX_3:def 4;
then
M = MXF2MXR ((MXR2MXF M1) * (MXR2MXF M2))
by MATRIXR1:def 2;
hence
M = M1 * M2
by MATRIXR1:def 6; verum