let m, n, l, k be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A1:
( l in dom M & k in dom M & i in dom M & M1 = InterchangeLine M,l,k )
; :: thesis: ( ( 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 )
:: thesis: ( ( i = k implies Line M1,i = Line M,l ) & ( i <> l & i <> k implies Line M1,i = Line M,i ) )proof
assume A2:
i = l
;
:: thesis: Line M1,i = Line M,k
A3:
width M1 = width M
by Th1;
A4:
(
len (Line M1,i) = width M1 &
len (Line M,k) = width M )
by MATRIX_1:def 8;
now let j be
Nat;
:: thesis: ( 1 <= j & j <= len (Line M1,i) implies (Line M1,i) . j = (Line M,k) . j )assume A5:
( 1
<= j &
j <= len (Line M1,i) )
;
:: thesis: (Line M1,i) . j = (Line M,k) . j
j in NAT
by ORDINAL1:def 13;
then A6:
j in Seg (width M1)
by A4, A5;
hence (Line M1,i) . j =
M1 * i,
j
by MATRIX_1:def 8
.=
M * k,
j
by A1, A2, A3, A6, Def1
.=
(Line M,k) . j
by A3, A6, MATRIX_1:def 8
;
:: thesis: verum end;
hence
Line M1,
i = Line M,
k
by A3, A4, FINSEQ_1:18;
:: thesis: verum
end;
thus
( i = k implies Line M1,i = Line M,l )
:: thesis: ( i <> l & i <> k implies Line M1,i = Line M,i )proof
assume A7:
i = k
;
:: thesis: Line M1,i = Line M,l
A8:
width M1 = width M
by Th1;
A9:
(
len (Line M1,i) = width M1 &
len (Line M,l) = width M )
by MATRIX_1:def 8;
now let j be
Nat;
:: thesis: ( 1 <= j & j <= len (Line M1,i) implies (Line M1,i) . j = (Line M,l) . j )assume A10:
( 1
<= j &
j <= len (Line M1,i) )
;
:: thesis: (Line M1,i) . j = (Line M,l) . j
j in NAT
by ORDINAL1:def 13;
then A11:
j in Seg (width M1)
by A9, A10;
hence (Line M1,i) . j =
M1 * i,
j
by MATRIX_1:def 8
.=
M * l,
j
by A1, A7, A8, A11, Def1
.=
(Line M,l) . j
by A8, A11, MATRIX_1:def 8
;
:: thesis: verum end;
hence
Line M1,
i = Line M,
l
by A8, A9, FINSEQ_1:18;
:: thesis: verum
end;
thus
( i <> l & i <> k implies Line M1,i = Line M,i )
:: thesis: verumproof
assume A12:
(
i <> l &
i <> k )
;
:: thesis: Line M1,i = Line M,i
A13:
width M1 = width M
by Th1;
A14:
(
len (Line M1,i) = width M1 &
len (Line M,i) = width M )
by MATRIX_1:def 8;
now let j be
Nat;
:: thesis: ( 1 <= j & j <= len (Line M1,i) implies (Line M1,i) . j = (Line M,i) . j )assume A15:
( 1
<= j &
j <= len (Line M1,i) )
;
:: thesis: (Line M1,i) . j = (Line M,i) . j
j in NAT
by ORDINAL1:def 13;
then A16:
j in Seg (width M1)
by A14, A15;
hence (Line M1,i) . j =
M1 * i,
j
by MATRIX_1:def 8
.=
M * i,
j
by A1, A12, A13, A16, Def1
.=
(Line M,i) . j
by A13, A16, MATRIX_1:def 8
;
:: thesis: verum end;
hence
Line M1,
i = Line M,
i
by A13, A14, FINSEQ_1:18;
:: thesis: verum
end;