let k, l, n, m be Nat; for K being Field
for a being Element of K
for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds
(RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a)
let K be Field; for a being Element of K
for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds
(RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a)
let a be Element of K; for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds
(RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a)
let M, M1 be Matrix of n,m,K; ( l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ implies (RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a) )
assume that
A1:
l in Seg (width M)
and
A2:
k in Seg (width M)
and
A3:
n > 0
and
A4:
m > 0
and
A5:
M1 = M @
; (RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a)
A6:
width M = m
by A3, MATRIX_0:23;
then A7:
len M1 = m
by A4, A5, MATRIX_0:54;
A8:
width (RLineXS (M1,l,k,a)) = width M1
by Th1;
len M = n
by A3, MATRIX_0:23;
then A9:
width M1 = n
by A4, A5, A6, MATRIX_0:54;
then A10:
len ((RLineXS (M1,l,k,a)) @) = n
by A3, A8, MATRIX_0:54;
A11: dom M1 =
Seg (len M1)
by FINSEQ_1:def 3
.=
Seg (width M)
by A4, A5, A6, MATRIX_0:54
;
then
len (RLineXS (M1,l,k,a)) = len M1
by A2, Def3;
then
width ((RLineXS (M1,l,k,a)) @) = m
by A3, A7, A9, A8, MATRIX_0:54;
then A12:
(RLineXS (M1,l,k,a)) @ is Matrix of n,m,K
by A3, A10, MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A13:
M2 = (RLineXS (M1,l,k,a)) @
;
A14:
for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) )
proof
let i,
j be
Nat;
( i in dom M & j in Seg (width M) implies ( ( j = l implies M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) )
assume that A15:
i in dom M
and A16:
j in Seg (width M)
;
( ( j = l implies M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) )
A17:
[i,j] in Indices M
by A15, A16, ZFMISC_1:87;
then A18:
[j,i] in Indices M1
by A5, MATRIX_0:def 6;
then A19:
i in Seg (width M1)
by ZFMISC_1:87;
A20:
len M1 = width M
by A5, MATRIX_0:def 6;
then A21:
k in dom M1
by A2, FINSEQ_1:def 3;
dom (RLineXS (M1,l,k,a)) =
Seg (len (RLineXS (M1,l,k,a)))
by FINSEQ_1:def 3
.=
Seg (len M1)
by A2, A11, Def3
.=
dom M1
by FINSEQ_1:def 3
;
then A22:
[j,i] in Indices (RLineXS (M1,l,k,a))
by A18, Th1;
A23:
l in dom M1
by A1, A20, FINSEQ_1:def 3;
thus
(
j = l implies
M2 * (
i,
j)
= (a * (M * (i,k))) + (M * (i,l)) )
( j <> l implies M2 * (i,j) = M * (i,j) )proof
A24:
[i,k] in Indices M
by A2, A15, ZFMISC_1:87;
assume A25:
j = l
;
M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l))
M2 * (
i,
j) =
(RLineXS (M1,l,k,a)) * (
j,
i)
by A13, A22, MATRIX_0:def 6
.=
(a * (M1 * (k,i))) + (M1 * (l,i))
by A23, A21, A19, A25, Def3
.=
(a * (M * (i,k))) + (M1 * (l,i))
by A5, A24, MATRIX_0:def 6
.=
(a * (M * (i,k))) + (M * (i,l))
by A5, A17, A25, MATRIX_0:def 6
;
hence
M2 * (
i,
j)
= (a * (M * (i,k))) + (M * (i,l))
;
verum
end;
A26:
j in dom M1
by A18, ZFMISC_1:87;
thus
(
j <> l implies
M2 * (
i,
j)
= M * (
i,
j) )
verumproof
assume A27:
j <> l
;
M2 * (i,j) = M * (i,j)
M2 * (
i,
j) =
(RLineXS (M1,l,k,a)) * (
j,
i)
by A13, A22, MATRIX_0:def 6
.=
M1 * (
j,
i)
by A21, A26, A19, A27, Def3
.=
M * (
i,
j)
by A5, A17, MATRIX_0:def 6
;
hence
M2 * (
i,
j)
= M * (
i,
j)
;
verum
end;
end;
for i, j being Nat st [i,j] in Indices (RColXS (M,l,k,a)) holds
(RColXS (M,l,k,a)) * (i,j) = ((RLineXS (M1,l,k,a)) @) * (i,j)
proof
A28:
Indices M = Indices (RColXS (M,l,k,a))
by MATRIX_0:26;
let i,
j be
Nat;
( [i,j] in Indices (RColXS (M,l,k,a)) implies (RColXS (M,l,k,a)) * (i,j) = ((RLineXS (M1,l,k,a)) @) * (i,j) )
assume
[i,j] in Indices (RColXS (M,l,k,a))
;
(RColXS (M,l,k,a)) * (i,j) = ((RLineXS (M1,l,k,a)) @) * (i,j)
then A29:
(
i in dom M &
j in Seg (width M) )
by A28, ZFMISC_1:87;
then A30:
(
j = l implies
((RLineXS (M1,l,k,a)) @) * (
i,
j)
= (a * (M * (i,k))) + (M * (i,l)) )
by A13, A14;
A31:
(
j <> l implies
((RLineXS (M1,l,k,a)) @) * (
i,
j)
= M * (
i,
j) )
by A13, A14, A29;
(
j = l implies
(RColXS (M,l,k,a)) * (
i,
j)
= (a * (M * (i,k))) + (M * (i,l)) )
by A2, A3, A4, A29, Def6;
hence
(RColXS (M,l,k,a)) * (
i,
j)
= ((RLineXS (M1,l,k,a)) @) * (
i,
j)
by A1, A2, A3, A4, A29, A30, A31, Def6;
verum
end;
hence
(RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a)
by A12, MATRIX_0:27; verum