let k, l, n, m be Nat; for K being Field
for M, M1 being Matrix of n,m,K
for i being Nat st l in dom M & k in dom M & i in dom M & M1 = InterchangeLine (M,l,k) holds
( ( i = l implies Line (M1,i) = Line (M,k) ) & ( i = k implies Line (M1,i) = Line (M,l) ) & ( i <> l & i <> k implies Line (M1,i) = Line (M,i) ) )
let K be Field; for M, M1 being Matrix of n,m,K
for i being Nat st l in dom M & k in dom M & i in dom M & M1 = InterchangeLine (M,l,k) holds
( ( i = l implies Line (M1,i) = Line (M,k) ) & ( i = k implies Line (M1,i) = Line (M,l) ) & ( i <> l & i <> k implies Line (M1,i) = Line (M,i) ) )
let M, M1 be Matrix of n,m,K; for i being Nat st l in dom M & k in dom M & i in dom M & M1 = InterchangeLine (M,l,k) holds
( ( i = l implies Line (M1,i) = Line (M,k) ) & ( i = k implies Line (M1,i) = Line (M,l) ) & ( i <> l & i <> k implies Line (M1,i) = Line (M,i) ) )
let i be Nat; ( l in dom M & k in dom M & i in dom M & M1 = InterchangeLine (M,l,k) implies ( ( i = l implies Line (M1,i) = Line (M,k) ) & ( i = k implies Line (M1,i) = Line (M,l) ) & ( i <> l & i <> k implies Line (M1,i) = Line (M,i) ) ) )
assume that
A1:
l in dom M
and
A2:
k in dom M
and
A3:
i in dom M
and
A4:
M1 = InterchangeLine (M,l,k)
; ( ( i = l implies Line (M1,i) = Line (M,k) ) & ( i = k implies Line (M1,i) = Line (M,l) ) & ( i <> l & i <> k implies Line (M1,i) = Line (M,i) ) )
thus
( i = l implies Line (M1,i) = Line (M,k) )
( ( i = k implies Line (M1,i) = Line (M,l) ) & ( i <> l & i <> k implies Line (M1,i) = Line (M,i) ) )proof
A5:
width M1 = width M
by Th1;
A6:
len (Line (M1,i)) = width M1
by MATRIX_0:def 7;
assume A7:
i = l
;
Line (M1,i) = Line (M,k)
A8:
now for j being Nat st 1 <= j & j <= len (Line (M1,i)) holds
(Line (M1,i)) . j = (Line (M,k)) . jlet j be
Nat;
( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = (Line (M,k)) . j )assume A9:
( 1
<= j &
j <= len (Line (M1,i)) )
;
(Line (M1,i)) . j = (Line (M,k)) . jA10:
j in Seg (width M1)
by A6, A9;
hence (Line (M1,i)) . j =
M1 * (
i,
j)
by MATRIX_0:def 7
.=
M * (
k,
j)
by A1, A4, A7, A5, A10, Def1
.=
(Line (M,k)) . j
by A5, A10, MATRIX_0:def 7
;
verum end;
len (Line (M,k)) = width M
by MATRIX_0:def 7;
hence
Line (
M1,
i)
= Line (
M,
k)
by A6, A8, Th1;
verum
end;
thus
( i = k implies Line (M1,i) = Line (M,l) )
( i <> l & i <> k implies Line (M1,i) = Line (M,i) )proof
A11:
width M1 = width M
by Th1;
A12:
len (Line (M1,i)) = width M1
by MATRIX_0:def 7;
assume A13:
i = k
;
Line (M1,i) = Line (M,l)
A14:
now for j being Nat st 1 <= j & j <= len (Line (M1,i)) holds
(Line (M1,i)) . j = (Line (M,l)) . jlet j be
Nat;
( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = (Line (M,l)) . j )assume A15:
( 1
<= j &
j <= len (Line (M1,i)) )
;
(Line (M1,i)) . j = (Line (M,l)) . jA16:
j in Seg (width M1)
by A12, A15;
hence (Line (M1,i)) . j =
M1 * (
i,
j)
by MATRIX_0:def 7
.=
M * (
l,
j)
by A2, A4, A13, A11, A16, Def1
.=
(Line (M,l)) . j
by A11, A16, MATRIX_0:def 7
;
verum end;
len (Line (M,l)) = width M
by MATRIX_0:def 7;
hence
Line (
M1,
i)
= Line (
M,
l)
by A12, A14, Th1;
verum
end;
thus
( i <> l & i <> k implies Line (M1,i) = Line (M,i) )
verumproof
A17:
width M1 = width M
by Th1;
A18:
len (Line (M1,i)) = width M1
by MATRIX_0:def 7;
assume A19:
(
i <> l &
i <> k )
;
Line (M1,i) = Line (M,i)
A20:
now for j being Nat st 1 <= j & j <= len (Line (M1,i)) holds
(Line (M1,i)) . j = (Line (M,i)) . jlet j be
Nat;
( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = (Line (M,i)) . j )assume A21:
( 1
<= j &
j <= len (Line (M1,i)) )
;
(Line (M1,i)) . j = (Line (M,i)) . jA22:
j in Seg (width M1)
by A18, A21;
hence (Line (M1,i)) . j =
M1 * (
i,
j)
by MATRIX_0:def 7
.=
M * (
i,
j)
by A3, A4, A19, A17, A22, Def1
.=
(Line (M,i)) . j
by A17, A22, MATRIX_0:def 7
;
verum end;
len (Line (M,i)) = width M
by MATRIX_0:def 7;
hence
Line (
M1,
i)
= Line (
M,
i)
by A18, A20, Th1;
verum
end;