let L be Field; :: thesis: for m, n, k being Element of NAT st m > 0 & n > 0 holds
for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2)
let m, n, k be Element of NAT ; :: thesis: ( m > 0 & n > 0 implies for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2) )
assume A1:
( m > 0 & n > 0 )
; :: thesis: for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2)
let M1 be Matrix of m,n,L; :: thesis: for M2 being Matrix of n,k,L holds ((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2)
let M2 be Matrix of n,k,L; :: thesis: ((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2)
A2:
width ((emb m,L) * M1) = len M2
A3: width M1 =
n
by A1, MATRIX_1:24
.=
len M2
by A1, MATRIX_1:24
;
A4: len (((emb m,L) * M1) * M2) =
len ((emb m,L) * M1)
by A2, MATRIX_3:def 4
.=
len M1
by MATRIX_3:def 5
;
A5: len ((emb m,L) * (M1 * M2)) =
len (M1 * M2)
by MATRIX_3:def 5
.=
len M1
by A3, MATRIX_3:def 4
;
width ((emb m,L) * (M1 * M2)) =
width (M1 * M2)
by MATRIX_3:def 5
.=
width M2
by A3, MATRIX_3:def 4
;
then A6:
width (((emb m,L) * M1) * M2) = width ((emb m,L) * (M1 * M2))
by A2, MATRIX_3:def 4;
for i, j being Nat st [i,j] in Indices (((emb m,L) * M1) * M2) holds
(((emb m,L) * M1) * M2) * i,j = ((emb m,L) * (M1 * M2)) * i,j
proof
let i,
j be
Nat;
:: thesis: ( [i,j] in Indices (((emb m,L) * M1) * M2) implies (((emb m,L) * M1) * M2) * i,j = ((emb m,L) * (M1 * M2)) * i,j )
assume A7:
[i,j] in Indices (((emb m,L) * M1) * M2)
;
:: thesis: (((emb m,L) * M1) * M2) * i,j = ((emb m,L) * (M1 * M2)) * i,j
A8:
len (((emb m,L) * M1) * M2) =
len ((emb m,L) * M1)
by A2, MATRIX_3:def 4
.=
len M1
by MATRIX_3:def 5
;
A9:
len M1 = len (M1 * M2)
by A3, MATRIX_3:def 4;
A10:
[i,j] in Indices (M1 * M2)
then A12:
((emb m,L) * (M1 * M2)) * i,
j =
(emb m,L) * ((M1 * M2) * i,j)
by MATRIX_3:def 5
.=
(emb m,L) * ((Line M1,i) "*" (Col M2,j))
by A3, A10, MATRIX_3:def 4
.=
(emb m,L) * (Sum (mlt (Line M1,i),(Col M2,j)))
by FVSUM_1:def 10
;
A13:
(((emb m,L) * M1) * M2) * i,
j =
(Line ((emb m,L) * M1),i) "*" (Col M2,j)
by A2, A7, MATRIX_3:def 4
.=
Sum (mlt (Line ((emb m,L) * M1),i),(Col M2,j))
by FVSUM_1:def 10
;
(emb m,L) * (Sum (mlt (Line M1,i),(Col M2,j))) = Sum (mlt (Line ((emb m,L) * M1),i),(Col M2,j))
proof
(emb m,L) * (mlt (Line M1,i),(Col M2,j)) = mlt (Line ((emb m,L) * M1),i),
(Col M2,j)
proof
A14:
Line ((emb m,L) * M1),
i = (emb m,L) * (Line M1,i)
proof
A15:
dom (Line ((emb m,L) * M1),i) = dom ((emb m,L) * (Line M1,i))
proof
len (Line ((emb m,L) * M1),i) =
width ((emb m,L) * M1)
by MATRIX_1:def 8
.=
width M1
by MATRIX_3:def 5
;
then A16:
dom (Line ((emb m,L) * M1),i) = Seg (width M1)
by FINSEQ_1:def 3;
Seg (len ((emb m,L) * (Line M1,i))) =
dom ((emb m,L) * (Line M1,i))
by FINSEQ_1:def 3
.=
dom (Line M1,i)
by POLYNOM1:def 2
.=
Seg (len (Line M1,i))
by FINSEQ_1:def 3
;
then len ((emb m,L) * (Line M1,i)) =
len (Line M1,i)
by FINSEQ_1:8
.=
width M1
by MATRIX_1:def 8
;
hence
dom (Line ((emb m,L) * M1),i) = dom ((emb m,L) * (Line M1,i))
by A16, FINSEQ_1:def 3;
:: thesis: verum
end;
for
k being
Nat st
k in dom (Line ((emb m,L) * M1),i) holds
(Line ((emb m,L) * M1),i) . k = ((emb m,L) * (Line M1,i)) . k
proof
let k be
Nat;
:: thesis: ( k in dom (Line ((emb m,L) * M1),i) implies (Line ((emb m,L) * M1),i) . k = ((emb m,L) * (Line M1,i)) . k )
assume A17:
k in dom (Line ((emb m,L) * M1),i)
;
:: thesis: (Line ((emb m,L) * M1),i) . k = ((emb m,L) * (Line M1,i)) . k
A18:
len (Line ((emb m,L) * M1),i) =
width ((emb m,L) * M1)
by MATRIX_1:def 8
.=
width M1
by MATRIX_3:def 5
;
then
dom (Line ((emb m,L) * M1),i) = Seg (width M1)
by FINSEQ_1:def 3;
then A19:
k in Seg (width ((emb m,L) * M1))
by A17, MATRIX_3:def 5;
A20:
k in Seg (width M1)
by A17, A18, FINSEQ_1:def 3;
len (Line M1,i) = width M1
by MATRIX_1:def 8;
then
k in dom (Line M1,i)
by A20, FINSEQ_1:def 3;
then
(Line M1,i) . k = (Line M1,i) /. k
by PARTFUN1:def 8;
then reconsider a =
(Line M1,i) . k as
Element of
L ;
A21:
((emb m,L) * (Line M1,i)) . k = (emb m,L) * a
by A15, A17, FVSUM_1:62;
A22:
[i,k] in Indices M1
proof
A23:
Indices M1 = [:(Seg m),(Seg n):]
by A1, MATRIX_1:24;
A24:
i in dom (M1 * M2)
by A10, ZFMISC_1:106;
len (M1 * M2) =
len M1
by A3, MATRIX_3:def 4
.=
m
by A1, MATRIX_1:24
;
then A25:
dom (M1 * M2) = Seg m
by FINSEQ_1:def 3;
k in Seg n
by A1, A20, MATRIX_1:24;
hence
[i,k] in Indices M1
by A23, A24, A25, ZFMISC_1:106;
:: thesis: verum
end;
a = M1 * i,
k
by A20, MATRIX_1:def 8;
then
(emb m,L) * a = ((emb m,L) * M1) * i,
k
by A22, MATRIX_3:def 5;
hence
(Line ((emb m,L) * M1),i) . k = ((emb m,L) * (Line M1,i)) . k
by A19, A21, MATRIX_1:def 8;
:: thesis: verum
end;
hence
Line ((emb m,L) * M1),
i = (emb m,L) * (Line M1,i)
by A15, FINSEQ_1:17;
:: thesis: verum
end;
(emb m,L) * (mlt (Line M1,i),(Col M2,j)) = mlt ((emb m,L) * (Line M1,i)),
(Col M2,j)
proof
A26:
dom (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) = dom ((emb m,L) * (mlt (Line M1,i),(Col M2,j)))
proof
Seg (len ((emb m,L) * (Line M1,i))) =
dom ((emb m,L) * (Line M1,i))
by FINSEQ_1:def 3
.=
dom (Line M1,i)
by POLYNOM1:def 2
.=
Seg (len (Line M1,i))
by FINSEQ_1:def 3
;
then A27:
len ((emb m,L) * (Line M1,i)) =
len (Line M1,i)
by FINSEQ_1:8
.=
len M2
by A3, MATRIX_1:def 8
.=
len (Col M2,j)
by MATRIX_1:def 9
;
A28:
dom ((emb m,L) * (Line M1,i)) =
Seg (len ((emb m,L) * (Line M1,i)))
by FINSEQ_1:def 3
.=
Seg (len (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)))
by A27, MATRIX_3:8
.=
dom (mlt ((emb m,L) * (Line M1,i)),(Col M2,j))
by FINSEQ_1:def 3
;
A29:
len (Line M1,i) =
len M2
by A3, MATRIX_1:def 8
.=
len (Col M2,j)
by MATRIX_1:def 9
;
dom ((emb m,L) * (Line M1,i)) =
dom (Line M1,i)
by POLYNOM1:def 2
.=
Seg (len (Line M1,i))
by FINSEQ_1:def 3
.=
Seg (len (mlt (Line M1,i),(Col M2,j)))
by A29, MATRIX_3:8
.=
dom (mlt (Line M1,i),(Col M2,j))
by FINSEQ_1:def 3
;
hence
dom (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) = dom ((emb m,L) * (mlt (Line M1,i),(Col M2,j)))
by A28, POLYNOM1:def 2;
:: thesis: verum
end;
for
k being
Nat st
k in dom (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) holds
(mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) . k = ((emb m,L) * (mlt (Line M1,i),(Col M2,j))) . k
proof
let k be
Nat;
:: thesis: ( k in dom (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) implies (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) . k = ((emb m,L) * (mlt (Line M1,i),(Col M2,j))) . k )
assume A30:
k in dom (mlt ((emb m,L) * (Line M1,i)),(Col M2,j))
;
:: thesis: (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) . k = ((emb m,L) * (mlt (Line M1,i),(Col M2,j))) . k
A31:
dom ((emb m,L) * (mlt (Line M1,i),(Col M2,j))) = dom (mlt (Line M1,i),(Col M2,j))
by POLYNOM1:def 2;
A32:
k in dom (mlt (Line M1,i),(Col M2,j))
by A26, A30, POLYNOM1:def 2;
A33:
len (Line M1,i) =
len M2
by A3, MATRIX_1:def 8
.=
len (Col M2,j)
by MATRIX_1:def 9
;
A34:
dom (Line M1,i) =
Seg (len (Line M1,i))
by FINSEQ_1:def 3
.=
Seg (len (mlt (Line M1,i),(Col M2,j)))
by A33, MATRIX_3:8
.=
dom (mlt (Line M1,i),(Col M2,j))
by FINSEQ_1:def 3
;
len (Line M1,i) = width M1
by MATRIX_1:def 8;
then A35:
k in Seg (width M1)
by A32, A34, FINSEQ_1:def 3;
then A36:
(Line M1,i) . k = M1 * i,
k
by MATRIX_1:def 8;
k in dom M2
by A3, A35, FINSEQ_1:def 3;
then A37:
(Col M2,j) . k = M2 * k,
j
by MATRIX_1:def 9;
A38:
k in dom ((emb m,L) * (Line M1,i))
by A32, A34, POLYNOM1:def 2;
reconsider c =
(Col M2,j) . k,
d =
(Line M1,i) . k as
Element of
L by A36, A37;
((emb m,L) * (Line M1,i)) . k = (emb m,L) * d
by A38, FVSUM_1:62;
then reconsider b =
((emb m,L) * (Line M1,i)) . k as
Element of
L ;
(mlt (Line M1,i),(Col M2,j)) . k = c * d
by A32, FVSUM_1:73;
then reconsider a =
(mlt (Line M1,i),(Col M2,j)) . k as
Element of
L ;
A39:
((emb m,L) * (mlt (Line M1,i),(Col M2,j))) . k = (emb m,L) * a
by A26, A30, FVSUM_1:62;
b * c =
((emb m,L) * d) * c
by A38, FVSUM_1:62
.=
(emb m,L) * (d * c)
by GROUP_1:def 4
.=
(emb m,L) * a
by A26, A30, A31, FVSUM_1:73
;
hence
(mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) . k = ((emb m,L) * (mlt (Line M1,i),(Col M2,j))) . k
by A30, A39, FVSUM_1:73;
:: thesis: verum
end;
hence
(emb m,L) * (mlt (Line M1,i),(Col M2,j)) = mlt ((emb m,L) * (Line M1,i)),
(Col M2,j)
by A26, FINSEQ_1:17;
:: thesis: verum
end;
hence
(emb m,L) * (mlt (Line M1,i),(Col M2,j)) = mlt (Line ((emb m,L) * M1),i),
(Col M2,j)
by A14;
:: thesis: verum
end;
hence
(emb m,L) * (Sum (mlt (Line M1,i),(Col M2,j))) = Sum (mlt (Line ((emb m,L) * M1),i),(Col M2,j))
by FVSUM_1:92;
:: thesis: verum
end;
hence
(((emb m,L) * M1) * M2) * i,
j = ((emb m,L) * (M1 * M2)) * i,
j
by A12, A13;
:: thesis: verum
end;
hence
((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2)
by A4, A5, A6, MATRIX_1:21; :: thesis: verum