let m, l, n be Nat; for S being Matrix of l,m,INT.Ring
for T being Matrix of m,n,INT.Ring
for S1 being Matrix of l,m,F_Real
for T1 being Matrix of m,n,F_Real st S = S1 & T = T1 & 0 < l & 0 < m holds
S * T = S1 * T1
let S be Matrix of l,m,INT.Ring; for T being Matrix of m,n,INT.Ring
for S1 being Matrix of l,m,F_Real
for T1 being Matrix of m,n,F_Real st S = S1 & T = T1 & 0 < l & 0 < m holds
S * T = S1 * T1
let T be Matrix of m,n,INT.Ring; for S1 being Matrix of l,m,F_Real
for T1 being Matrix of m,n,F_Real st S = S1 & T = T1 & 0 < l & 0 < m holds
S * T = S1 * T1
let S1 be Matrix of l,m,F_Real; for T1 being Matrix of m,n,F_Real st S = S1 & T = T1 & 0 < l & 0 < m holds
S * T = S1 * T1
let T1 be Matrix of m,n,F_Real; ( S = S1 & T = T1 & 0 < l & 0 < m implies S * T = S1 * T1 )
assume AS:
( S = S1 & T = T1 & 0 < l & 0 < m )
; S * T = S1 * T1
P1:
( len S = l & width S = m & Indices S = [:(Seg l),(Seg m):] )
by MATRIX_0:23, AS;
Q1:
( len S1 = l & width S1 = m & Indices S1 = [:(Seg l),(Seg m):] )
by MATRIX_0:23, AS;
P2:
( len T = m & width T = n & Indices T = [:(Seg m),(Seg n):] )
by MATRIX_0:23, AS;
Q2:
( len T1 = m & width T1 = n & Indices T1 = [:(Seg m),(Seg n):] )
by MATRIX_0:23, AS;
P3:
( len (S * T) = len S & width (S * T) = width T )
by P1, P2, MATRIX_3:def 4;
Q3:
( len (S1 * T1) = len S1 & width (S1 * T1) = width T1 )
by Q1, Q2, MATRIX_3:def 4;
reconsider ST = S * T as Matrix of l,n,INT.Ring by P3, AS, P1, P2, MATRIX_0:20;
reconsider S1T1 = S1 * T1 as Matrix of l,n,F_Real by Q3, AS, Q1, Q2, MATRIX_0:20;
for i, j being Nat st [i,j] in Indices ST holds
ST * (i,j) = S1T1 * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices ST implies ST * (i,j) = S1T1 * (i,j) )
assume A1:
[i,j] in Indices ST
;
ST * (i,j) = S1T1 * (i,j)
A2:
Indices ST =
[:(Seg (len ST)),(Seg (width ST)):]
by FINSEQ_1:def 3
.=
Indices S1T1
by AS, P3, Q3, FINSEQ_1:def 3
;
i in dom ST
by A1, ZFMISC_1:87;
then
i in Seg (len ST)
by FINSEQ_1:def 3;
then
i in dom S
by FINSEQ_1:def 3, P3;
then X1:
Line (
S,
i)
= Line (
S1,
i)
by ZMATRLIN:2, AS;
j in Seg (width T)
by A1, P3, ZFMISC_1:87;
then X2:
Col (
T,
j)
= Col (
T1,
j)
by ZMATRLIN:3, AS;
thus ST * (
i,
j) =
(Line (S,i)) "*" (Col (T,j))
by A1, P1, P2, MATRIX_3:def 4
.=
(Line (S1,i)) "*" (Col (T1,j))
by X1, X2, ZMATRLIN:37
.=
S1T1 * (
i,
j)
by A1, A2, Q1, Q2, MATRIX_3:def 4
;
verum
end;
hence
S * T = S1 * T1
by AS, P3, Q3, ZMATRLIN:4; verum