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 being Nat st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) ) ) )
assume A1:
width M1 = len M2
; ( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i being Nat st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) ) )
hereby ( len M = len M1 & width M = width M2 & ( for i being Nat st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) implies M = M1 * M2 )
assume A2:
M = M1 * M2
;
( len M = len M1 & width M = width M2 & ( for i being Nat st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) )hence A3:
(
len M = len M1 &
width M = width M2 )
by A1, Th39;
for i being Nat st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2thus
for
i being
Nat st
i in Seg (len M) holds
Line (
M,
i)
= (Line (M1,i)) * M2
verumproof
let i be
Nat;
( i in Seg (len M) implies Line (M,i) = (Line (M1,i)) * M2 )
assume A4:
i in Seg (len M)
;
Line (M,i) = (Line (M1,i)) * M2
A5:
len (Line (M1,i)) = len M2
by A1, MATRIX_0:def 7;
then A6:
len ((Line (M1,i)) * M2) = width M2
by MATRIXR1:62;
len (Line (M,i)) = width M
by MATRIX_0:def 7;
then A7:
dom (Line (M,i)) =
Seg (width M2)
by A3, FINSEQ_1:def 3
.=
dom ((Line (M1,i)) * M2)
by A6, FINSEQ_1:def 3
;
A8:
i in dom M
by A4, FINSEQ_1:def 3;
for
j being
Nat st
j in dom (Line (M,i)) holds
(Line (M,i)) . j = ((Line (M1,i)) * M2) . j
proof
let j be
Nat;
( j in dom (Line (M,i)) implies (Line (M,i)) . j = ((Line (M1,i)) * M2) . j )
assume A9:
j in dom (Line (M,i))
;
(Line (M,i)) . j = ((Line (M1,i)) * M2) . j
A10:
j in Seg (len ((Line (M1,i)) * M2))
by A7, A9, FINSEQ_1:def 3;
j in Seg (len (Line (M,i)))
by A9, FINSEQ_1:def 3;
then
j in Seg (width M)
by MATRIX_0:def 7;
then A11:
[i,j] in Indices M
by A4, Th12;
A12:
(M . i) . j in REAL
by XREAL_0:def 1;
thus (Line (M,i)) . j =
(M . i) . j
by A8, MATRIX_0:60
.=
M * (
i,
j)
by A11, MATRIX_0:def 5, A12
.=
(Line (M1,i)) "*" (Col (M2,j))
by A1, A2, A11, Th39
.=
((Line (M1,i)) * M2) . j
by A5, A10, Th40
;
verum
end;
hence
Line (
M,
i)
= (Line (M1,i)) * M2
by A7, FINSEQ_1:13;
verum
end;
end;
assume that
A13:
len M = len M1
and
A14:
width M = width M2
and
A15:
for i being Nat st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2
; M = M1 * M2
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))
proof
let i,
j be
Nat;
( [i,j] in Indices M implies M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) )
assume A16:
[i,j] in Indices M
;
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))
A17:
i in Seg (len M)
by A16, Th12;
then A18:
i in dom M
by FINSEQ_1:def 3;
A19:
len (Line (M1,i)) = len M2
by A1, MATRIX_0:def 7;
j in Seg (width M)
by A16, Th12;
then A20:
j in Seg (len ((Line (M1,i)) * M2))
by A14, A19, MATRIXR1:62;
(M . i) . j in REAL
by XREAL_0:def 1;
hence M * (
i,
j) =
(M . i) . j
by A16, MATRIX_0:def 5
.=
(Line (M,i)) . j
by A18, MATRIX_0:60
.=
((Line (M1,i)) * M2) . j
by A15, A17
.=
(Line (M1,i)) "*" (Col (M2,j))
by A19, A20, Th40
;
verum
end;
hence
M = M1 * M2
by A1, A13, A14, Th39; verum