let M, M1, M2 be Matrix of REAL ; :: thesis: ( width M1 = len M2 & width M1 > 0 & width M2 > 0 implies ( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line M,i = (Line M1,i) * M2 ) ) ) )
assume A1:
( width M1 = len M2 & width M1 > 0 & width M2 > 0 )
; :: thesis: ( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line M,i = (Line M1,i) * M2 ) ) )
hereby :: thesis: ( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line M,i = (Line M1,i) * M2 ) implies M = M1 * M2 )
assume A2:
M = M1 * M2
;
:: thesis: ( len M = len M1 & width M = width M2 & ( for i being Element of 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;
:: thesis: for i being Element of NAT st i in Seg (len M) holds
Line M,i = (Line M1,i) * M2thus
for
i being
Element of
NAT st
i in Seg (len M) holds
Line M,
i = (Line M1,i) * M2
:: thesis: verumproof
let i be
Element of
NAT ;
:: thesis: ( i in Seg (len M) implies Line M,i = (Line M1,i) * M2 )
assume A4:
i in Seg (len M)
;
:: thesis: Line M,i = (Line M1,i) * M2
A5:
i in dom M
by A4, FINSEQ_1:def 3;
A6:
len (Line M,i) = width M
by MATRIX_1:def 8;
A7:
len (Line M1,i) = len M2
by A1, MATRIX_1:def 8;
then A8:
len ((Line M1,i) * M2) = width M2
by MATRIXR1:62;
A9:
dom (Line M,i) =
Seg (width M2)
by A3, A6, FINSEQ_1:def 3
.=
dom ((Line M1,i) * M2)
by A8, 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;
:: thesis: ( j in dom (Line M,i) implies (Line M,i) . j = ((Line M1,i) * M2) . j )
assume A10:
j in dom (Line M,i)
;
:: thesis: (Line M,i) . j = ((Line M1,i) * M2) . j
j in Seg (len (Line M,i))
by A10, FINSEQ_1:def 3;
then
j in Seg (width M)
by MATRIX_1:def 8;
then A11:
[i,j] in Indices M
by A4, Th12;
A12:
j in Seg (len ((Line M1,i) * M2))
by A9, A10, FINSEQ_1:def 3;
thus (Line M,i) . j =
(M . i) . j
by A5, MATRIX_2:18
.=
M * i,
j
by A11, MATRIX_1:def 6
.=
(Line M1,i) "*" (Col M2,j)
by A1, A2, A10, A11, Th39
.=
((Line M1,i) * M2) . j
by A7, A12, Th40
;
:: thesis: verum
end;
hence
Line M,
i = (Line M1,i) * M2
by A9, FINSEQ_1:17;
:: thesis: verum
end;
end;
assume A13:
( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line M,i = (Line M1,i) * M2 ) )
; :: thesis: M = M1 * M2
for i, j being Element of NAT st [i,j] in Indices M holds
M * i,j = (Line M1,i) "*" (Col M2,j)
proof
let i,
j be
Element of
NAT ;
:: thesis: ( [i,j] in Indices M implies M * i,j = (Line M1,i) "*" (Col M2,j) )
assume A14:
[i,j] in Indices M
;
:: thesis: M * i,j = (Line M1,i) "*" (Col M2,j)
A15:
(
i in Seg (len M) &
j in Seg (width M) )
by A14, Th12;
then A16:
i in dom M
by FINSEQ_1:def 3;
A17:
len (Line M1,i) = len M2
by A1, MATRIX_1:def 8;
then A18:
j in Seg (len ((Line M1,i) * M2))
by A13, A15, MATRIXR1:62;
thus M * i,
j =
(M . i) . j
by A14, MATRIX_1:def 6
.=
(Line M,i) . j
by A16, MATRIX_2:18
.=
((Line M1,i) * M2) . j
by A13, A15
.=
(Line M1,i) "*" (Col M2,j)
by A17, A18, Th40
;
:: thesis: verum
end;
hence
M = M1 * M2
by A1, A13, Th39; :: thesis: verum