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