per cases ( not i in Seg (width G) or i in Seg (width G) ) ;
suppose not i in Seg (width G) ; :: thesis: ( DelCol (G,i) is X_equal-in-line & DelCol (G,i) is Y_equal-in-column & DelCol (G,i) is Y_increasing-in-line & DelCol (G,i) is X_increasing-in-column )
then DelCol (G,i) = G by MATRIX_0:61;
hence ( DelCol (G,i) is X_equal-in-line & DelCol (G,i) is Y_equal-in-column & DelCol (G,i) is Y_increasing-in-line & DelCol (G,i) is X_increasing-in-column ) ; :: thesis: verum
end;
suppose A1: i in Seg (width G) ; :: thesis: ( DelCol (G,i) is X_equal-in-line & DelCol (G,i) is Y_equal-in-column & DelCol (G,i) is Y_increasing-in-line & DelCol (G,i) is X_increasing-in-column )
( 0 < len G & 0 < width G ) by MATRIX_0:44;
then consider m being Nat such that
A2: width G = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
set M = DelCol (G,i);
A3: width (DelCol (G,i)) = m by A1, A2, MATRIX_0:63;
then A4: ( len (DelCol (G,i)) = len G & width (DelCol (G,i)) = m ) by MATRIX_0:def 13;
then A5: dom G = dom (DelCol (G,i)) by FINSEQ_3:29;
then A6: Indices (DelCol (G,i)) = [:(dom G),(Seg m):] by A4, MATRIX_0:def 4;
A7: for k, j being Nat st k in dom G & j in Seg m holds
(DelCol (G,i)) * (k,j) = (Del ((Line (G,k)),i)) . j
proof
let k, j be Nat; :: thesis: ( k in dom G & j in Seg m implies (DelCol (G,i)) * (k,j) = (Del ((Line (G,k)),i)) . j )
assume A8: ( k in dom G & j in Seg m ) ; :: thesis: (DelCol (G,i)) * (k,j) = (Del ((Line (G,k)),i)) . j
then A9: (DelCol (G,i)) . k = Del ((Line (G,k)),i) by MATRIX_0:def 13;
[k,j] in Indices (DelCol (G,i)) by A6, A8, ZFMISC_1:87;
then ex p being FinSequence of (TOP-REAL 2) st
( p = (DelCol (G,i)) . k & (DelCol (G,i)) * (k,j) = p . j ) by MATRIX_0:def 5;
hence (DelCol (G,i)) * (k,j) = (Del ((Line (G,k)),i)) . j by A9; :: thesis: verum
end;
A10: for k, j being Nat st k in dom G & j in Seg m & not (DelCol (G,i)) * (k,j) = (Line (G,k)) . j holds
(DelCol (G,i)) * (k,j) = (Line (G,k)) . (j + 1)
proof
let k, j be Nat; :: thesis: ( k in dom G & j in Seg m & not (DelCol (G,i)) * (k,j) = (Line (G,k)) . j implies (DelCol (G,i)) * (k,j) = (Line (G,k)) . (j + 1) )
assume A11: ( k in dom G & j in Seg m ) ; :: thesis: ( (DelCol (G,i)) * (k,j) = (Line (G,k)) . j or (DelCol (G,i)) * (k,j) = (Line (G,k)) . (j + 1) )
then A12: (DelCol (G,i)) * (k,j) = (Del ((Line (G,k)),i)) . j by A7;
A13: len (Line (G,k)) = m + 1 by A2, MATRIX_0:def 7;
i in Seg (len (Line (G,k))) by A1, MATRIX_0:def 7;
then i in dom (Line (G,k)) by FINSEQ_1:def 3;
hence ( (DelCol (G,i)) * (k,j) = (Line (G,k)) . j or (DelCol (G,i)) * (k,j) = (Line (G,k)) . (j + 1) ) by A11, A12, A13, SEQM_3:44; :: thesis: verum
end;
set N = DelCol (G,i);
A14: for k being Nat holds
( not k in Seg m or Col ((DelCol (G,i)),k) = Col (G,k) or Col ((DelCol (G,i)),k) = Col (G,(k + 1)) )
proof
let k be Nat; :: thesis: ( not k in Seg m or Col ((DelCol (G,i)),k) = Col (G,k) or Col ((DelCol (G,i)),k) = Col (G,(k + 1)) )
assume A15: k in Seg m ; :: thesis: ( Col ((DelCol (G,i)),k) = Col (G,k) or Col ((DelCol (G,i)),k) = Col (G,(k + 1)) )
then A16: ( 1 <= k & k <= m ) by FINSEQ_1:1;
( m <= m + 1 & k <= k + 1 ) by NAT_1:11;
then ( k <= m + 1 & 1 <= k + 1 & k + 1 <= m + 1 ) by A16, XREAL_1:6, XXREAL_0:2;
then A17: ( k in Seg (width G) & k + 1 in Seg (width G) ) by A2, A16, FINSEQ_1:1;
A18: ( len (Col ((DelCol (G,i)),k)) = len (DelCol (G,i)) & len (Col (G,k)) = len G & len (Col (G,(k + 1))) = len G ) by MATRIX_0:def 8;
now :: thesis: ( Col ((DelCol (G,i)),k) = Col (G,k) or Col ((DelCol (G,i)),k) = Col (G,(k + 1)) )
per cases ( k < i or k >= i ) ;
suppose A19: k < i ; :: thesis: ( Col ((DelCol (G,i)),k) = Col (G,k) or Col ((DelCol (G,i)),k) = Col (G,(k + 1)) )
now :: thesis: for j being Nat st 1 <= j & j <= len (Col ((DelCol (G,i)),k)) holds
(Col ((DelCol (G,i)),k)) . j = (Col (G,k)) . j
let j be Nat; :: thesis: ( 1 <= j & j <= len (Col ((DelCol (G,i)),k)) implies (Col ((DelCol (G,i)),k)) . j = (Col (G,k)) . j )
assume ( 1 <= j & j <= len (Col ((DelCol (G,i)),k)) ) ; :: thesis: (Col ((DelCol (G,i)),k)) . j = (Col (G,k)) . j
then A20: j in dom (DelCol (G,i)) by A18, FINSEQ_3:25;
hence (Col ((DelCol (G,i)),k)) . j = (DelCol (G,i)) * (j,k) by MATRIX_0:def 8
.= (Del ((Line (G,j)),i)) . k by A7, A15, A20, A5
.= (Line (G,j)) . k by A19, FINSEQ_3:110
.= (Col (G,k)) . j by A17, A20, A5, MATRIX_0:42 ;
:: thesis: verum
end;
hence ( Col ((DelCol (G,i)),k) = Col (G,k) or Col ((DelCol (G,i)),k) = Col (G,(k + 1)) ) by A4, A18, FINSEQ_1:14; :: thesis: verum
end;
suppose A21: k >= i ; :: thesis: ( Col ((DelCol (G,i)),k) = Col (G,k) or Col ((DelCol (G,i)),k) = Col (G,(k + 1)) )
now :: thesis: for j being Nat st 1 <= j & j <= len (Col ((DelCol (G,i)),k)) holds
(Col ((DelCol (G,i)),k)) . j = (Col (G,(k + 1))) . j
let j be Nat; :: thesis: ( 1 <= j & j <= len (Col ((DelCol (G,i)),k)) implies (Col ((DelCol (G,i)),k)) . j = (Col (G,(k + 1))) . j )
assume ( 1 <= j & j <= len (Col ((DelCol (G,i)),k)) ) ; :: thesis: (Col ((DelCol (G,i)),k)) . j = (Col (G,(k + 1))) . j
then A22: j in dom (DelCol (G,i)) by A18, FINSEQ_3:25;
A23: len (Line (G,j)) = m + 1 by A2, MATRIX_0:def 7;
A24: dom (Line (G,j)) = Seg (len (Line (G,j))) by FINSEQ_1:def 3;
thus (Col ((DelCol (G,i)),k)) . j = (DelCol (G,i)) * (j,k) by A22, MATRIX_0:def 8
.= (Del ((Line (G,j)),i)) . k by A7, A15, A22, A5
.= (Line (G,j)) . (k + 1) by A2, A16, A21, A23, A24, A1, FINSEQ_3:111
.= (Col (G,(k + 1))) . j by A17, A22, A5, MATRIX_0:42 ; :: thesis: verum
end;
hence ( Col ((DelCol (G,i)),k) = Col (G,k) or Col ((DelCol (G,i)),k) = Col (G,(k + 1)) ) by A4, A18, FINSEQ_1:14; :: thesis: verum
end;
end;
end;
hence ( Col ((DelCol (G,i)),k) = Col (G,k) or Col ((DelCol (G,i)),k) = Col (G,(k + 1)) ) ; :: thesis: verum
end;
thus DelCol (G,i) is X_equal-in-line :: thesis: ( DelCol (G,i) is Y_equal-in-column & DelCol (G,i) is Y_increasing-in-line & DelCol (G,i) is X_increasing-in-column )
proof
let k be Nat; :: according to GOBOARD1:def 4 :: thesis: ( k in dom (DelCol (G,i)) implies X_axis (Line ((DelCol (G,i)),k)) is constant )
assume A25: k in dom (DelCol (G,i)) ; :: thesis: X_axis (Line ((DelCol (G,i)),k)) is constant
then A26: X_axis (Line (G,k)) is constant by Def3, A5;
m <= m + 1 by NAT_1:11;
then A27: Seg m c= Seg (width G) by A2, FINSEQ_1:5;
reconsider L = Line ((DelCol (G,i)),k), lg = Line (G,k) as FinSequence of (TOP-REAL 2) ;
set X = X_axis L;
set xg = X_axis lg;
now :: thesis: for n, j being Nat st n in dom (X_axis L) & j in dom (X_axis L) holds
(X_axis L) . n = (X_axis L) . j
let n, j be Nat; :: thesis: ( n in dom (X_axis L) & j in dom (X_axis L) implies (X_axis L) . n = (X_axis L) . j )
assume A28: ( n in dom (X_axis L) & j in dom (X_axis L) ) ; :: thesis: (X_axis L) . n = (X_axis L) . j
A29: ( dom (X_axis L) = Seg (len (X_axis L)) & len (X_axis L) = len L & len L = width (DelCol (G,i)) & dom (X_axis lg) = Seg (len (X_axis lg)) & len (X_axis lg) = len lg & len lg = width G ) by Def1, FINSEQ_1:def 3, MATRIX_0:def 7;
then A30: ( L . n = (DelCol (G,i)) * (k,n) & L . j = (DelCol (G,i)) * (k,j) & n in Seg m & j in Seg m ) by A28, A3, MATRIX_0:def 7;
then A31: ( ( L . n = lg . n or L . n = lg . (n + 1) ) & ( L . j = lg . j or L . j = lg . (j + 1) ) ) by A10, A25, A5;
( n in dom L & j in dom L ) by A28, A29, FINSEQ_1:def 3;
then ( L . n = L /. n & L . j = L /. j ) by PARTFUN1:def 6;
then A32: ( (X_axis L) . n = ((DelCol (G,i)) * (k,n)) `1 & (X_axis L) . j = ((DelCol (G,i)) * (k,j)) `1 ) by A28, A30, Def1;
( 1 <= n & n <= m & 1 <= j & j <= m ) by A4, A28, A29, FINSEQ_3:25;
then A33: ( n <= n + 1 & n + 1 <= m + 1 & j <= j + 1 & j + 1 <= m + 1 ) by NAT_1:11, XREAL_1:6;
( 1 <= n + 1 & 1 <= j + 1 ) by NAT_1:11;
then A34: ( n + 1 in Seg (width G) & j + 1 in Seg (width G) & n in Seg (width G) & j in Seg (width G) ) by A2, A4, A27, A28, A29, A33, FINSEQ_3:25;
then A35: ( lg . n = G * (k,n) & lg . (n + 1) = G * (k,(n + 1)) & lg . j = G * (k,j) & lg . (j + 1) = G * (k,(j + 1)) ) by MATRIX_0:def 7;
dom lg = Seg (len (X_axis lg)) by A29, FINSEQ_1:def 3;
then ( lg . n = lg /. n & lg . (n + 1) = lg /. (n + 1) & lg . j = lg /. j & lg . (j + 1) = lg /. (j + 1) ) by A29, A34, PARTFUN1:def 6;
then ( (X_axis lg) . n = (G * (k,n)) `1 & (X_axis lg) . (n + 1) = (G * (k,(n + 1))) `1 & (X_axis lg) . j = (G * (k,j)) `1 & (X_axis lg) . (j + 1) = (G * (k,(j + 1))) `1 ) by A29, A34, A35, Def1;
hence (X_axis L) . n = (X_axis L) . j by A26, A29, A30, A31, A32, A34, A35; :: thesis: verum
end;
hence X_axis (Line ((DelCol (G,i)),k)) is constant ; :: thesis: verum
end;
thus DelCol (G,i) is Y_equal-in-column :: thesis: ( DelCol (G,i) is Y_increasing-in-line & DelCol (G,i) is X_increasing-in-column )
proof
let k be Nat; :: according to GOBOARD1:def 5 :: thesis: ( k in Seg (width (DelCol (G,i))) implies Y_axis (Col ((DelCol (G,i)),k)) is constant )
assume A36: k in Seg (width (DelCol (G,i))) ; :: thesis: Y_axis (Col ((DelCol (G,i)),k)) is constant
then A37: ( Col ((DelCol (G,i)),k) = Col (G,k) or Col ((DelCol (G,i)),k) = Col (G,(k + 1)) ) by A4, A14;
A38: ( 1 <= k & k <= m ) by A4, A36, FINSEQ_1:1;
( m <= m + 1 & k <= k + 1 ) by NAT_1:11;
then ( k <= m + 1 & 1 <= k + 1 & k + 1 <= m + 1 ) by A38, XREAL_1:6, XXREAL_0:2;
then ( k in Seg (width G) & k + 1 in Seg (width G) ) by A2, A38, FINSEQ_1:1;
hence Y_axis (Col ((DelCol (G,i)),k)) is constant by A37, Def4; :: thesis: verum
end;
thus DelCol (G,i) is Y_increasing-in-line :: thesis: DelCol (G,i) is X_increasing-in-column
proof
let k be Nat; :: according to GOBOARD1:def 6 :: thesis: ( k in dom (DelCol (G,i)) implies Y_axis (Line ((DelCol (G,i)),k)) is increasing )
reconsider L = Line ((DelCol (G,i)),k), lg = Line (G,k) as FinSequence of (TOP-REAL 2) ;
set X = Y_axis L;
set xg = Y_axis lg;
m <= m + 1 by NAT_1:11;
then A39: Seg m c= Seg (width G) by A2, FINSEQ_1:5;
assume A40: k in dom (DelCol (G,i)) ; :: thesis: Y_axis (Line ((DelCol (G,i)),k)) is increasing
then A41: Y_axis lg is increasing by Def5, A5;
now :: thesis: for n, j being Nat st n in dom (Y_axis L) & j in dom (Y_axis L) & n < j holds
(Y_axis L) . n < (Y_axis L) . j
let n, j be Nat; :: thesis: ( n in dom (Y_axis L) & j in dom (Y_axis L) & n < j implies (Y_axis L) . b1 < (Y_axis L) . b2 )
assume A42: ( n in dom (Y_axis L) & j in dom (Y_axis L) & n < j ) ; :: thesis: (Y_axis L) . b1 < (Y_axis L) . b2
A43: ( dom (Y_axis L) = Seg (len (Y_axis L)) & len (Y_axis L) = len L & len L = width (DelCol (G,i)) & dom (Y_axis lg) = Seg (len (Y_axis lg)) & len (Y_axis lg) = len lg & len lg = width G ) by Def2, FINSEQ_1:def 3, MATRIX_0:def 7;
then A44: ( L . n = (DelCol (G,i)) * (k,n) & L . j = (DelCol (G,i)) * (k,j) & n in Seg m & j in Seg m ) by A42, A3, MATRIX_0:def 7;
dom L = Seg (len (Y_axis L)) by A43, FINSEQ_1:def 3;
then ( L . n = L /. n & L . j = L /. j ) by A42, A43, PARTFUN1:def 6;
then A45: ( (Y_axis L) . n = ((DelCol (G,i)) * (k,n)) `2 & (Y_axis L) . j = ((DelCol (G,i)) * (k,j)) `2 ) by A42, A44, Def2;
A46: ( 1 <= n & n <= m & 1 <= j & j <= m ) by A4, A42, A43, FINSEQ_3:25;
then A47: ( n <= n + 1 & n + 1 <= m + 1 & j <= j + 1 & j + 1 <= m + 1 ) by NAT_1:11, XREAL_1:6;
( 1 <= n + 1 & 1 <= j + 1 ) by NAT_1:11;
then A48: ( n + 1 in Seg (width G) & j + 1 in Seg (width G) & n in Seg (width G) & j in Seg (width G) ) by A2, A4, A39, A42, A43, A47, FINSEQ_3:25;
then A49: ( lg . n = G * (k,n) & lg . (n + 1) = G * (k,(n + 1)) & lg . j = G * (k,j) & lg . (j + 1) = G * (k,(j + 1)) ) by MATRIX_0:def 7;
dom lg = Seg (len (Y_axis lg)) by A43, FINSEQ_1:def 3;
then ( lg . n = lg /. n & lg . (n + 1) = lg /. (n + 1) & lg . j = lg /. j & lg . (j + 1) = lg /. (j + 1) ) by A43, A48, PARTFUN1:def 6;
then A50: ( (Y_axis lg) . n = (G * (k,n)) `2 & (Y_axis lg) . (n + 1) = (G * (k,(n + 1))) `2 & (Y_axis lg) . j = (G * (k,j)) `2 & (Y_axis lg) . (j + 1) = (G * (k,(j + 1))) `2 ) by A43, A48, A49, Def2;
set r = (Y_axis L) . n;
set s = (Y_axis L) . j;
A51: dom lg = Seg (len lg) by FINSEQ_1:def 3;
per cases ( j < i or j >= i ) ;
suppose A52: j < i ; :: thesis: (Y_axis L) . b1 < (Y_axis L) . b2
then A53: n < i by A42, XXREAL_0:2;
A54: (DelCol (G,i)) * (k,n) = (Del (lg,i)) . n by A4, A7, A40, A42, A43, A5
.= G * (k,n) by A49, A53, FINSEQ_3:110 ;
(DelCol (G,i)) * (k,j) = (Del (lg,i)) . j by A4, A7, A40, A42, A43, A5
.= G * (k,j) by A49, A52, FINSEQ_3:110 ;
hence (Y_axis L) . n < (Y_axis L) . j by A4, A39, A41, A42, A43, A45, A50, A54; :: thesis: verum
end;
suppose A55: j >= i ; :: thesis: (Y_axis L) . b1 < (Y_axis L) . b2
A56: (DelCol (G,i)) * (k,j) = (Del (lg,i)) . j by A4, A7, A40, A42, A43, A5
.= G * (k,(j + 1)) by A2, A43, A46, A49, A51, A55, A1, FINSEQ_3:111 ;
now :: thesis: (Y_axis L) . n < (Y_axis L) . j
per cases ( n < i or n >= i ) ;
suppose A57: n < i ; :: thesis: (Y_axis L) . n < (Y_axis L) . j
j <= j + 1 by NAT_1:11;
then A58: n < j + 1 by A42, XXREAL_0:2;
(DelCol (G,i)) * (k,n) = (Del (lg,i)) . n by A4, A7, A40, A42, A43, A5
.= G * (k,n) by A49, A57, FINSEQ_3:110 ;
hence (Y_axis L) . n < (Y_axis L) . j by A41, A43, A45, A48, A50, A56, A58; :: thesis: verum
end;
suppose A59: n >= i ; :: thesis: (Y_axis L) . n < (Y_axis L) . j
A60: n + 1 < j + 1 by A42, XREAL_1:6;
(DelCol (G,i)) * (k,n) = (Del (lg,i)) . n by A4, A7, A40, A42, A43, A5
.= G * (k,(n + 1)) by A2, A43, A46, A49, A51, A59, A1, FINSEQ_3:111 ;
hence (Y_axis L) . n < (Y_axis L) . j by A41, A43, A45, A48, A50, A56, A60; :: thesis: verum
end;
end;
end;
hence (Y_axis L) . n < (Y_axis L) . j ; :: thesis: verum
end;
end;
end;
hence Y_axis (Line ((DelCol (G,i)),k)) is increasing ; :: thesis: verum
end;
let k be Nat; :: according to GOBOARD1:def 7 :: thesis: ( k in Seg (width (DelCol (G,i))) implies X_axis (Col ((DelCol (G,i)),k)) is increasing )
assume A61: k in Seg (width (DelCol (G,i))) ; :: thesis: X_axis (Col ((DelCol (G,i)),k)) is increasing
then A62: ( Col ((DelCol (G,i)),k) = Col (G,k) or Col ((DelCol (G,i)),k) = Col (G,(k + 1)) ) by A4, A14;
A63: ( 1 <= k & k <= m ) by A4, A61, FINSEQ_1:1;
( m <= m + 1 & k <= k + 1 ) by NAT_1:11;
then ( k <= m + 1 & 1 <= k + 1 & k + 1 <= m + 1 ) by A63, XREAL_1:6, XXREAL_0:2;
then ( k in Seg (width G) & k + 1 in Seg (width G) ) by A2, A63, FINSEQ_1:1;
hence X_axis (Col ((DelCol (G,i)),k)) is increasing by A62, Def6; :: thesis: verum
end;
end;