let i be Nat; :: thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in Seg (width G) & rng f misses rng (Col (G,i)) & width G > 1 holds
f is_sequence_on DelCol (G,i)
let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in Seg (width G) & rng f misses rng (Col (G,i)) & width G > 1 holds
f is_sequence_on DelCol (G,i)
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & i in Seg (width G) & rng f misses rng (Col (G,i)) & width G > 1 implies f is_sequence_on DelCol (G,i) )
set D = DelCol (G,i);
assume that
A1: f is_sequence_on G and
A2: i in Seg (width G) and
A3: rng f misses rng (Col (G,i)) and
A4: width G > 1 ; :: thesis: f is_sequence_on DelCol (G,i)
A5: len G = len (DelCol (G,i)) by MATRIX_0:def 13;
A6: Indices (DelCol (G,i)) = [:(dom (DelCol (G,i))),(Seg (width (DelCol (G,i)))):] by MATRIX_0:def 4;
A7: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_0:def 4;
A8: ( dom G = Seg (len G) & dom (DelCol (G,i)) = Seg (len (DelCol (G,i))) ) by FINSEQ_1:def 3;
consider M being Nat such that
A9: width G = M + 1 and
A10: M > 0 by A4, SEQM_3:43;
A11: width (DelCol (G,i)) = M by A2, A9, MATRIX_0:63;
A12: now :: thesis: for n being Nat st n in dom f & n + 1 in dom f holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices (DelCol (G,i)) & [j1,j2] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
let n be Nat; :: thesis: ( n in dom f & n + 1 in dom f implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices (DelCol (G,i)) & [j1,j2] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 )
assume A13: ( n in dom f & n + 1 in dom f ) ; :: thesis: for i1, i2, j1, j2 being Nat st [i1,i2] in Indices (DelCol (G,i)) & [j1,j2] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
let i1, i2, j1, j2 be Nat; :: thesis: ( [i1,i2] in Indices (DelCol (G,i)) & [j1,j2] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )
assume that
A14: [i1,i2] in Indices (DelCol (G,i)) and
A15: [j1,j2] in Indices (DelCol (G,i)) and
A16: ( f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) ) ; :: thesis: |.(i1 - j1).| + |.(i2 - j2).| = 1
A17: i1 in dom (DelCol (G,i)) by A6, A14, ZFMISC_1:87;
A18: i2 in Seg (width (DelCol (G,i))) by A6, A14, ZFMISC_1:87;
then A19: 1 <= i2 by FINSEQ_1:1;
A20: i2 <= M by A11, A18, FINSEQ_1:1;
then ( 1 <= i2 + 1 & i2 + 1 <= M + 1 ) by NAT_1:11, XREAL_1:6;
then i2 + 1 in Seg (M + 1) by FINSEQ_1:1;
then A21: [i1,(i2 + 1)] in Indices G by A5, A9, A8, A7, A17, ZFMISC_1:87;
A22: j1 in dom (DelCol (G,i)) by A6, A15, ZFMISC_1:87;
A23: j2 in Seg (width (DelCol (G,i))) by A6, A15, ZFMISC_1:87;
then A24: 1 <= j2 by FINSEQ_1:1;
M <= M + 1 by NAT_1:11;
then A25: Seg (width (DelCol (G,i))) c= Seg (width G) by A9, A11, FINSEQ_1:5;
then A26: [j1,j2] in Indices G by A5, A8, A7, A22, A23, ZFMISC_1:87;
A27: j2 <= M by A11, A23, FINSEQ_1:1;
then ( 1 <= j2 + 1 & j2 + 1 <= M + 1 ) by NAT_1:11, XREAL_1:6;
then j2 + 1 in Seg (M + 1) by FINSEQ_1:1;
then A28: [j1,(j2 + 1)] in Indices G by A5, A9, A8, A7, A22, ZFMISC_1:87;
A29: [i1,i2] in Indices G by A5, A8, A7, A17, A18, A25, ZFMISC_1:87;
now :: thesis: ( ( i2 < i & j2 < i & |.(i1 - j1).| + |.(i2 - j2).| = 1 ) or ( i <= i2 & j2 < i & contradiction ) or ( i2 < i & i <= j2 & contradiction ) or ( i <= i2 & i <= j2 & 1 = |.(i1 - j1).| + |.(i2 - j2).| ) )
per cases ( ( i2 < i & j2 < i ) or ( i <= i2 & j2 < i ) or ( i2 < i & i <= j2 ) or ( i <= i2 & i <= j2 ) ) ;
case ( i2 < i & j2 < i ) ; :: thesis: |.(i1 - j1).| + |.(i2 - j2).| = 1
then ( f /. n = G * (i1,i2) & f /. (n + 1) = G * (j1,j2) ) by A2, A5, A9, A10, A8, A16, A17, A22, A19, A24, Th8;
hence |.(i1 - j1).| + |.(i2 - j2).| = 1 by A1, A13, A29, A26; :: thesis: verum
end;
case A30: ( i <= i2 & j2 < i ) ; :: thesis: contradiction
i2 <= i2 + 1 by NAT_1:11;
then i <= i2 + 1 by A30, XXREAL_0:2;
then A31: j2 < i2 + 1 by A30, XXREAL_0:2;
then j2 + 1 <= i2 + 1 by NAT_1:13;
then A32: 1 <= (i2 + 1) - j2 by XREAL_1:19;
( f /. n = G * (i1,(i2 + 1)) & f /. (n + 1) = G * (j1,j2) ) by A2, A5, A9, A8, A16, A17, A22, A20, A24, A30, Th8, Th9;
then A33: 1 = |.(i1 - j1).| + |.((i2 + 1) - j2).| by A1, A13, A26, A21;
0 < (i2 + 1) - j2 by A31, XREAL_1:50;
then A34: |.((i2 + 1) - j2).| = (i2 + 1) - j2 by ABSVALUE:def 1;
0 <= |.(i1 - j1).| by COMPLEX1:46;
then 0 + ((i2 + 1) - j2) <= 1 by A33, A34, XREAL_1:7;
then (i2 + 1) - j2 = 1 by A32, XXREAL_0:1;
hence contradiction by A30; :: thesis: verum
end;
case A35: ( i2 < i & i <= j2 ) ; :: thesis: contradiction
j2 <= j2 + 1 by NAT_1:11;
then i <= j2 + 1 by A35, XXREAL_0:2;
then A36: i2 < j2 + 1 by A35, XXREAL_0:2;
then i2 + 1 <= j2 + 1 by NAT_1:13;
then A37: 1 <= (j2 + 1) - i2 by XREAL_1:19;
( f /. n = G * (i1,i2) & f /. (n + 1) = G * (j1,(j2 + 1)) ) by A2, A5, A9, A8, A16, A17, A22, A19, A27, A35, Th8, Th9;
then A38: 1 = |.(i1 - j1).| + |.(i2 - (j2 + 1)).| by A1, A13, A29, A28
.= |.(i1 - j1).| + |.(- ((j2 + 1) - i2)).|
.= |.(i1 - j1).| + |.((j2 + 1) - i2).| by COMPLEX1:52 ;
0 < (j2 + 1) - i2 by A36, XREAL_1:50;
then A39: |.((j2 + 1) - i2).| = (j2 + 1) - i2 by ABSVALUE:def 1;
0 <= |.(i1 - j1).| by COMPLEX1:46;
then 0 + ((j2 + 1) - i2) <= 1 by A38, A39, XREAL_1:7;
then (j2 + 1) - i2 = 1 by A37, XXREAL_0:1;
hence contradiction by A35; :: thesis: verum
end;
case ( i <= i2 & i <= j2 ) ; :: thesis: 1 = |.(i1 - j1).| + |.(i2 - j2).|
then ( f /. n = G * (i1,(i2 + 1)) & f /. (n + 1) = G * (j1,(j2 + 1)) ) by A2, A5, A9, A10, A8, A16, A17, A22, A20, A27, Th9;
hence 1 = |.(i1 - j1).| + |.((i2 + 1) - (j2 + 1)).| by A1, A13, A21, A28
.= |.(i1 - j1).| + |.(i2 - j2).| ;
:: thesis: verum
end;
end;
end;
hence |.(i1 - j1).| + |.(i2 - j2).| = 1 ; :: thesis: verum
end;
A40: 1 <= i by A2, FINSEQ_1:1;
A41: i <= width G by A2, FINSEQ_1:1;
now :: thesis: for n being Nat st n in dom f holds
ex m, k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
let n be Nat; :: thesis: ( n in dom f implies ex m, k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) ) )
assume A42: n in dom f ; :: thesis: ex m, k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
then consider m, k being Nat such that
A43: [m,k] in Indices G and
A44: f /. n = G * (m,k) by A1;
take m = m; :: thesis: ex k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
A45: m in dom G by A7, A43, ZFMISC_1:87;
A46: k in Seg (width G) by A7, A43, ZFMISC_1:87;
then A47: 1 <= k by FINSEQ_1:1;
A48: k <= M + 1 by A9, A46, FINSEQ_1:1;
now :: thesis: ex k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
per cases ( k < i or i <= k ) ;
suppose A49: k < i ; :: thesis: ex k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
take k = k; :: thesis: ( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
k < width G by A41, A49, XXREAL_0:2;
then k <= M by A9, NAT_1:13;
then k in Seg M by A47, FINSEQ_1:1;
hence ( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) ) by A2, A5, A9, A10, A11, A8, A6, A44, A45, A47, A49, Th8, ZFMISC_1:87; :: thesis: verum
end;
suppose i <= k ; :: thesis: ex l being Nat st
( [m,l] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,l) )
then A50: i < k by A3, A42, A44, A45, MATRIX_0:43, XXREAL_0:1;
then k - 1 in NAT by A40, INT_1:5, XXREAL_0:2;
then reconsider l = k - 1 as Nat ;
take l = l; :: thesis: ( [m,l] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,l) )
A51: l <= M by A48, XREAL_1:20;
i + 1 <= k by A50, NAT_1:13;
then A52: i <= k - 1 by XREAL_1:19;
then 1 <= l by A40, XXREAL_0:2;
then A53: l in Seg M by A51, FINSEQ_1:1;
(DelCol (G,i)) * (m,l) = G * (m,(l + 1)) by A2, A9, A40, A45, A52, A51, Th9;
hence ( [m,l] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,l) ) by A5, A11, A8, A6, A44, A45, A53, ZFMISC_1:87; :: thesis: verum
end;
end;
end;
hence ex k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) ) ; :: thesis: verum
end;
hence f is_sequence_on DelCol (G,i) by A12; :: thesis: verum