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