let n be Nat; for K being Field
for M being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n holds
for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds
( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )
let K be Field; for M being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n holds
for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds
( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )
let M be Matrix of n,K; for i, j being Nat st i in Seg n & j in Seg n holds
for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds
( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )
let i, j be Nat; ( i in Seg n & j in Seg n implies for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds
( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) ) )
assume that
A1:
i in Seg n
and
A2:
j in Seg n
; for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds
( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )
set DM = Delete (M,i,j);
A3:
Deleting (M,i,j) = Delete (M,i,j)
by A1, A2, Def1;
n > 0
by A1;
then reconsider n9 = n - 1 as Element of NAT by NAT_1:20;
set DL = DelLine (M,i);
let k, m be Nat; ( k in Seg (n -' 1) & m in Seg (n -' 1) implies ( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) ) )
assume that
A4:
k in Seg (n -' 1)
and
A5:
m in Seg (n -' 1)
; ( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )
A6:
n -' 1 = n9
by XREAL_0:def 2;
then A7:
k + 1 in Seg (n9 + 1)
by A4, FINSEQ_1:60;
reconsider I = i, J = j, K = k, U = m as Element of NAT by ORDINAL1:def 12;
n9 <= n9 + 1
by NAT_1:11;
then A8:
Seg n9 c= Seg n
by FINSEQ_1:5;
A9:
len M = n
by MATRIX_0:24;
then A10:
dom M = Seg n
by FINSEQ_1:def 3;
then
len (DelLine (M,i)) = n9
by A1, A6, A9, Th1;
then A11:
dom (DelLine (M,i)) = Seg n9
by FINSEQ_1:def 3;
then A12:
(Deleting (M,i,j)) . k = Del ((Line ((DelLine (M,i)),k)),j)
by A4, A6, MATRIX_0:def 13;
len (Delete (M,i,j)) = n9
by A6, MATRIX_0:24;
then
dom (Delete (M,i,j)) = Seg n9
by FINSEQ_1:def 3;
then A13:
(Delete (M,i,j)) . k = Line ((Delete (M,i,j)),k)
by A4, A6, MATRIX_0:60;
width (Delete (M,i,j)) = n9
by A6, MATRIX_0:24;
then A14:
(Line ((Delete (M,i,j)),k)) . m = (Delete (M,i,j)) * (k,m)
by A5, A6, MATRIX_0:def 7;
A15:
Line ((DelLine (M,i)),k) = (DelLine (M,i)) . k
by A4, A6, A11, MATRIX_0:60;
A16:
m + 1 in Seg (n9 + 1)
by A5, A6, FINSEQ_1:60;
A17:
( K >= I implies ( ( U < J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),U) ) & ( U >= J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1)) ) ) )
proof
assume A18:
K >= I
;
( ( U < J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),U) ) & ( U >= J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1)) ) )
K <= n9
by A4, A6, FINSEQ_1:1;
then A19:
(DelLine (M,i)) . K = M . (K + 1)
by A1, A9, A10, A7, A18, FINSEQ_3:111;
A20:
M . (K + 1) = Line (
M,
(K + 1))
by A10, A7, MATRIX_0:60;
thus
(
U < J implies
(Delete (M,i,j)) * (
K,
U)
= M * (
(K + 1),
U) )
( U >= J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1)) )proof
A21:
width M = n
by MATRIX_0:24;
assume
U < J
;
(Delete (M,i,j)) * (K,U) = M * ((K + 1),U)
then
(Delete (M,i,j)) * (
K,
U)
= (Line (M,(K + 1))) . U
by A12, A3, A13, A14, A15, A19, A20, FINSEQ_3:110;
hence
(Delete (M,i,j)) * (
K,
U)
= M * (
(K + 1),
U)
by A5, A6, A8, A21, MATRIX_0:def 7;
verum
end;
assume A22:
U >= J
;
(Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1))
A23:
U <= n9
by A5, A6, FINSEQ_1:1;
A24:
width M = n
by MATRIX_0:24;
A25:
len (Line ((DelLine (M,i)),K)) = width M
by A15, A19, A20, MATRIX_0:def 7;
then
J in dom (Line ((DelLine (M,i)),K))
by A2, A24, FINSEQ_1:def 3;
then
(Delete (M,i,j)) * (
K,
U)
= (Line (M,(K + 1))) . (U + 1)
by A12, A3, A13, A14, A15, A7, A19, A20, A22, A25, A23, FINSEQ_3:111, MATRIX_0:24;
hence
(Delete (M,i,j)) * (
K,
U)
= M * (
(K + 1),
(U + 1))
by A16, A24, MATRIX_0:def 7;
verum
end;
( K < I implies ( ( U < J implies (Delete (M,i,j)) * (K,U) = M * (K,U) ) & ( U >= J implies (Delete (M,i,j)) * (K,U) = M * (K,(U + 1)) ) ) )
proof
assume
K < I
;
( ( U < J implies (Delete (M,i,j)) * (K,U) = M * (K,U) ) & ( U >= J implies (Delete (M,i,j)) * (K,U) = M * (K,(U + 1)) ) )
then A26:
(DelLine (M,i)) . K = M . K
by FINSEQ_3:110;
A27:
M . K = Line (
M,
K)
by A4, A6, A10, A8, MATRIX_0:60;
thus
(
U < J implies
(Delete (M,i,j)) * (
K,
U)
= M * (
K,
U) )
( U >= J implies (Delete (M,i,j)) * (K,U) = M * (K,(U + 1)) )proof
assume A28:
U < J
;
(Delete (M,i,j)) * (K,U) = M * (K,U)
A29:
width M = n9 + 1
by MATRIX_0:24;
(Delete (M,i,j)) * (
K,
U)
= (Line (M,K)) . U
by A12, A3, A13, A14, A15, A26, A27, A28, FINSEQ_3:110;
hence
(Delete (M,i,j)) * (
K,
U)
= M * (
K,
U)
by A5, A6, A8, A29, MATRIX_0:def 7;
verum
end;
assume A30:
U >= J
;
(Delete (M,i,j)) * (K,U) = M * (K,(U + 1))
A31:
U <= n9
by A5, A6, FINSEQ_1:1;
A32:
width M = n
by MATRIX_0:24;
A33:
len (Line ((DelLine (M,i)),K)) = width M
by A15, A26, A27, MATRIX_0:def 7;
then
J in dom (Line ((DelLine (M,i)),K))
by A2, A32, FINSEQ_1:def 3;
then
(Delete (M,i,j)) * (
K,
U)
= (Line (M,K)) . (U + 1)
by A12, A3, A13, A14, A15, A7, A26, A27, A30, A33, A31, FINSEQ_3:111, MATRIX_0:24;
hence
(Delete (M,i,j)) * (
K,
U)
= M * (
K,
(U + 1))
by A16, A32, MATRIX_0:def 7;
verum
end;
hence
( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )
by A17; verum