let k, l, n, m be Nat; for K being Field
for M being Matrix of n,m,K holds ILine (M,l,k) = ILine (M,k,l)
let K be Field; for M being Matrix of n,m,K holds ILine (M,l,k) = ILine (M,k,l)
let M be Matrix of n,m,K; ILine (M,l,k) = ILine (M,k,l)
A1:
width (ILine (M,k,l)) = width M
by Th1;
A2:
for i, j being Nat st [i,j] in Indices (ILine (M,l,k)) holds
(ILine (M,l,k)) * (i,j) = (ILine (M,k,l)) * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices (ILine (M,l,k)) implies (ILine (M,l,k)) * (i,j) = (ILine (M,k,l)) * (i,j) )
A3:
Indices (ILine (M,l,k)) = Indices M
by MATRIX_0:26;
assume
[i,j] in Indices (ILine (M,l,k))
;
(ILine (M,l,k)) * (i,j) = (ILine (M,k,l)) * (i,j)
then A4:
(
i in dom M &
j in Seg (width M) )
by A3, ZFMISC_1:87;
then A5:
(
i = k implies
(ILine (M,l,k)) * (
i,
j)
= M * (
l,
j) )
by Def1;
A6:
(
i = l implies
(ILine (M,k,l)) * (
i,
j)
= M * (
k,
j) )
by A4, Def1;
A7:
(
i <> l &
i <> k implies
(ILine (M,l,k)) * (
i,
j)
= M * (
i,
j) )
by A4, Def1;
A8:
(
i = k implies
(ILine (M,k,l)) * (
i,
j)
= M * (
l,
j) )
by A4, Def1;
(
i = l implies
(ILine (M,l,k)) * (
i,
j)
= M * (
k,
j) )
by A4, Def1;
hence
(ILine (M,l,k)) * (
i,
j)
= (ILine (M,k,l)) * (
i,
j)
by A4, A5, A7, A6, A8, Def1;
verum
end;
( len (ILine (M,l,k)) = len M & len (ILine (M,k,l)) = len M )
by Def1;
hence
ILine (M,l,k) = ILine (M,k,l)
by A1, A2, Th1, MATRIX_0:21; verum