:: GOBOARD5 semantic presentation
begin
definition
let G be Matrix of (TOP-REAL 2);
let i be Nat;
func v_strip (G,i) -> Subset of (TOP-REAL 2) equals :Def1: :: GOBOARD5:def 1
{ |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } if ( 1 <= i & i < len G )
{ |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } if i >= len G
otherwise { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } ;
coherence
( ( 1 <= i & i < len G implies { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } is Subset of (TOP-REAL 2) ) & ( i >= len G implies { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < len G ) & not i >= len G implies { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } is Subset of (TOP-REAL 2) ) )
proof
hereby ::_thesis: ( ( i >= len G implies { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < len G ) & not i >= len G implies { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } is Subset of (TOP-REAL 2) ) )
assume that
1 <= i and
i < len G ; ::_thesis: { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } is Subset of (TOP-REAL 2)
set A = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } ;
{ |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } or x in the carrier of (TOP-REAL 2) )
assume x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex r, s being Real st
( x = |[r,s]| & (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
hence { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } is Subset of (TOP-REAL 2) ; ::_thesis: verum
end;
hereby ::_thesis: ( ( not 1 <= i or not i < len G ) & not i >= len G implies { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } is Subset of (TOP-REAL 2) )
assume i >= len G ; ::_thesis: { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } is Subset of (TOP-REAL 2)
set A = { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } ;
{ |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } or x in the carrier of (TOP-REAL 2) )
assume x in { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex r, s being Real st
( x = |[r,s]| & (G * (i,1)) `1 <= r ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
hence { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } is Subset of (TOP-REAL 2) ; ::_thesis: verum
end;
assume that
( not 1 <= i or not i < len G ) and
i < len G ; ::_thesis: { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } is Subset of (TOP-REAL 2)
set A = { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } ;
{ |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } or x in the carrier of (TOP-REAL 2) )
assume x in { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex r, s being Real st
( x = |[r,s]| & r <= (G * ((i + 1),1)) `1 ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
hence { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } is Subset of (TOP-REAL 2) ; ::_thesis: verum
end;
correctness
consistency
for b1 being Subset of (TOP-REAL 2) st 1 <= i & i < len G & i >= len G holds
( b1 = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } iff b1 = { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } );
;
func h_strip (G,i) -> Subset of (TOP-REAL 2) equals :Def2: :: GOBOARD5:def 2
{ |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } if ( 1 <= i & i < width G )
{ |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } if i >= width G
otherwise { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } ;
coherence
( ( 1 <= i & i < width G implies { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } is Subset of (TOP-REAL 2) ) & ( i >= width G implies { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < width G ) & not i >= width G implies { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) ) )
proof
hereby ::_thesis: ( ( i >= width G implies { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < width G ) & not i >= width G implies { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) ) )
assume that
1 <= i and
i < width G ; ::_thesis: { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } is Subset of (TOP-REAL 2)
set A = { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } ;
{ |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } or x in the carrier of (TOP-REAL 2) )
assume x in { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex r, s being Real st
( x = |[r,s]| & (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
hence { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } is Subset of (TOP-REAL 2) ; ::_thesis: verum
end;
hereby ::_thesis: ( ( not 1 <= i or not i < width G ) & not i >= width G implies { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) )
assume i >= width G ; ::_thesis: { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } is Subset of (TOP-REAL 2)
set A = { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } ;
{ |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } or x in the carrier of (TOP-REAL 2) )
assume x in { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex r, s being Real st
( x = |[r,s]| & (G * (1,i)) `2 <= s ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
hence { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } is Subset of (TOP-REAL 2) ; ::_thesis: verum
end;
assume that
( not 1 <= i or not i < width G ) and
i < width G ; ::_thesis: { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2)
set A = { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } ;
{ |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } or x in the carrier of (TOP-REAL 2) )
assume x in { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex r, s being Real st
( x = |[r,s]| & s <= (G * (1,(i + 1))) `2 ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
hence { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) ; ::_thesis: verum
end;
correctness
consistency
for b1 being Subset of (TOP-REAL 2) st 1 <= i & i < width G & i >= width G holds
( b1 = { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } iff b1 = { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } );
;
end;
:: deftheorem Def1 defines v_strip GOBOARD5:def_1_:_
for G being Matrix of (TOP-REAL 2)
for i being Nat holds
( ( 1 <= i & i < len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } ) & ( i >= len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } ) & ( ( not 1 <= i or not i < len G ) & not i >= len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } ) );
:: deftheorem Def2 defines h_strip GOBOARD5:def_2_:_
for G being Matrix of (TOP-REAL 2)
for i being Nat holds
( ( 1 <= i & i < width G implies h_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } ) & ( i >= width G implies h_strip (G,i) = { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } ) & ( ( not 1 <= i or not i < width G ) & not i >= width G implies h_strip (G,i) = { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } ) );
theorem Th1: :: GOBOARD5:1
for j, i being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G holds
(G * (i,j)) `2 = (G * (1,j)) `2
proof
let j, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G holds
(G * (i,j)) `2 = (G * (1,j)) `2
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G implies (G * (i,j)) `2 = (G * (1,j)) `2 )
assume that
A1: G is Y_equal-in-column and
A2: 1 <= j and
A3: j <= width G and
A4: 1 <= i and
A5: i <= len G ; ::_thesis: (G * (i,j)) `2 = (G * (1,j)) `2
j in Seg (width G) by A2, A3, FINSEQ_1:1;
then A6: Y_axis (Col (G,j)) is constant by A1, GOBOARD1:def_5;
reconsider c = Col (G,j) as FinSequence of (TOP-REAL 2) ;
A7: i in dom G by A4, A5, FINSEQ_3:25;
A8: 1 <= len G by A4, A5, XXREAL_0:2;
then A9: 1 in dom G by FINSEQ_3:25;
A10: len c = len G by MATRIX_1:def_8;
then 1 in dom c by A8, FINSEQ_3:25;
then A11: c /. 1 = c . 1 by PARTFUN1:def_6;
i in dom c by A4, A5, A10, FINSEQ_3:25;
then A12: c /. i = c . i by PARTFUN1:def_6;
A13: len (Y_axis (Col (G,j))) = len c by GOBOARD1:def_2;
then A14: 1 in dom (Y_axis (Col (G,j))) by A8, A10, FINSEQ_3:25;
A15: i in dom (Y_axis (Col (G,j))) by A4, A5, A10, A13, FINSEQ_3:25;
thus (G * (i,j)) `2 = (c /. i) `2 by A7, A12, MATRIX_1:def_8
.= (Y_axis (Col (G,j))) . i by A15, GOBOARD1:def_2
.= (Y_axis (Col (G,j))) . 1 by A6, A14, A15, SEQM_3:def_10
.= (c /. 1) `2 by A14, GOBOARD1:def_2
.= (G * (1,j)) `2 by A9, A11, MATRIX_1:def_8 ; ::_thesis: verum
end;
theorem Th2: :: GOBOARD5:2
for j, i being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= j & j <= width G & 1 <= i & i <= len G holds
(G * (i,j)) `1 = (G * (i,1)) `1
proof
let j, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= j & j <= width G & 1 <= i & i <= len G holds
(G * (i,j)) `1 = (G * (i,1)) `1
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is X_equal-in-line & 1 <= j & j <= width G & 1 <= i & i <= len G implies (G * (i,j)) `1 = (G * (i,1)) `1 )
assume that
A1: G is X_equal-in-line and
A2: 1 <= j and
A3: j <= width G and
A4: 1 <= i and
A5: i <= len G ; ::_thesis: (G * (i,j)) `1 = (G * (i,1)) `1
i in dom G by A4, A5, FINSEQ_3:25;
then A6: X_axis (Line (G,i)) is constant by A1, GOBOARD1:def_4;
reconsider c = Line (G,i) as FinSequence of (TOP-REAL 2) ;
A7: j in Seg (width G) by A2, A3, FINSEQ_1:1;
A8: 1 <= width G by A2, A3, XXREAL_0:2;
then A9: 1 in Seg (width G) by FINSEQ_1:1;
A10: len c = width G by MATRIX_1:def_7;
then 1 in dom c by A8, FINSEQ_3:25;
then A11: c /. 1 = c . 1 by PARTFUN1:def_6;
j in dom c by A2, A3, A10, FINSEQ_3:25;
then A12: c /. j = c . j by PARTFUN1:def_6;
A13: len (X_axis (Line (G,i))) = len c by GOBOARD1:def_1;
then A14: 1 in dom (X_axis (Line (G,i))) by A8, A10, FINSEQ_3:25;
A15: j in dom (X_axis (Line (G,i))) by A2, A3, A10, A13, FINSEQ_3:25;
thus (G * (i,j)) `1 = (c /. j) `1 by A7, A12, MATRIX_1:def_7
.= (X_axis (Line (G,i))) . j by A15, GOBOARD1:def_1
.= (X_axis (Line (G,i))) . 1 by A6, A14, A15, SEQM_3:def_10
.= (c /. 1) `1 by A14, GOBOARD1:def_1
.= (G * (i,1)) `1 by A9, A11, MATRIX_1:def_7 ; ::_thesis: verum
end;
theorem Th3: :: GOBOARD5:3
for j, i1, i2 being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds
(G * (i1,j)) `1 < (G * (i2,j)) `1
proof
let j, i1, i2 be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds
(G * (i1,j)) `1 < (G * (i2,j)) `1
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G implies (G * (i1,j)) `1 < (G * (i2,j)) `1 )
assume that
A1: G is X_increasing-in-column and
A2: 1 <= j and
A3: j <= width G and
A4: 1 <= i1 and
A5: i1 < i2 and
A6: i2 <= len G ; ::_thesis: (G * (i1,j)) `1 < (G * (i2,j)) `1
j in Seg (width G) by A2, A3, FINSEQ_1:1;
then A7: X_axis (Col (G,j)) is increasing by A1, GOBOARD1:def_7;
reconsider c = Col (G,j) as FinSequence of (TOP-REAL 2) ;
A8: i1 <= len G by A5, A6, XXREAL_0:2;
then A9: i1 in dom G by A4, FINSEQ_3:25;
A10: 1 <= i2 by A4, A5, XXREAL_0:2;
then A11: i2 in dom G by A6, FINSEQ_3:25;
A12: len c = len G by MATRIX_1:def_8;
then i1 in dom c by A4, A8, FINSEQ_3:25;
then A13: c /. i1 = c . i1 by PARTFUN1:def_6;
i2 in dom c by A6, A10, A12, FINSEQ_3:25;
then A14: c /. i2 = c . i2 by PARTFUN1:def_6;
A15: len (X_axis (Col (G,j))) = len c by GOBOARD1:def_1;
then A16: i1 in dom (X_axis (Col (G,j))) by A4, A8, A12, FINSEQ_3:25;
A17: (G * (i1,j)) `1 = (c /. i1) `1 by A9, A13, MATRIX_1:def_8
.= (X_axis (Col (G,j))) . i1 by A16, GOBOARD1:def_1 ;
A18: i2 in dom (X_axis (Col (G,j))) by A6, A10, A12, A15, FINSEQ_3:25;
then (X_axis (Col (G,j))) . i2 = (c /. i2) `1 by GOBOARD1:def_1
.= (G * (i2,j)) `1 by A11, A14, MATRIX_1:def_8 ;
hence (G * (i1,j)) `1 < (G * (i2,j)) `1 by A5, A7, A16, A17, A18, SEQM_3:def_1; ::_thesis: verum
end;
theorem Th4: :: GOBOARD5:4
for j1, j2, i being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is Y_increasing-in-line & 1 <= j1 & j1 < j2 & j2 <= width G & 1 <= i & i <= len G holds
(G * (i,j1)) `2 < (G * (i,j2)) `2
proof
let j1, j2, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is Y_increasing-in-line & 1 <= j1 & j1 < j2 & j2 <= width G & 1 <= i & i <= len G holds
(G * (i,j1)) `2 < (G * (i,j2)) `2
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is Y_increasing-in-line & 1 <= j1 & j1 < j2 & j2 <= width G & 1 <= i & i <= len G implies (G * (i,j1)) `2 < (G * (i,j2)) `2 )
assume that
A1: G is Y_increasing-in-line and
A2: 1 <= j1 and
A3: j1 < j2 and
A4: j2 <= width G and
A5: 1 <= i and
A6: i <= len G ; ::_thesis: (G * (i,j1)) `2 < (G * (i,j2)) `2
i in dom G by A5, A6, FINSEQ_3:25;
then A7: Y_axis (Line (G,i)) is increasing by A1, GOBOARD1:def_6;
reconsider c = Line (G,i) as FinSequence of (TOP-REAL 2) ;
A8: j1 <= width G by A3, A4, XXREAL_0:2;
then A9: j1 in Seg (width G) by A2, FINSEQ_1:1;
A10: 1 <= j2 by A2, A3, XXREAL_0:2;
then A11: j2 in Seg (width G) by A4, FINSEQ_1:1;
A12: len c = width G by MATRIX_1:def_7;
then j1 in dom c by A2, A8, FINSEQ_3:25;
then A13: c /. j1 = c . j1 by PARTFUN1:def_6;
j2 in dom c by A4, A10, A12, FINSEQ_3:25;
then A14: c /. j2 = c . j2 by PARTFUN1:def_6;
A15: len (Y_axis (Line (G,i))) = len c by GOBOARD1:def_2;
then A16: j1 in dom (Y_axis (Line (G,i))) by A2, A8, A12, FINSEQ_3:25;
A17: (G * (i,j1)) `2 = (c /. j1) `2 by A9, A13, MATRIX_1:def_7
.= (Y_axis (Line (G,i))) . j1 by A16, GOBOARD1:def_2 ;
A18: j2 in dom (Y_axis (Line (G,i))) by A4, A10, A12, A15, FINSEQ_3:25;
then (Y_axis (Line (G,i))) . j2 = (c /. j2) `2 by GOBOARD1:def_2
.= (G * (i,j2)) `2 by A11, A14, MATRIX_1:def_7 ;
hence (G * (i,j1)) `2 < (G * (i,j2)) `2 by A3, A7, A16, A17, A18, SEQM_3:def_1; ::_thesis: verum
end;
theorem Th5: :: GOBOARD5:5
for j, i being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G holds
h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }
proof
let j, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G holds
h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G implies h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } )
assume that
A1: G is Y_equal-in-column and
A2: 1 <= j and
A3: j < width G and
A4: 1 <= i and
A5: i <= len G ; ::_thesis: h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }
A6: 1 <= j + 1 by A2, NAT_1:13;
A7: j + 1 <= width G by A3, NAT_1:13;
A8: (G * (i,j)) `2 = (G * (1,j)) `2 by A1, A2, A3, A4, A5, Th1;
(G * (i,(j + 1))) `2 = (G * (1,(j + 1))) `2 by A1, A4, A5, A6, A7, Th1;
hence h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } by A2, A3, A8, Def2; ::_thesis: verum
end;
theorem Th6: :: GOBOARD5:6
for i being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G holds
h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s }
proof
let i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G holds
h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s }
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G implies h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s } )
assume that
A1: ( G is V3() & G is Y_equal-in-column ) and
A2: 1 <= i and
A3: i <= len G ; ::_thesis: h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s }
width G <> 0 by A1, GOBOARD1:def_3;
then 1 <= width G by NAT_1:14;
then (G * (i,(width G))) `2 = (G * (1,(width G))) `2 by A1, A2, A3, Th1;
hence h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s } by Def2; ::_thesis: verum
end;
theorem Th7: :: GOBOARD5:7
for i being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G holds
h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 }
proof
let i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G holds
h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 }
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G implies h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 } )
assume that
A1: ( G is V3() & G is Y_equal-in-column ) and
A2: 1 <= i and
A3: i <= len G ; ::_thesis: h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 }
set A = { |[r,s]| where r, s is Real : (G * (i,1)) `2 >= s } ;
A4: 0 <> width G by A1, GOBOARD1:def_3;
then A5: 0 < width G by NAT_1:3;
1 <= width G by A4, NAT_1:14;
then (G * (i,1)) `2 = (G * (1,1)) `2 by A1, A2, A3, Th1;
then { |[r,s]| where r, s is Real : (G * (i,1)) `2 >= s } = { |[r,s]| where r, s is Real : (G * (1,(1 + 0))) `2 >= s } ;
hence h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 } by A5, Def2; ::_thesis: verum
end;
theorem Th8: :: GOBOARD5:8
for i, j being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= i & i < len G & 1 <= j & j <= width G holds
v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) }
proof
let i, j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= i & i < len G & 1 <= j & j <= width G holds
v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) }
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is X_equal-in-line & 1 <= i & i < len G & 1 <= j & j <= width G implies v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } )
assume that
A1: G is X_equal-in-line and
A2: 1 <= i and
A3: i < len G and
A4: 1 <= j and
A5: j <= width G ; ::_thesis: v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) }
A6: 1 <= i + 1 by A2, NAT_1:13;
A7: i + 1 <= len G by A3, NAT_1:13;
A8: (G * (i,j)) `1 = (G * (i,1)) `1 by A1, A2, A3, A4, A5, Th2;
(G * ((i + 1),j)) `1 = (G * ((i + 1),1)) `1 by A1, A4, A5, A6, A7, Th2;
hence v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } by A2, A3, A8, Def1; ::_thesis: verum
end;
theorem Th9: :: GOBOARD5:9
for j being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds
v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r }
proof
let j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds
v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r }
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is X_equal-in-line & 1 <= j & j <= width G implies v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r } )
assume that
A1: ( G is V3() & G is X_equal-in-line ) and
A2: 1 <= j and
A3: j <= width G ; ::_thesis: v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r }
len G <> 0 by A1, GOBOARD1:def_3;
then 1 <= len G by NAT_1:14;
then (G * ((len G),j)) `1 = (G * ((len G),1)) `1 by A1, A2, A3, Th2;
hence v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r } by Def1; ::_thesis: verum
end;
theorem Th10: :: GOBOARD5:10
for j being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds
v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 }
proof
let j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds
v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 }
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is X_equal-in-line & 1 <= j & j <= width G implies v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 } )
assume that
A1: ( G is V3() & G is X_equal-in-line ) and
A2: 1 <= j and
A3: j <= width G ; ::_thesis: v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 }
set A = { |[r,s]| where r, s is Real : (G * (1,j)) `1 >= r } ;
A4: 0 <> len G by A1, GOBOARD1:def_3;
then A5: 0 < len G by NAT_1:3;
1 <= len G by A4, NAT_1:14;
then (G * (1,j)) `1 = (G * (1,1)) `1 by A1, A2, A3, Th2;
then { |[r,s]| where r, s is Real : (G * (1,j)) `1 >= r } = { |[r,s]| where r, s is Real : (G * (1,(1 + 0))) `1 >= r } ;
hence v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 } by A5, Def1; ::_thesis: verum
end;
definition
let G be Matrix of (TOP-REAL 2);
let i, j be Nat;
func cell (G,i,j) -> Subset of (TOP-REAL 2) equals :: GOBOARD5:def 3
(v_strip (G,i)) /\ (h_strip (G,j));
correctness
coherence
(v_strip (G,i)) /\ (h_strip (G,j)) is Subset of (TOP-REAL 2);
;
end;
:: deftheorem defines cell GOBOARD5:def_3_:_
for G being Matrix of (TOP-REAL 2)
for i, j being Nat holds cell (G,i,j) = (v_strip (G,i)) /\ (h_strip (G,j));
definition
let IT be FinSequence of (TOP-REAL 2);
attrIT is s.c.c. means :: GOBOARD5:def 4
for i, j being Element of NAT st i + 1 < j & ( ( i > 1 & j < len IT ) or j + 1 < len IT ) holds
LSeg (IT,i) misses LSeg (IT,j);
end;
:: deftheorem defines s.c.c. GOBOARD5:def_4_:_
for IT being FinSequence of (TOP-REAL 2) holds
( IT is s.c.c. iff for i, j being Element of NAT st i + 1 < j & ( ( i > 1 & j < len IT ) or j + 1 < len IT ) holds
LSeg (IT,i) misses LSeg (IT,j) );
definition
let IT be non empty FinSequence of (TOP-REAL 2);
attrIT is standard means :Def5: :: GOBOARD5:def 5
IT is_sequence_on GoB IT;
end;
:: deftheorem Def5 defines standard GOBOARD5:def_5_:_
for IT being non empty FinSequence of (TOP-REAL 2) holds
( IT is standard iff IT is_sequence_on GoB IT );
registration
clusterV1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non constant non empty V33() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard for FinSequence of the carrier of (TOP-REAL 2);
existence
ex b1 being non empty FinSequence of (TOP-REAL 2) st
( not b1 is constant & b1 is special & b1 is unfolded & b1 is circular & b1 is s.c.c. & b1 is standard )
proof
set f1 = <*|[0,0]|,|[0,1]|,|[1,1]|*>;
set f2 = <*|[1,0]|,|[0,0]|*>;
A1: len <*|[0,0]|,|[0,1]|,|[1,1]|*> = 3 by FINSEQ_1:45;
A2: len <*|[1,0]|,|[0,0]|*> = 2 by FINSEQ_1:44;
then A3: len (<*|[0,0]|,|[0,1]|,|[1,1]|*> ^ <*|[1,0]|,|[0,0]|*>) = 3 + 2 by A1, FINSEQ_1:22;
reconsider f = <*|[0,0]|,|[0,1]|,|[1,1]|*> ^ <*|[1,0]|,|[0,0]|*> as non empty FinSequence of (TOP-REAL 2) ;
take f ; ::_thesis: ( not f is constant & f is special & f is unfolded & f is circular & f is s.c.c. & f is standard )
A4: 1 in dom <*|[0,0]|,|[0,1]|,|[1,1]|*> by A1, FINSEQ_3:25;
then A5: f /. 1 = <*|[0,0]|,|[0,1]|,|[1,1]|*> /. 1 by FINSEQ_4:68
.= |[0,0]| by FINSEQ_4:18 ;
A6: 2 in dom <*|[0,0]|,|[0,1]|,|[1,1]|*> by A1, FINSEQ_3:25;
then A7: f /. 2 = <*|[0,0]|,|[0,1]|,|[1,1]|*> /. 2 by FINSEQ_4:68
.= |[0,1]| by FINSEQ_4:18 ;
A8: dom <*|[0,0]|,|[0,1]|,|[1,1]|*> c= dom f by FINSEQ_1:26;
then A9: f . 1 = f /. 1 by A4, PARTFUN1:def_6;
f . 2 = f /. 2 by A6, A8, PARTFUN1:def_6;
then f . 1 <> f . 2 by A5, A7, A9, SPPOL_2:1;
hence not f is constant by A4, A6, A8, SEQM_3:def_10; ::_thesis: ( f is special & f is unfolded & f is circular & f is s.c.c. & f is standard )
3 in dom <*|[0,0]|,|[0,1]|,|[1,1]|*> by A1, FINSEQ_3:25;
then A10: f /. 3 = <*|[0,0]|,|[0,1]|,|[1,1]|*> /. 3 by FINSEQ_4:68
.= |[1,1]| by FINSEQ_4:18 ;
1 in dom <*|[1,0]|,|[0,0]|*> by A2, FINSEQ_3:25;
then A11: f /. (3 + 1) = <*|[1,0]|,|[0,0]|*> /. 1 by A1, FINSEQ_4:69
.= |[1,0]| by FINSEQ_4:17 ;
2 in dom <*|[1,0]|,|[0,0]|*> by A2, FINSEQ_3:25;
then A12: f /. (3 + 2) = <*|[1,0]|,|[0,0]|*> /. 2 by A1, FINSEQ_4:69
.= |[0,0]| by FINSEQ_4:17 ;
1 + 1 = 2 ;
then A13: LSeg (f,1) = LSeg (|[0,0]|,|[0,1]|) by A3, A5, A7, TOPREAL1:def_3;
2 + 1 = 3 ;
then A14: LSeg (f,2) = LSeg (|[0,1]|,|[1,1]|) by A3, A7, A10, TOPREAL1:def_3;
A15: LSeg (f,3) = LSeg (|[1,1]|,|[1,0]|) by A3, A10, A11, TOPREAL1:def_3;
4 + 1 = 5 ;
then A16: LSeg (f,4) = LSeg (|[1,0]|,|[0,0]|) by A3, A11, A12, TOPREAL1:def_3;
thus f is special ::_thesis: ( f is unfolded & f is circular & f is s.c.c. & f is standard )
proof
let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
assume 1 <= i ; ::_thesis: ( not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
then 1 + 1 <= i + 1 by XREAL_1:6;
then A17: 1 < i + 1 by XXREAL_0:2;
assume i + 1 <= len f ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
then A18: ( i + 1 = 1 + 1 or i + 1 = 2 + 1 or i + 1 = 3 + 1 or i + 1 = 4 + 1 ) by A3, A17, NAT_1:29;
percases ( i = 1 or i = 2 or i = 3 or i = 4 ) by A18;
supposeA19: i = 1 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
(f /. 1) `1 = 0 by A5, EUCLID:52
.= (f /. (1 + 1)) `1 by A7, EUCLID:52 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A19; ::_thesis: verum
end;
supposeA20: i = 2 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
(f /. 2) `2 = 1 by A7, EUCLID:52
.= (f /. (2 + 1)) `2 by A10, EUCLID:52 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A20; ::_thesis: verum
end;
supposeA21: i = 3 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
(f /. 3) `1 = 1 by A10, EUCLID:52
.= (f /. (3 + 1)) `1 by A11, EUCLID:52 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A21; ::_thesis: verum
end;
supposeA22: i = 4 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
(f /. 4) `2 = 0 by A11, EUCLID:52
.= (f /. (4 + 1)) `2 by A12, EUCLID:52 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A22; ::_thesis: verum
end;
end;
end;
thus f is unfolded ::_thesis: ( f is circular & f is s.c.c. & f is standard )
proof
let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len f or (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} )
assume 1 <= i ; ::_thesis: ( not i + 2 <= len f or (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} )
then A23: 1 + 2 <= i + 2 by XREAL_1:6;
then A24: 2 < i + 2 by XXREAL_0:2;
A25: 1 < i + 2 by A23, XXREAL_0:2;
assume i + 2 <= len f ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
then A26: ( i + 2 = 1 + 2 or i + 2 = 2 + 2 or i + 2 = 3 + 2 ) by A3, A24, A25, NAT_1:29;
percases ( i = 1 or i = 2 or i = 3 ) by A26;
suppose i = 1 ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A5, A7, A14, TOPREAL1:15, TOPREAL1:def_3; ::_thesis: verum
end;
suppose i = 2 ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A7, A10, A15, TOPREAL1:18, TOPREAL1:def_3; ::_thesis: verum
end;
suppose i = 3 ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A10, A11, A16, TOPREAL1:16, TOPREAL1:def_3; ::_thesis: verum
end;
end;
end;
thus f /. 1 = f /. (len f) by A1, A2, A5, A12, FINSEQ_1:22; :: according to FINSEQ_6:def_1 ::_thesis: ( f is s.c.c. & f is standard )
thus f is s.c.c. ::_thesis: f is standard
proof
let i be Element of NAT ; :: according to GOBOARD5:def_4 ::_thesis: for j being Element of NAT st i + 1 < j & ( ( i > 1 & j < len f ) or j + 1 < len f ) holds
LSeg (f,i) misses LSeg (f,j)
let j be Element of NAT ; ::_thesis: ( i + 1 < j & ( ( i > 1 & j < len f ) or j + 1 < len f ) implies LSeg (f,i) misses LSeg (f,j) )
assume that
A27: i + 1 < j and
A28: ( ( i > 1 & j < len f ) or j + 1 < len f ) ; ::_thesis: LSeg (f,i) misses LSeg (f,j)
A29: i + 1 >= 1 by NAT_1:11;
A30: ( j + 1 = 0 + 1 or j + 1 = 1 + 1 or j + 1 = 2 + 1 or j + 1 = 3 + 1 or j + 1 = 4 + 1 ) by A3, A28, NAT_1:29;
A31: (i + 1) + 1 = i + (1 + 1) ;
then A32: i + 2 <= j by A27, NAT_1:13;
A33: ( i + 2 = 2 + 2 implies i = 2 ) ;
A34: ( i + 2 = 1 + 2 implies i = 1 ) ;
A35: ( i + 2 = 0 + 2 implies i = 0 ) ;
A36: i + 2 <> 0 + 1 by A31;
A37: now__::_thesis:_(_(_j_=_2_&_i_=_0_)_or_(_j_=_3_&_(_i_=_0_or_i_=_1_)_)_or_(_j_=_4_&_(_i_=_0_or_i_=_2_)_)_)
percases ( j = 2 or j = 3 or j = 4 ) by A27, A29, A30, XXREAL_0:2;
case j = 2 ; ::_thesis: i = 0
hence i = 0 by A27, A31, A35, NAT_1:26; ::_thesis: verum
end;
case j = 3 ; ::_thesis: ( i = 0 or i = 1 )
hence ( i = 0 or i = 1 ) by A27, A31, A34, A35, NAT_1:27; ::_thesis: verum
end;
case j = 4 ; ::_thesis: ( i = 0 or i = 2 )
hence ( i = 0 or i = 2 ) by A3, A28, A32, A33, A34, A35, A36, NAT_1:28; ::_thesis: verum
end;
end;
end;
percases ( i = 0 or ( i = 1 & j = 3 ) or ( i = 2 & j = 4 ) ) by A37;
suppose i = 0 ; ::_thesis: LSeg (f,i) misses LSeg (f,j)
then LSeg (f,i) = {} by TOPREAL1:def_3;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
suppose ( i = 1 & j = 3 ) ; ::_thesis: LSeg (f,i) misses LSeg (f,j)
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} by A13, A15, TOPREAL1:20, XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
suppose ( i = 2 & j = 4 ) ; ::_thesis: LSeg (f,i) misses LSeg (f,j)
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} by A14, A16, TOPREAL1:19, XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
end;
end;
set Xf1 = <*0,0,1*>;
set Xf2 = <*1,0*>;
reconsider Xf = <*0,0,1*> ^ <*1,0*> as FinSequence of REAL ;
A38: len <*0,0,1*> = 3 by FINSEQ_1:45;
A39: len <*1,0*> = 2 by FINSEQ_1:44;
then A40: len Xf = 3 + 2 by A38, FINSEQ_1:22;
1 in dom <*0,0,1*> by A38, FINSEQ_3:25;
then A41: Xf . 1 = <*0,0,1*> . 1 by FINSEQ_1:def_7
.= 0 by FINSEQ_1:45 ;
2 in dom <*0,0,1*> by A38, FINSEQ_3:25;
then A42: Xf . 2 = <*0,0,1*> . 2 by FINSEQ_1:def_7
.= 0 by FINSEQ_1:45 ;
3 in dom <*0,0,1*> by A38, FINSEQ_3:25;
then A43: Xf . 3 = <*0,0,1*> . 3 by FINSEQ_1:def_7
.= 1 by FINSEQ_1:45 ;
1 in dom <*1,0*> by A39, FINSEQ_3:25;
then A44: Xf . (3 + 1) = <*1,0*> . 1 by A38, FINSEQ_1:def_7
.= 1 by FINSEQ_1:44 ;
2 in dom <*1,0*> by A39, FINSEQ_3:25;
then A45: Xf . (3 + 2) = <*1,0*> . 2 by A38, FINSEQ_1:def_7
.= 0 by FINSEQ_1:44 ;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_Xf_holds_
Xf_._n_=_(f_/._n)_`1
let n be Element of NAT ; ::_thesis: ( n in dom Xf implies Xf . b1 = (f /. b1) `1 )
assume A46: n in dom Xf ; ::_thesis: Xf . b1 = (f /. b1) `1
then A47: n <> 0 by FINSEQ_3:25;
A48: n <= 5 by A40, A46, FINSEQ_3:25;
percases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A47, A48, NAT_1:29;
suppose n = 1 ; ::_thesis: Xf . b1 = (f /. b1) `1
hence Xf . n = (f /. n) `1 by A5, A41, EUCLID:52; ::_thesis: verum
end;
suppose n = 2 ; ::_thesis: Xf . b1 = (f /. b1) `1
hence Xf . n = (f /. n) `1 by A7, A42, EUCLID:52; ::_thesis: verum
end;
suppose n = 3 ; ::_thesis: Xf . b1 = (f /. b1) `1
hence Xf . n = (f /. n) `1 by A10, A43, EUCLID:52; ::_thesis: verum
end;
suppose n = 4 ; ::_thesis: Xf . b1 = (f /. b1) `1
hence Xf . n = (f /. n) `1 by A11, A44, EUCLID:52; ::_thesis: verum
end;
suppose n = 5 ; ::_thesis: Xf . b1 = (f /. b1) `1
hence Xf . n = (f /. n) `1 by A12, A45, EUCLID:52; ::_thesis: verum
end;
end;
end;
then A49: Xf = X_axis f by A3, A40, GOBOARD1:def_1;
A50: rng <*0,0,1*> = {0,0,1} by FINSEQ_2:128
.= {0,1} by ENUMSET1:30 ;
rng <*1,0*> = {0,1} by FINSEQ_2:127;
then A51: rng Xf = {0,1} \/ {0,1} by A50, FINSEQ_1:31
.= {0,1} ;
then A52: rng <*0,1*> = rng Xf by FINSEQ_2:127;
A53: len <*0,1*> = 2 by FINSEQ_1:44
.= card (rng Xf) by A51, CARD_2:57 ;
<*0,1*> is increasing
proof
let n, m be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: ( not n in K83(<*0,1*>) or not m in K83(<*0,1*>) or m <= n or not K441(<*0,1*>,m) <= K441(<*0,1*>,n) )
len <*0,1*> = 2 by FINSEQ_1:44;
then A54: dom <*0,1*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3;
assume that
A55: n in dom <*0,1*> and
A56: m in dom <*0,1*> ; ::_thesis: ( m <= n or not K441(<*0,1*>,m) <= K441(<*0,1*>,n) )
A57: ( n = 1 or n = 2 ) by A54, A55, TARSKI:def_2;
A58: ( m = 1 or m = 2 ) by A54, A56, TARSKI:def_2;
assume A59: n < m ; ::_thesis: not K441(<*0,1*>,m) <= K441(<*0,1*>,n)
then A60: <*0,1*> . n = 0 by A57, A58, FINSEQ_1:44;
<*0,1*> . m = 1 by A57, A58, A59, FINSEQ_1:44;
hence <*0,1*> . n < <*0,1*> . m by A60; ::_thesis: verum
end;
then A61: <*0,1*> = Incr (X_axis f) by A49, A52, A53, SEQ_4:def_21;
set Yf1 = <*0,1,1*>;
set Yf2 = <*0,0*>;
reconsider Yf = <*0,1,1*> ^ <*0,0*> as FinSequence of REAL ;
A62: len <*0,1,1*> = 3 by FINSEQ_1:45;
A63: len <*0,0*> = 2 by FINSEQ_1:44;
then A64: len Yf = 3 + 2 by A62, FINSEQ_1:22;
1 in dom <*0,1,1*> by A62, FINSEQ_3:25;
then A65: Yf . 1 = <*0,1,1*> . 1 by FINSEQ_1:def_7
.= 0 by FINSEQ_1:45 ;
2 in dom <*0,1,1*> by A62, FINSEQ_3:25;
then A66: Yf . 2 = <*0,1,1*> . 2 by FINSEQ_1:def_7
.= 1 by FINSEQ_1:45 ;
3 in dom <*0,1,1*> by A62, FINSEQ_3:25;
then A67: Yf . 3 = <*0,1,1*> . 3 by FINSEQ_1:def_7
.= 1 by FINSEQ_1:45 ;
1 in dom <*0,0*> by A63, FINSEQ_3:25;
then A68: Yf . (3 + 1) = <*0,0*> . 1 by A62, FINSEQ_1:def_7
.= 0 by FINSEQ_1:44 ;
2 in dom <*0,0*> by A63, FINSEQ_3:25;
then A69: Yf . (3 + 2) = <*0,0*> . 2 by A62, FINSEQ_1:def_7
.= 0 by FINSEQ_1:44 ;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_Yf_holds_
Yf_._n_=_(f_/._n)_`2
let n be Element of NAT ; ::_thesis: ( n in dom Yf implies Yf . b1 = (f /. b1) `2 )
assume A70: n in dom Yf ; ::_thesis: Yf . b1 = (f /. b1) `2
then A71: n <> 0 by FINSEQ_3:25;
A72: n <= 5 by A64, A70, FINSEQ_3:25;
percases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A71, A72, NAT_1:29;
suppose n = 1 ; ::_thesis: Yf . b1 = (f /. b1) `2
hence Yf . n = (f /. n) `2 by A5, A65, EUCLID:52; ::_thesis: verum
end;
suppose n = 2 ; ::_thesis: Yf . b1 = (f /. b1) `2
hence Yf . n = (f /. n) `2 by A7, A66, EUCLID:52; ::_thesis: verum
end;
suppose n = 3 ; ::_thesis: Yf . b1 = (f /. b1) `2
hence Yf . n = (f /. n) `2 by A10, A67, EUCLID:52; ::_thesis: verum
end;
suppose n = 4 ; ::_thesis: Yf . b1 = (f /. b1) `2
hence Yf . n = (f /. n) `2 by A11, A68, EUCLID:52; ::_thesis: verum
end;
suppose n = 5 ; ::_thesis: Yf . b1 = (f /. b1) `2
hence Yf . n = (f /. n) `2 by A12, A69, EUCLID:52; ::_thesis: verum
end;
end;
end;
then A73: Yf = Y_axis f by A3, A64, GOBOARD1:def_2;
A74: rng <*0,1,1*> = {0,1,1} by FINSEQ_2:128
.= {1,1,0} by ENUMSET1:59
.= {0,1} by ENUMSET1:30 ;
rng <*0,0*> = {0,0} by FINSEQ_2:127
.= {0} by ENUMSET1:29 ;
then A75: rng Yf = {0,1} \/ {0} by A74, FINSEQ_1:31
.= {0,0,1} by ENUMSET1:2
.= {0,1} by ENUMSET1:30 ;
then A76: rng <*0,1*> = rng Yf by FINSEQ_2:127;
A77: len <*0,1*> = 2 by FINSEQ_1:44
.= card (rng Yf) by A75, CARD_2:57 ;
<*0,1*> is increasing
proof
let n, m be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: ( not n in K83(<*0,1*>) or not m in K83(<*0,1*>) or m <= n or not K441(<*0,1*>,m) <= K441(<*0,1*>,n) )
len <*0,1*> = 2 by FINSEQ_1:44;
then A78: dom <*0,1*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3;
assume that
A79: n in dom <*0,1*> and
A80: m in dom <*0,1*> ; ::_thesis: ( m <= n or not K441(<*0,1*>,m) <= K441(<*0,1*>,n) )
A81: ( n = 1 or n = 2 ) by A78, A79, TARSKI:def_2;
A82: ( m = 1 or m = 2 ) by A78, A80, TARSKI:def_2;
assume A83: n < m ; ::_thesis: not K441(<*0,1*>,m) <= K441(<*0,1*>,n)
then A84: <*0,1*> . n = 0 by A81, A82, FINSEQ_1:44;
<*0,1*> . m = 1 by A81, A82, A83, FINSEQ_1:44;
hence <*0,1*> . n < <*0,1*> . m by A84; ::_thesis: verum
end;
then A85: <*0,1*> = Incr (Y_axis f) by A73, A76, A77, SEQ_4:def_21;
set M = (|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|);
A86: len ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) = 2 by MATRIX_2:3
.= len (Incr (X_axis f)) by A61, FINSEQ_1:44 ;
A87: width ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) = 2 by MATRIX_2:3
.= len (Incr (Y_axis f)) by A85, FINSEQ_1:44 ;
for n, m being Element of NAT st [n,m] in Indices ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) holds
((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
proof
let n, m be Element of NAT ; ::_thesis: ( [n,m] in Indices ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) implies ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| )
assume [n,m] in Indices ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) ; ::_thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then [n,m] in [:{1,2},{1,2}:] by FINSEQ_1:2, MATRIX_2:3;
then A88: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by MCART_1:23;
A89: <*0,1*> . 1 = 0 by FINSEQ_1:44;
A90: <*0,1*> . 2 = 1 by FINSEQ_1:44;
percases ( [n,m] = [1,1] or [n,m] = [1,2] or [n,m] = [2,1] or [n,m] = [2,2] ) by A88, ENUMSET1:def_2;
supposeA91: [n,m] = [1,1] ; ::_thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A92: n = 1 by XTUPLE_0:1;
m = 1 by A91, XTUPLE_0:1;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A61, A85, A89, A92, MATRIX_2:6; ::_thesis: verum
end;
supposeA93: [n,m] = [1,2] ; ::_thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A94: n = 1 by XTUPLE_0:1;
m = 2 by A93, XTUPLE_0:1;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A61, A85, A89, A90, A94, MATRIX_2:6; ::_thesis: verum
end;
supposeA95: [n,m] = [2,1] ; ::_thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A96: n = 2 by XTUPLE_0:1;
m = 1 by A95, XTUPLE_0:1;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A61, A85, A89, A90, A96, MATRIX_2:6; ::_thesis: verum
end;
supposeA97: [n,m] = [2,2] ; ::_thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A98: n = 2 by XTUPLE_0:1;
m = 2 by A97, XTUPLE_0:1;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A61, A85, A90, A98, MATRIX_2:6; ::_thesis: verum
end;
end;
end;
then A99: (|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|) = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by A86, A87, GOBOARD2:def_1
.= GoB f by GOBOARD2:def_2 ;
then A100: f /. 1 = (GoB f) * (1,1) by A5, MATRIX_2:6;
A101: f /. 2 = (GoB f) * (1,2) by A7, A99, MATRIX_2:6;
A102: f /. 3 = (GoB f) * (2,2) by A10, A99, MATRIX_2:6;
A103: f /. 4 = (GoB f) * (2,1) by A11, A99, MATRIX_2:6;
thus for k being Element of NAT st k in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) :: according to GOBOARD1:def_9,GOBOARD5:def_5 ::_thesis: for b1 being Element of NAT holds
( not b1 in dom f or not b1 + 1 in dom f or for b2, b3, b4, b5 being Element of NAT holds
( not [b2,b3] in Indices (GoB f) or not [b4,b5] in Indices (GoB f) or not f /. b1 = (GoB f) * (b2,b3) or not f /. (b1 + 1) = (GoB f) * (b4,b5) or (abs (b2 - b4)) + (abs (b3 - b5)) = 1 ) )
proof
let k be Element of NAT ; ::_thesis: ( k in dom f implies ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) )
assume A104: k in dom f ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
then A105: k <= 5 by A3, FINSEQ_3:25;
A106: k <> 0 by A104, FINSEQ_3:25;
percases ( k = 1 or k = 2 or k = 3 or k = 4 or k = 5 ) by A105, A106, NAT_1:29;
supposeA107: k = 1 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
take 1 ; ::_thesis: ex j being Element of NAT st
( [1,j] in Indices (GoB f) & f /. k = (GoB f) * (1,j) )
take 1 ; ::_thesis: ( [1,1] in Indices (GoB f) & f /. k = (GoB f) * (1,1) )
thus [1,1] in Indices (GoB f) by A99, MATRIX_2:4; ::_thesis: f /. k = (GoB f) * (1,1)
thus f /. k = (GoB f) * (1,1) by A5, A99, A107, MATRIX_2:6; ::_thesis: verum
end;
supposeA108: k = 2 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
take 1 ; ::_thesis: ex j being Element of NAT st
( [1,j] in Indices (GoB f) & f /. k = (GoB f) * (1,j) )
take 2 ; ::_thesis: ( [1,2] in Indices (GoB f) & f /. k = (GoB f) * (1,2) )
thus [1,2] in Indices (GoB f) by A99, MATRIX_2:4; ::_thesis: f /. k = (GoB f) * (1,2)
thus f /. k = (GoB f) * (1,2) by A7, A99, A108, MATRIX_2:6; ::_thesis: verum
end;
supposeA109: k = 3 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
take 2 ; ::_thesis: ex j being Element of NAT st
( [2,j] in Indices (GoB f) & f /. k = (GoB f) * (2,j) )
take 2 ; ::_thesis: ( [2,2] in Indices (GoB f) & f /. k = (GoB f) * (2,2) )
thus [2,2] in Indices (GoB f) by A99, MATRIX_2:4; ::_thesis: f /. k = (GoB f) * (2,2)
thus f /. k = (GoB f) * (2,2) by A10, A99, A109, MATRIX_2:6; ::_thesis: verum
end;
supposeA110: k = 4 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
take 2 ; ::_thesis: ex j being Element of NAT st
( [2,j] in Indices (GoB f) & f /. k = (GoB f) * (2,j) )
take 1 ; ::_thesis: ( [2,1] in Indices (GoB f) & f /. k = (GoB f) * (2,1) )
thus [2,1] in Indices (GoB f) by A99, MATRIX_2:4; ::_thesis: f /. k = (GoB f) * (2,1)
thus f /. k = (GoB f) * (2,1) by A11, A99, A110, MATRIX_2:6; ::_thesis: verum
end;
supposeA111: k = 5 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
take 1 ; ::_thesis: ex j being Element of NAT st
( [1,j] in Indices (GoB f) & f /. k = (GoB f) * (1,j) )
take 1 ; ::_thesis: ( [1,1] in Indices (GoB f) & f /. k = (GoB f) * (1,1) )
thus [1,1] in Indices (GoB f) by A99, MATRIX_2:4; ::_thesis: f /. k = (GoB f) * (1,1)
thus f /. k = (GoB f) * (1,1) by A12, A99, A111, MATRIX_2:6; ::_thesis: verum
end;
end;
end;
let n be Element of NAT ; ::_thesis: ( not n in dom f or not n + 1 in dom f or for b1, b2, b3, b4 being Element of NAT holds
( not [b1,b2] in Indices (GoB f) or not [b3,b4] in Indices (GoB f) or not f /. n = (GoB f) * (b1,b2) or not f /. (n + 1) = (GoB f) * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 ) )
assume that
A112: n in dom f and
A113: n + 1 in dom f ; ::_thesis: for b1, b2, b3, b4 being Element of NAT holds
( not [b1,b2] in Indices (GoB f) or not [b3,b4] in Indices (GoB f) or not f /. n = (GoB f) * (b1,b2) or not f /. (n + 1) = (GoB f) * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 )
let m, k, i, j be Element of NAT ; ::_thesis: ( not [m,k] in Indices (GoB f) or not [i,j] in Indices (GoB f) or not f /. n = (GoB f) * (m,k) or not f /. (n + 1) = (GoB f) * (i,j) or (abs (m - i)) + (abs (k - j)) = 1 )
assume that
A114: [m,k] in Indices (GoB f) and
A115: [i,j] in Indices (GoB f) and
A116: f /. n = (GoB f) * (m,k) and
A117: f /. (n + 1) = (GoB f) * (i,j) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
A118: n <> 0 by A112, FINSEQ_3:25;
n + 1 <= 4 + 1 by A3, A113, FINSEQ_3:25;
then A119: n <= 4 by XREAL_1:6;
percases ( n = 1 or n = 2 or n = 3 or n = 4 ) by A118, A119, NAT_1:28;
supposeA120: n = 1 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
A121: [1,1] in Indices (GoB f) by A99, MATRIX_2:4;
then A122: m = 1 by A100, A114, A116, A120, GOBOARD1:5;
A123: k = 1 by A100, A114, A116, A120, A121, GOBOARD1:5;
A124: [1,2] in Indices (GoB f) by A99, MATRIX_2:4;
then A125: i = 1 by A101, A115, A117, A120, GOBOARD1:5;
j = 1 + 1 by A101, A115, A117, A120, A124, GOBOARD1:5;
then abs (k - j) = 1 by A123, SEQM_3:41;
hence (abs (m - i)) + (abs (k - j)) = 1 by A122, A125, SEQM_3:42; ::_thesis: verum
end;
supposeA126: n = 2 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
A127: [1,2] in Indices (GoB f) by A99, MATRIX_2:4;
then A128: m = 1 by A101, A114, A116, A126, GOBOARD1:5;
A129: k = 2 by A101, A114, A116, A126, A127, GOBOARD1:5;
A130: [2,2] in Indices (GoB f) by A99, MATRIX_2:4;
then A131: i = 1 + 1 by A102, A115, A117, A126, GOBOARD1:5;
A132: j = 2 by A102, A115, A117, A126, A130, GOBOARD1:5;
abs (m - i) = 1 by A128, A131, SEQM_3:41;
hence (abs (m - i)) + (abs (k - j)) = 1 by A129, A132, SEQM_3:42; ::_thesis: verum
end;
supposeA133: n = 3 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
A134: [2,2] in Indices (GoB f) by A99, MATRIX_2:4;
then A135: m = 2 by A102, A114, A116, A133, GOBOARD1:5;
A136: k = 1 + 1 by A102, A114, A116, A133, A134, GOBOARD1:5;
A137: [2,1] in Indices (GoB f) by A99, MATRIX_2:4;
then A138: i = 2 by A103, A115, A117, A133, GOBOARD1:5;
j = 1 by A103, A115, A117, A133, A137, GOBOARD1:5;
then abs (k - j) = 1 by A136, SEQM_3:41;
hence (abs (m - i)) + (abs (k - j)) = 1 by A135, A138, SEQM_3:42; ::_thesis: verum
end;
supposeA139: n = 4 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
A140: [2,1] in Indices (GoB f) by A99, MATRIX_2:4;
then A141: m = 1 + 1 by A103, A114, A116, A139, GOBOARD1:5;
A142: k = 1 by A103, A114, A116, A139, A140, GOBOARD1:5;
A143: [1,1] in Indices (GoB f) by A99, MATRIX_2:4;
then A144: i = 1 by A5, A12, A100, A115, A117, A139, GOBOARD1:5;
A145: j = 1 by A5, A12, A100, A115, A117, A139, A143, GOBOARD1:5;
abs (m - i) = 1 by A141, A144, SEQM_3:41;
hence (abs (m - i)) + (abs (k - j)) = 1 by A142, A145, SEQM_3:42; ::_thesis: verum
end;
end;
end;
end;
Lm1: for f being FinSequence of (TOP-REAL 2) holds dom (X_axis f) = dom f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: dom (X_axis f) = dom f
len (X_axis f) = len f by GOBOARD1:def_1;
hence dom (X_axis f) = dom f by FINSEQ_3:29; ::_thesis: verum
end;
Lm2: for f being FinSequence of (TOP-REAL 2) holds dom (Y_axis f) = dom f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: dom (Y_axis f) = dom f
len (Y_axis f) = len f by GOBOARD1:def_2;
hence dom (Y_axis f) = dom f by FINSEQ_3:29; ::_thesis: verum
end;
theorem Th11: :: GOBOARD5:11
for f being non empty FinSequence of (TOP-REAL 2)
for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
let n be Element of NAT ; ::_thesis: ( n in dom f implies ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) )
assume A1: n in dom f ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
A2: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def_2;
set x = (f /. n) `1 ;
set y = (f /. n) `2 ;
A3: n in dom (X_axis f) by A1, Lm1;
then (X_axis f) . n = (f /. n) `1 by GOBOARD1:def_1;
then (f /. n) `1 in rng (X_axis f) by A3, FUNCT_1:def_3;
then (f /. n) `1 in rng (Incr (X_axis f)) by SEQ_4:def_21;
then consider i being Nat such that
A4: i in dom (Incr (X_axis f)) and
A5: (Incr (X_axis f)) . i = (f /. n) `1 by FINSEQ_2:10;
A6: n in dom (Y_axis f) by A1, Lm2;
then (Y_axis f) . n = (f /. n) `2 by GOBOARD1:def_2;
then (f /. n) `2 in rng (Y_axis f) by A6, FUNCT_1:def_3;
then (f /. n) `2 in rng (Incr (Y_axis f)) by SEQ_4:def_21;
then consider j being Nat such that
A7: j in dom (Incr (Y_axis f)) and
A8: (Incr (Y_axis f)) . j = (f /. n) `2 by FINSEQ_2:10;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def_12;
take i ; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
take j ; ::_thesis: ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
i in Seg (len (Incr (X_axis f))) by A4, FINSEQ_1:def_3;
then i in Seg (len (GoB ((Incr (X_axis f)),(Incr (Y_axis f))))) by GOBOARD2:def_1;
then A9: i in dom (GoB f) by A2, FINSEQ_1:def_3;
j in Seg (len (Incr (Y_axis f))) by A7, FINSEQ_1:def_3;
then j in Seg (width (GoB ((Incr (X_axis f)),(Incr (Y_axis f))))) by GOBOARD2:def_1;
then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A2, A9, ZFMISC_1:87;
hence A10: [i,j] in Indices (GoB f) by MATRIX_1:def_4; ::_thesis: f /. n = (GoB f) * (i,j)
thus f /. n = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A5, A8, EUCLID:53
.= (GoB f) * (i,j) by A2, A10, GOBOARD2:def_1 ; ::_thesis: verum
end;
theorem Th12: :: GOBOARD5:12
for f being non empty standard FinSequence of (TOP-REAL 2)
for n being Element of NAT st n in dom f & n + 1 in dom f holds
for m, k, i, j being Element of NAT st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1
proof
let f be non empty standard FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st n in dom f & n + 1 in dom f holds
for m, k, i, j being Element of NAT st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1
let n be Element of NAT ; ::_thesis: ( n in dom f & n + 1 in dom f implies for m, k, i, j being Element of NAT st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 )
assume that
A1: n in dom f and
A2: n + 1 in dom f ; ::_thesis: for m, k, i, j being Element of NAT st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1
f is_sequence_on GoB f by Def5;
hence for m, k, i, j being Element of NAT st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A1, A2, GOBOARD1:def_9; ::_thesis: verum
end;
definition
mode special_circular_sequence is non empty circular special unfolded s.c.c. FinSequence of (TOP-REAL 2);
end;
definition
let f be standard special_circular_sequence;
let k be Element of NAT ;
assume that
A1: 1 <= k and
A2: k + 1 <= len f ;
k <= k + 1 by NAT_1:11;
then k <= len f by A2, XXREAL_0:2;
then A3: k in dom f by A1, FINSEQ_3:25;
then consider i1, j1 being Element of NAT such that
A4: [i1,j1] in Indices (GoB f) and
A5: f /. k = (GoB f) * (i1,j1) by Th11;
k + 1 >= 1 by NAT_1:11;
then A6: k + 1 in dom f by A2, FINSEQ_3:25;
then consider i2, j2 being Element of NAT such that
A7: [i2,j2] in Indices (GoB f) and
A8: f /. (k + 1) = (GoB f) * (i2,j2) by Th11;
A9: (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A4, A5, A6, A7, A8, Th12;
A10: now__::_thesis:_(_(_abs_(i1_-_i2)_=_1_&_j1_=_j2_&_(_i1_=_i2_+_1_or_i1_+_1_=_i2_)_&_j1_=_j2_)_or_(_i1_=_i2_&_abs_(j1_-_j2)_=_1_&_(_j1_=_j2_+_1_or_j1_+_1_=_j2_)_&_i1_=_i2_)_)
percases ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( i1 = i2 & abs (j1 - j2) = 1 ) ) by A9, SEQM_3:42;
casethat A11: abs (i1 - i2) = 1 and
A12: j1 = j2 ; ::_thesis: ( ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 )
( i1 - i2 = 1 or - (i1 - i2) = 1 ) by A11, ABSVALUE:def_1;
hence ( i1 = i2 + 1 or i1 + 1 = i2 ) ; ::_thesis: j1 = j2
thus j1 = j2 by A12; ::_thesis: verum
end;
casethat A13: i1 = i2 and
A14: abs (j1 - j2) = 1 ; ::_thesis: ( ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 )
( j1 - j2 = 1 or - (j1 - j2) = 1 ) by A14, ABSVALUE:def_1;
hence ( j1 = j2 + 1 or j1 + 1 = j2 ) ; ::_thesis: i1 = i2
thus i1 = i2 by A13; ::_thesis: verum
end;
end;
end;
func right_cell (f,k) -> Subset of (TOP-REAL 2) means :Def6: :: GOBOARD5:def 6
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & it = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & it = cell ((GoB f),(i1 -' 1),j2) );
existence
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) )
proof
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10;
supposeA15: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) )
take cell ((GoB f),i1,j1) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),i1,j1) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),i1,j1) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),i1,j1) = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),(i1 -' 1),j2) )
let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j29) ) )
assume that
A16: [i19,j19] in Indices (GoB f) and
A17: [i29,j29] in Indices (GoB f) and
A18: f /. k = (GoB f) * (i19,j19) and
A19: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j29) ) )
A20: i1 = i19 by A4, A5, A16, A18, GOBOARD1:5;
j1 = j19 by A4, A5, A16, A18, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j29) ) ) by A7, A8, A15, A17, A19, A20, GOBOARD1:5; ::_thesis: verum
end;
supposeA21: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) )
take cell ((GoB f),i1,(j1 -' 1)) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),(i1 -' 1),j2) )
let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),(i19 -' 1),j29) ) )
assume that
A22: [i19,j19] in Indices (GoB f) and
A23: [i29,j29] in Indices (GoB f) and
A24: f /. k = (GoB f) * (i19,j19) and
A25: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),(i19 -' 1),j29) ) )
A26: i1 = i19 by A4, A5, A22, A24, GOBOARD1:5;
j1 = j19 by A4, A5, A22, A24, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),(i19 -' 1),j29) ) ) by A7, A8, A21, A23, A25, A26, GOBOARD1:5; ::_thesis: verum
end;
supposeA27: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) )
take cell ((GoB f),i2,j2) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),i2,j2) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),i2,j2) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),i2,j2) = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),i2,j2) = cell ((GoB f),(i1 -' 1),j2) )
let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,j2) = cell ((GoB f),(i19 -' 1),j29) ) )
assume that
A28: [i19,j19] in Indices (GoB f) and
A29: [i29,j29] in Indices (GoB f) and
A30: f /. k = (GoB f) * (i19,j19) and
A31: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,j2) = cell ((GoB f),(i19 -' 1),j29) ) )
A32: i2 = i29 by A7, A8, A29, A31, GOBOARD1:5;
j1 = j19 by A4, A5, A28, A30, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,j2) = cell ((GoB f),(i19 -' 1),j29) ) ) by A4, A5, A7, A8, A27, A28, A29, A30, A31, A32, GOBOARD1:5; ::_thesis: verum
end;
supposeA33: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) )
take cell ((GoB f),(i1 -' 1),j2) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),(i1 -' 1),j2) )
let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),(i19 -' 1),j29) ) )
assume that
A34: [i19,j19] in Indices (GoB f) and
A35: [i29,j29] in Indices (GoB f) and
A36: f /. k = (GoB f) * (i19,j19) and
A37: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),(i19 -' 1),j29) ) )
A38: i1 = i19 by A4, A5, A34, A36, GOBOARD1:5;
j1 = j19 by A4, A5, A34, A36, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),(i19 -' 1),j29) ) ) by A7, A8, A33, A35, A37, A38, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) ) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b2 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell ((GoB f),(i1 -' 1),j2) ) ) holds
b1 = b2
proof
let P1, P2 be Subset of (TOP-REAL 2); ::_thesis: ( ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & P1 = cell ((GoB f),(i1 -' 1),j2) ) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P2 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & P2 = cell ((GoB f),(i1 -' 1),j2) ) ) implies P1 = P2 )
assume that
A39: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & P1 = cell ((GoB f),(i1 -' 1),j2) ) and
A40: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P2 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & P2 = cell ((GoB f),(i1 -' 1),j2) ) ; ::_thesis: P1 = P2
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10;
suppose ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: P1 = P2
then A41: j1 < j2 by XREAL_1:29;
A42: j2 <= j2 + 1 by NAT_1:11;
hence P1 = cell ((GoB f),i1,j1) by A4, A5, A7, A8, A39, A41
.= P2 by A4, A5, A7, A8, A40, A41, A42 ;
::_thesis: verum
end;
suppose ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: P1 = P2
then A43: i1 < i2 by XREAL_1:29;
A44: i2 <= i2 + 1 by NAT_1:11;
hence P1 = cell ((GoB f),i1,(j1 -' 1)) by A4, A5, A7, A8, A39, A43
.= P2 by A4, A5, A7, A8, A40, A43, A44 ;
::_thesis: verum
end;
suppose ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: P1 = P2
then A45: i2 < i1 by XREAL_1:29;
A46: i1 <= i1 + 1 by NAT_1:11;
hence P1 = cell ((GoB f),i2,j2) by A4, A5, A7, A8, A39, A45
.= P2 by A4, A5, A7, A8, A40, A45, A46 ;
::_thesis: verum
end;
suppose ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: P1 = P2
then A47: j2 < j1 by XREAL_1:29;
A48: j1 <= j1 + 1 by NAT_1:11;
hence P1 = cell ((GoB f),(i1 -' 1),j2) by A4, A5, A7, A8, A39, A47
.= P2 by A4, A5, A7, A8, A40, A47, A48 ;
::_thesis: verum
end;
end;
end;
func left_cell (f,k) -> Subset of (TOP-REAL 2) means :Def7: :: GOBOARD5:def 7
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & it = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & it = cell ((GoB f),i1,j2) );
existence
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) )
proof
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10;
supposeA49: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) )
take cell ((GoB f),(i1 -' 1),j1) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i1,j2) )
let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),(i19 -' 1),j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i19,j19) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i29,(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i19,j29) ) )
assume that
A50: [i19,j19] in Indices (GoB f) and
A51: [i29,j29] in Indices (GoB f) and
A52: f /. k = (GoB f) * (i19,j19) and
A53: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i19,j29) ) )
A54: i1 = i19 by A4, A5, A50, A52, GOBOARD1:5;
j1 = j19 by A4, A5, A50, A52, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i19,j29) ) ) by A7, A8, A49, A51, A53, A54, GOBOARD1:5; ::_thesis: verum
end;
supposeA55: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) )
take cell ((GoB f),i1,j1) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),i1,j1) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),i1,j1) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),i1,j1) = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),i1,j2) )
let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j29) ) )
assume that
A56: [i19,j19] in Indices (GoB f) and
A57: [i29,j29] in Indices (GoB f) and
A58: f /. k = (GoB f) * (i19,j19) and
A59: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j29) ) )
A60: i1 = i19 by A4, A5, A56, A58, GOBOARD1:5;
j1 = j19 by A4, A5, A56, A58, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j29) ) ) by A7, A8, A55, A57, A59, A60, GOBOARD1:5; ::_thesis: verum
end;
supposeA61: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) )
take cell ((GoB f),i2,(j2 -' 1)) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i1,j2) )
let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),(i19 -' 1),j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i19,j19) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i29,(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i19,j29) ) )
assume that
A62: [i19,j19] in Indices (GoB f) and
A63: [i29,j29] in Indices (GoB f) and
A64: f /. k = (GoB f) * (i19,j19) and
A65: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i19,j29) ) )
A66: i2 = i29 by A7, A8, A63, A65, GOBOARD1:5;
j1 = j19 by A4, A5, A62, A64, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i19,j29) ) ) by A4, A5, A7, A8, A61, A62, A63, A64, A65, A66, GOBOARD1:5; ::_thesis: verum
end;
supposeA67: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) )
take cell ((GoB f),i1,j2) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),i1,j2) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),i1,j2) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),i1,j2) = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),i1,j2) = cell ((GoB f),i1,j2) )
let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),(i19 -' 1),j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),i19,j19) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),i29,(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j2) = cell ((GoB f),i19,j29) ) )
assume that
A68: [i19,j19] in Indices (GoB f) and
A69: [i29,j29] in Indices (GoB f) and
A70: f /. k = (GoB f) * (i19,j19) and
A71: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j2) = cell ((GoB f),i19,j29) ) )
A72: i1 = i19 by A4, A5, A68, A70, GOBOARD1:5;
j1 = j19 by A4, A5, A68, A70, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j2) = cell ((GoB f),i19,j29) ) ) by A7, A8, A67, A69, A71, A72, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) ) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b2 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell ((GoB f),i1,j2) ) ) holds
b1 = b2
proof
let P1, P2 be Subset of (TOP-REAL 2); ::_thesis: ( ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & P1 = cell ((GoB f),i1,j2) ) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P2 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & P2 = cell ((GoB f),i1,j2) ) ) implies P1 = P2 )
assume that
A73: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & P1 = cell ((GoB f),i1,j2) ) and
A74: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P2 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & P2 = cell ((GoB f),i1,j2) ) ; ::_thesis: P1 = P2
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10;
suppose ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: P1 = P2
then A75: j1 < j2 by XREAL_1:29;
A76: j2 <= j2 + 1 by NAT_1:11;
hence P1 = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A7, A8, A73, A75
.= P2 by A4, A5, A7, A8, A74, A75, A76 ;
::_thesis: verum
end;
suppose ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: P1 = P2
then A77: i1 < i2 by XREAL_1:29;
A78: i2 <= i2 + 1 by NAT_1:11;
hence P1 = cell ((GoB f),i1,j1) by A4, A5, A7, A8, A73, A77
.= P2 by A4, A5, A7, A8, A74, A77, A78 ;
::_thesis: verum
end;
suppose ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: P1 = P2
then A79: i2 < i1 by XREAL_1:29;
A80: i1 <= i1 + 1 by NAT_1:11;
hence P1 = cell ((GoB f),i2,(j2 -' 1)) by A4, A5, A7, A8, A73, A79
.= P2 by A4, A5, A7, A8, A74, A79, A80 ;
::_thesis: verum
end;
suppose ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: P1 = P2
then A81: j2 < j1 by XREAL_1:29;
A82: j1 <= j1 + 1 by NAT_1:11;
hence P1 = cell ((GoB f),i1,j2) by A4, A5, A7, A8, A73, A81
.= P2 by A4, A5, A7, A8, A74, A81, A82 ;
::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def6 defines right_cell GOBOARD5:def_6_:_
for f being standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
for b3 being Subset of (TOP-REAL 2) holds
( b3 = right_cell (f,k) iff for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b3 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b3 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b3 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b3 = cell ((GoB f),(i1 -' 1),j2) ) );
:: deftheorem Def7 defines left_cell GOBOARD5:def_7_:_
for f being standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
for b3 being Subset of (TOP-REAL 2) holds
( b3 = left_cell (f,k) iff for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b3 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b3 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b3 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b3 = cell ((GoB f),i1,j2) ) );
theorem Th13: :: GOBOARD5:13
for i, j being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i < len G & 1 <= j & j < width G holds
LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i)
proof
let i, j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i < len G & 1 <= j & j < width G holds
LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i)
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i < len G & 1 <= j & j < width G implies LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i) )
assume that
A1: G is V3() and
A2: G is X_equal-in-line and
A3: G is X_increasing-in-column and
A4: i < len G and
A5: 1 <= j and
A6: j < width G ; ::_thesis: LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i)
A7: 1 <= j + 1 by A5, NAT_1:13;
A8: j + 1 <= width G by A6, NAT_1:13;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) or x in v_strip (G,i) )
assume A9: x in LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) ; ::_thesis: x in v_strip (G,i)
then reconsider p = x as Point of (TOP-REAL 2) ;
A10: p = |[(p `1),(p `2)]| by EUCLID:53;
A11: 1 <= i + 1 by NAT_1:11;
A12: i + 1 <= len G by A4, NAT_1:13;
then A13: (G * ((i + 1),j)) `1 = (G * ((i + 1),1)) `1 by A2, A5, A6, A11, Th2
.= (G * ((i + 1),(j + 1))) `1 by A2, A7, A8, A11, A12, Th2 ;
now__::_thesis:_x_in_v_strip_(G,i)
percases ( i = 0 or i > 0 ) by NAT_1:3;
supposeA14: i = 0 ; ::_thesis: x in v_strip (G,i)
then p `1 <= (G * (1,j)) `1 by A9, A13, TOPREAL1:3;
then p in { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 } by A10;
hence x in v_strip (G,i) by A1, A2, A5, A6, A14, Th10; ::_thesis: verum
end;
suppose i > 0 ; ::_thesis: x in v_strip (G,i)
then A15: 0 + 1 <= i by NAT_1:13;
A16: (G * ((i + 1),j)) `1 <= p `1 by A9, A13, TOPREAL1:3;
A17: p `1 <= (G * ((i + 1),j)) `1 by A9, A13, TOPREAL1:3;
then A18: p `1 = (G * ((i + 1),j)) `1 by A16, XXREAL_0:1;
i < i + 1 by XREAL_1:29;
then (G * (i,j)) `1 < p `1 by A3, A5, A6, A12, A15, A18, Th3;
then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } by A10, A17;
hence x in v_strip (G,i) by A2, A4, A5, A6, A15, Th8; ::_thesis: verum
end;
end;
end;
hence x in v_strip (G,i) ; ::_thesis: verum
end;
theorem Th14: :: GOBOARD5:14
for i, j being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & 1 <= i & i <= len G & 1 <= j & j < width G holds
LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i)
proof
let i, j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & 1 <= i & i <= len G & 1 <= j & j < width G holds
LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i)
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is X_equal-in-line & G is X_increasing-in-column & 1 <= i & i <= len G & 1 <= j & j < width G implies LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i) )
assume that
A1: G is V3() and
A2: G is X_equal-in-line and
A3: G is X_increasing-in-column and
A4: 1 <= i and
A5: i <= len G and
A6: 1 <= j and
A7: j < width G ; ::_thesis: LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i)
A8: 1 <= j + 1 by A6, NAT_1:13;
A9: j + 1 <= width G by A7, NAT_1:13;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg ((G * (i,j)),(G * (i,(j + 1)))) or x in v_strip (G,i) )
assume A10: x in LSeg ((G * (i,j)),(G * (i,(j + 1)))) ; ::_thesis: x in v_strip (G,i)
then reconsider p = x as Point of (TOP-REAL 2) ;
A11: p = |[(p `1),(p `2)]| by EUCLID:53;
A12: (G * (i,j)) `1 = (G * (i,1)) `1 by A2, A4, A5, A6, A7, Th2
.= (G * (i,(j + 1))) `1 by A2, A4, A5, A8, A9, Th2 ;
now__::_thesis:_x_in_v_strip_(G,i)
percases ( i = len G or i < len G ) by A5, XXREAL_0:1;
supposeA13: i = len G ; ::_thesis: x in v_strip (G,i)
then (G * ((len G),j)) `1 <= p `1 by A10, A12, TOPREAL1:3;
then p in { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r } by A11;
hence x in v_strip (G,i) by A1, A2, A6, A7, A13, Th9; ::_thesis: verum
end;
supposeA14: i < len G ; ::_thesis: x in v_strip (G,i)
then A15: i + 1 <= len G by NAT_1:13;
A16: (G * (i,j)) `1 <= p `1 by A10, A12, TOPREAL1:3;
p `1 <= (G * (i,j)) `1 by A10, A12, TOPREAL1:3;
then A17: p `1 = (G * (i,j)) `1 by A16, XXREAL_0:1;
i < i + 1 by XREAL_1:29;
then p `1 < (G * ((i + 1),j)) `1 by A3, A4, A6, A7, A15, A17, Th3;
then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } by A11, A16;
hence x in v_strip (G,i) by A2, A4, A6, A7, A14, Th8; ::_thesis: verum
end;
end;
end;
hence x in v_strip (G,i) ; ::_thesis: verum
end;
theorem Th15: :: GOBOARD5:15
for j, i being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j < width G & 1 <= i & i < len G holds
LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= h_strip (G,j)
proof
let j, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j < width G & 1 <= i & i < len G holds
LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= h_strip (G,j)
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j < width G & 1 <= i & i < len G implies LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= h_strip (G,j) )
assume that
A1: G is V3() and
A2: G is Y_equal-in-column and
A3: G is Y_increasing-in-line and
A4: j < width G and
A5: 1 <= i and
A6: i < len G ; ::_thesis: LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= h_strip (G,j)
A7: 1 <= i + 1 by A5, NAT_1:13;
A8: i + 1 <= len G by A6, NAT_1:13;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) or x in h_strip (G,j) )
assume A9: x in LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) ; ::_thesis: x in h_strip (G,j)
then reconsider p = x as Point of (TOP-REAL 2) ;
A10: p = |[(p `1),(p `2)]| by EUCLID:53;
A11: 1 <= j + 1 by NAT_1:11;
A12: j + 1 <= width G by A4, NAT_1:13;
then A13: (G * (i,(j + 1))) `2 = (G * (1,(j + 1))) `2 by A2, A5, A6, A11, Th1
.= (G * ((i + 1),(j + 1))) `2 by A2, A7, A8, A11, A12, Th1 ;
now__::_thesis:_x_in_h_strip_(G,j)
percases ( j = 0 or j > 0 ) by NAT_1:3;
supposeA14: j = 0 ; ::_thesis: x in h_strip (G,j)
then p `2 <= (G * (i,1)) `2 by A9, A13, TOPREAL1:4;
then p in { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 } by A10;
hence x in h_strip (G,j) by A1, A2, A5, A6, A14, Th7; ::_thesis: verum
end;
suppose j > 0 ; ::_thesis: x in h_strip (G,j)
then A15: 0 + 1 <= j by NAT_1:13;
A16: (G * (i,(j + 1))) `2 <= p `2 by A9, A13, TOPREAL1:4;
A17: p `2 <= (G * (i,(j + 1))) `2 by A9, A13, TOPREAL1:4;
then A18: p `2 = (G * (i,(j + 1))) `2 by A16, XXREAL_0:1;
j < j + 1 by XREAL_1:29;
then (G * (i,j)) `2 < p `2 by A3, A5, A6, A12, A15, A18, Th4;
then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } by A10, A17;
hence x in h_strip (G,j) by A2, A4, A5, A6, A15, Th5; ::_thesis: verum
end;
end;
end;
hence x in h_strip (G,j) ; ::_thesis: verum
end;
theorem Th16: :: GOBOARD5:16
for j, i being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= j & j <= width G & 1 <= i & i < len G holds
LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j)
proof
let j, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= j & j <= width G & 1 <= i & i < len G holds
LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j)
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= j & j <= width G & 1 <= i & i < len G implies LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j) )
assume that
A1: G is V3() and
A2: G is Y_equal-in-column and
A3: G is Y_increasing-in-line and
A4: 1 <= j and
A5: j <= width G and
A6: 1 <= i and
A7: i < len G ; ::_thesis: LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j)
A8: 1 <= i + 1 by A6, NAT_1:13;
A9: i + 1 <= len G by A7, NAT_1:13;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg ((G * (i,j)),(G * ((i + 1),j))) or x in h_strip (G,j) )
assume A10: x in LSeg ((G * (i,j)),(G * ((i + 1),j))) ; ::_thesis: x in h_strip (G,j)
then reconsider p = x as Point of (TOP-REAL 2) ;
A11: p = |[(p `1),(p `2)]| by EUCLID:53;
A12: (G * (i,j)) `2 = (G * (1,j)) `2 by A2, A4, A5, A6, A7, Th1
.= (G * ((i + 1),j)) `2 by A2, A4, A5, A8, A9, Th1 ;
now__::_thesis:_x_in_h_strip_(G,j)
percases ( j = width G or j < width G ) by A5, XXREAL_0:1;
supposeA13: j = width G ; ::_thesis: x in h_strip (G,j)
then (G * (i,(width G))) `2 <= p `2 by A10, A12, TOPREAL1:4;
then p in { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s } by A11;
hence x in h_strip (G,j) by A1, A2, A6, A7, A13, Th6; ::_thesis: verum
end;
supposeA14: j < width G ; ::_thesis: x in h_strip (G,j)
then A15: j + 1 <= width G by NAT_1:13;
A16: (G * (i,j)) `2 <= p `2 by A10, A12, TOPREAL1:4;
p `2 <= (G * (i,j)) `2 by A10, A12, TOPREAL1:4;
then A17: p `2 = (G * (i,j)) `2 by A16, XXREAL_0:1;
j < j + 1 by XREAL_1:29;
then p `2 < (G * (i,(j + 1))) `2 by A3, A4, A6, A7, A15, A17, Th4;
then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } by A11, A16;
hence x in h_strip (G,j) by A2, A4, A6, A7, A14, Th5; ::_thesis: verum
end;
end;
end;
hence x in h_strip (G,j) ; ::_thesis: verum
end;
theorem Th17: :: GOBOARD5:17
for i, j being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= i & i <= len G & 1 <= j & j + 1 <= width G holds
LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= h_strip (G,j)
proof
let i, j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= i & i <= len G & 1 <= j & j + 1 <= width G holds
LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= h_strip (G,j)
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= i & i <= len G & 1 <= j & j + 1 <= width G implies LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= h_strip (G,j) )
assume that
A1: G is Y_equal-in-column and
A2: G is Y_increasing-in-line and
A3: 1 <= i and
A4: i <= len G and
A5: 1 <= j and
A6: j + 1 <= width G ; ::_thesis: LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= h_strip (G,j)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg ((G * (i,j)),(G * (i,(j + 1)))) or x in h_strip (G,j) )
assume A7: x in LSeg ((G * (i,j)),(G * (i,(j + 1)))) ; ::_thesis: x in h_strip (G,j)
then reconsider p = x as Point of (TOP-REAL 2) ;
A8: p = |[(p `1),(p `2)]| by EUCLID:53;
A9: j < width G by A6, NAT_1:13;
j < j + 1 by XREAL_1:29;
then A10: (G * (i,j)) `2 < (G * (i,(j + 1))) `2 by A2, A3, A4, A5, A6, Th4;
then A11: (G * (i,j)) `2 <= p `2 by A7, TOPREAL1:4;
p `2 <= (G * (i,(j + 1))) `2 by A7, A10, TOPREAL1:4;
then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } by A8, A11;
hence x in h_strip (G,j) by A1, A3, A4, A5, A9, Th5; ::_thesis: verum
end;
theorem Th18: :: GOBOARD5:18
for i, j being Element of NAT
for G being Go-board st i < len G & 1 <= j & j < width G holds
LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j)
proof
let i, j be Element of NAT ; ::_thesis: for G being Go-board st i < len G & 1 <= j & j < width G holds
LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j)
let G be Go-board; ::_thesis: ( i < len G & 1 <= j & j < width G implies LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) )
assume that
A1: i < len G and
A2: 1 <= j and
A3: j < width G ; ::_thesis: LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j)
A4: LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i) by A1, A2, A3, Th13;
A5: 1 <= i + 1 by NAT_1:11;
A6: i + 1 <= len G by A1, NAT_1:13;
j + 1 <= width G by A3, NAT_1:13;
then LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= h_strip (G,j) by A2, A5, A6, Th17;
hence LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) by A4, XBOOLE_1:19; ::_thesis: verum
end;
theorem Th19: :: GOBOARD5:19
for i, j being Element of NAT
for G being Go-board st 1 <= i & i <= len G & 1 <= j & j < width G holds
LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= cell (G,i,j)
proof
let i, j be Element of NAT ; ::_thesis: for G being Go-board st 1 <= i & i <= len G & 1 <= j & j < width G holds
LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= cell (G,i,j)
let G be Go-board; ::_thesis: ( 1 <= i & i <= len G & 1 <= j & j < width G implies LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= cell (G,i,j) )
assume that
A1: 1 <= i and
A2: i <= len G and
A3: 1 <= j and
A4: j < width G ; ::_thesis: LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= cell (G,i,j)
A5: LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i) by A1, A2, A3, A4, Th14;
j + 1 <= width G by A4, NAT_1:13;
then LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= h_strip (G,j) by A1, A2, A3, Th17;
hence LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= cell (G,i,j) by A5, XBOOLE_1:19; ::_thesis: verum
end;
theorem Th20: :: GOBOARD5:20
for j, i being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i & i + 1 <= len G holds
LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i)
proof
let j, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i & i + 1 <= len G holds
LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i)
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is X_equal-in-line & G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i & i + 1 <= len G implies LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i) )
assume that
A1: G is X_equal-in-line and
A2: G is X_increasing-in-column and
A3: 1 <= j and
A4: j <= width G and
A5: 1 <= i and
A6: i + 1 <= len G ; ::_thesis: LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg ((G * (i,j)),(G * ((i + 1),j))) or x in v_strip (G,i) )
assume A7: x in LSeg ((G * (i,j)),(G * ((i + 1),j))) ; ::_thesis: x in v_strip (G,i)
then reconsider p = x as Point of (TOP-REAL 2) ;
A8: p = |[(p `1),(p `2)]| by EUCLID:53;
A9: i < len G by A6, NAT_1:13;
i < i + 1 by XREAL_1:29;
then A10: (G * (i,j)) `1 < (G * ((i + 1),j)) `1 by A2, A3, A4, A5, A6, Th3;
then A11: (G * (i,j)) `1 <= p `1 by A7, TOPREAL1:3;
p `1 <= (G * ((i + 1),j)) `1 by A7, A10, TOPREAL1:3;
then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } by A8, A11;
hence x in v_strip (G,i) by A1, A3, A4, A5, A9, Th8; ::_thesis: verum
end;
theorem Th21: :: GOBOARD5:21
for j, i being Element of NAT
for G being Go-board st j < width G & 1 <= i & i < len G holds
LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j)
proof
let j, i be Element of NAT ; ::_thesis: for G being Go-board st j < width G & 1 <= i & i < len G holds
LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j)
let G be Go-board; ::_thesis: ( j < width G & 1 <= i & i < len G implies LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) )
assume that
A1: j < width G and
A2: 1 <= i and
A3: i < len G ; ::_thesis: LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j)
A4: LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= h_strip (G,j) by A1, A2, A3, Th15;
A5: 1 <= j + 1 by NAT_1:11;
A6: i + 1 <= len G by A3, NAT_1:13;
j + 1 <= width G by A1, NAT_1:13;
then LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= v_strip (G,i) by A2, A5, A6, Th20;
hence LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) by A4, XBOOLE_1:19; ::_thesis: verum
end;
theorem Th22: :: GOBOARD5:22
for i, j being Element of NAT
for G being Go-board st 1 <= i & i < len G & 1 <= j & j <= width G holds
LSeg ((G * (i,j)),(G * ((i + 1),j))) c= cell (G,i,j)
proof
let i, j be Element of NAT ; ::_thesis: for G being Go-board st 1 <= i & i < len G & 1 <= j & j <= width G holds
LSeg ((G * (i,j)),(G * ((i + 1),j))) c= cell (G,i,j)
let G be Go-board; ::_thesis: ( 1 <= i & i < len G & 1 <= j & j <= width G implies LSeg ((G * (i,j)),(G * ((i + 1),j))) c= cell (G,i,j) )
assume that
A1: 1 <= i and
A2: i < len G and
A3: 1 <= j and
A4: j <= width G ; ::_thesis: LSeg ((G * (i,j)),(G * ((i + 1),j))) c= cell (G,i,j)
A5: LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j) by A1, A2, A3, A4, Th16;
i + 1 <= len G by A2, NAT_1:13;
then LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i) by A1, A3, A4, Th20;
hence LSeg ((G * (i,j)),(G * ((i + 1),j))) c= cell (G,i,j) by A5, XBOOLE_1:19; ::_thesis: verum
end;
theorem Th23: :: GOBOARD5:23
for i being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i + 1 <= len G holds
(v_strip (G,i)) /\ (v_strip (G,(i + 1))) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 }
proof
let i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i + 1 <= len G holds
(v_strip (G,i)) /\ (v_strip (G,(i + 1))) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 }
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i + 1 <= len G implies (v_strip (G,i)) /\ (v_strip (G,(i + 1))) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } )
assume that
A1: ( G is V3() & G is X_equal-in-line ) and
A2: G is X_increasing-in-column and
A3: i + 1 <= len G ; ::_thesis: (v_strip (G,i)) /\ (v_strip (G,(i + 1))) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 }
width G <> 0 by A1, GOBOARD1:def_3;
then A4: 1 <= width G by NAT_1:14;
A5: i < len G by A3, NAT_1:13;
thus (v_strip (G,i)) /\ (v_strip (G,(i + 1))) c= { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } :: according to XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } c= (v_strip (G,i)) /\ (v_strip (G,(i + 1)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (v_strip (G,i)) /\ (v_strip (G,(i + 1))) or x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } )
assume A6: x in (v_strip (G,i)) /\ (v_strip (G,(i + 1))) ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 }
then A7: x in v_strip (G,i) by XBOOLE_0:def_4;
A8: x in v_strip (G,(i + 1)) by A6, XBOOLE_0:def_4;
reconsider p = x as Point of (TOP-REAL 2) by A6;
percases ( ( i = 0 & i + 1 = len G ) or ( i = 0 & i + 1 <> len G ) or ( i <> 0 & i + 1 = len G ) or ( i <> 0 & i + 1 <> len G ) ) ;
supposethat A9: i = 0 and
A10: i + 1 = len G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 }
v_strip (G,i) = { |[r,s]| where r, s is Real : r <= (G * ((0 + 1),1)) `1 } by A1, A4, A9, Th10;
then consider r1, s1 being Real such that
A11: x = |[r1,s1]| and
A12: r1 <= (G * (1,1)) `1 by A7;
v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } by A1, A4, Th9;
then consider r2, s2 being Real such that
A13: x = |[r2,s2]| and
A14: (G * ((i + 1),1)) `1 <= r2 by A8, A10;
r1 = |[r2,s2]| `1 by A11, A13, EUCLID:52
.= r2 by EUCLID:52 ;
then (G * ((i + 1),1)) `1 = r1 by A9, A12, A14, XXREAL_0:1;
then (G * ((i + 1),1)) `1 = p `1 by A11, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; ::_thesis: verum
end;
supposethat A15: i = 0 and
A16: i + 1 <> len G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 }
v_strip (G,i) = { |[r,s]| where r, s is Real : r <= (G * ((0 + 1),1)) `1 } by A1, A4, A15, Th10;
then consider r1, s1 being Real such that
A17: x = |[r1,s1]| and
A18: r1 <= (G * (1,1)) `1 by A7;
i + 1 < len G by A3, A16, XXREAL_0:1;
then v_strip (G,(i + 1)) = { |[r,s]| where r, s is Real : ( (G * ((0 + 1),1)) `1 <= r & r <= (G * (((0 + 1) + 1),1)) `1 ) } by A1, A4, A15, Th8;
then consider r2, s2 being Real such that
A19: x = |[r2,s2]| and
A20: (G * (1,1)) `1 <= r2 and
r2 <= (G * ((1 + 1),1)) `1 by A8;
r1 = |[r2,s2]| `1 by A17, A19, EUCLID:52
.= r2 by EUCLID:52 ;
then (G * (1,1)) `1 = r1 by A18, A20, XXREAL_0:1;
then (G * (1,1)) `1 = p `1 by A17, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } by A15; ::_thesis: verum
end;
supposethat A21: i <> 0 and
A22: i + 1 = len G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 }
A23: 1 <= i by A21, NAT_1:14;
i < len G by A3, NAT_1:13;
then v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } by A1, A4, A23, Th8;
then consider r1, s1 being Real such that
A24: x = |[r1,s1]| and
(G * (i,1)) `1 <= r1 and
A25: r1 <= (G * ((i + 1),1)) `1 by A7;
v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } by A1, A4, Th9;
then consider r2, s2 being Real such that
A26: x = |[r2,s2]| and
A27: (G * ((i + 1),1)) `1 <= r2 by A8, A22;
r1 = |[r2,s2]| `1 by A24, A26, EUCLID:52
.= r2 by EUCLID:52 ;
then (G * ((i + 1),1)) `1 = r1 by A25, A27, XXREAL_0:1;
then (G * ((i + 1),1)) `1 = p `1 by A24, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; ::_thesis: verum
end;
supposethat A28: i <> 0 and
A29: i + 1 <> len G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 }
A30: 1 <= i by A28, NAT_1:14;
i < len G by A3, NAT_1:13;
then v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } by A1, A4, A30, Th8;
then consider r1, s1 being Real such that
A31: x = |[r1,s1]| and
(G * (i,1)) `1 <= r1 and
A32: r1 <= (G * ((i + 1),1)) `1 by A7;
A33: 1 <= i + 1 by NAT_1:11;
i + 1 < len G by A3, A29, XXREAL_0:1;
then v_strip (G,(i + 1)) = { |[r,s]| where r, s is Real : ( (G * ((i + 1),1)) `1 <= r & r <= (G * (((i + 1) + 1),1)) `1 ) } by A1, A4, A33, Th8;
then consider r2, s2 being Real such that
A34: x = |[r2,s2]| and
A35: (G * ((i + 1),1)) `1 <= r2 and
r2 <= (G * (((i + 1) + 1),1)) `1 by A8;
r1 = |[r2,s2]| `1 by A31, A34, EUCLID:52
.= r2 by EUCLID:52 ;
then (G * ((i + 1),1)) `1 = r1 by A32, A35, XXREAL_0:1;
then (G * ((i + 1),1)) `1 = p `1 by A31, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; ::_thesis: verum
end;
end;
end;
A36: { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } c= v_strip (G,i)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } or x in v_strip (G,i) )
assume x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; ::_thesis: x in v_strip (G,i)
then consider p being Point of (TOP-REAL 2) such that
A37: p = x and
A38: p `1 = (G * ((i + 1),1)) `1 ;
A39: p = |[(p `1),(p `2)]| by EUCLID:53;
percases ( i = 0 or i >= 1 ) by NAT_1:14;
supposeA40: i = 0 ; ::_thesis: x in v_strip (G,i)
then v_strip (G,i) = { |[r,s]| where r, s is Real : r <= (G * (1,1)) `1 } by A1, A4, Th10;
hence x in v_strip (G,i) by A37, A38, A39, A40; ::_thesis: verum
end;
supposeA41: i >= 1 ; ::_thesis: x in v_strip (G,i)
then A42: v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } by A1, A4, A5, Th8;
i < i + 1 by XREAL_1:29;
then (G * (i,1)) `1 < p `1 by A2, A3, A4, A38, A41, Th3;
hence x in v_strip (G,i) by A37, A38, A39, A42; ::_thesis: verum
end;
end;
end;
{ q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } c= v_strip (G,(i + 1))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } or x in v_strip (G,(i + 1)) )
assume x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; ::_thesis: x in v_strip (G,(i + 1))
then consider p being Point of (TOP-REAL 2) such that
A43: p = x and
A44: p `1 = (G * ((i + 1),1)) `1 ;
A45: p = |[(p `1),(p `2)]| by EUCLID:53;
A46: 1 <= i + 1 by NAT_1:11;
percases ( i + 1 = len G or i + 1 < len G ) by A3, XXREAL_0:1;
supposeA47: i + 1 = len G ; ::_thesis: x in v_strip (G,(i + 1))
then v_strip (G,(i + 1)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } by A1, A4, Th9;
hence x in v_strip (G,(i + 1)) by A43, A44, A45, A47; ::_thesis: verum
end;
supposeA48: i + 1 < len G ; ::_thesis: x in v_strip (G,(i + 1))
then A49: v_strip (G,(i + 1)) = { |[r,s]| where r, s is Real : ( (G * ((i + 1),1)) `1 <= r & r <= (G * (((i + 1) + 1),1)) `1 ) } by A1, A4, A46, Th8;
A50: i + 1 < (i + 1) + 1 by NAT_1:13;
(i + 1) + 1 <= len G by A48, NAT_1:13;
then p `1 < (G * (((i + 1) + 1),1)) `1 by A2, A4, A44, A46, A50, Th3;
hence x in v_strip (G,(i + 1)) by A43, A44, A45, A49; ::_thesis: verum
end;
end;
end;
hence { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } c= (v_strip (G,i)) /\ (v_strip (G,(i + 1))) by A36, XBOOLE_1:19; ::_thesis: verum
end;
theorem Th24: :: GOBOARD5:24
for j being Element of NAT
for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j + 1 <= width G holds
(h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
proof
let j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j + 1 <= width G holds
(h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j + 1 <= width G implies (h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } )
assume that
A1: ( G is V3() & G is Y_equal-in-column ) and
A2: G is Y_increasing-in-line and
A3: j + 1 <= width G ; ::_thesis: (h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
len G <> 0 by A1, GOBOARD1:def_3;
then A4: 1 <= len G by NAT_1:14;
A5: j < width G by A3, NAT_1:13;
thus (h_strip (G,j)) /\ (h_strip (G,(j + 1))) c= { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } :: according to XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= (h_strip (G,j)) /\ (h_strip (G,(j + 1)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (h_strip (G,j)) /\ (h_strip (G,(j + 1))) or x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } )
assume A6: x in (h_strip (G,j)) /\ (h_strip (G,(j + 1))) ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
then A7: x in h_strip (G,j) by XBOOLE_0:def_4;
A8: x in h_strip (G,(j + 1)) by A6, XBOOLE_0:def_4;
reconsider p = x as Point of (TOP-REAL 2) by A6;
percases ( ( j = 0 & j + 1 = width G ) or ( j = 0 & j + 1 <> width G ) or ( j <> 0 & j + 1 = width G ) or ( j <> 0 & j + 1 <> width G ) ) ;
supposethat A9: j = 0 and
A10: j + 1 = width G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
h_strip (G,j) = { |[r,s]| where r, s is Real : s <= (G * (1,(0 + 1))) `2 } by A1, A4, A9, Th7;
then consider r1, s1 being Real such that
A11: x = |[r1,s1]| and
A12: s1 <= (G * (1,1)) `2 by A7;
h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } by A1, A4, Th6;
then consider r2, s2 being Real such that
A13: x = |[r2,s2]| and
A14: (G * (1,(j + 1))) `2 <= s2 by A8, A10;
s1 = |[r2,s2]| `2 by A11, A13, EUCLID:52
.= s2 by EUCLID:52 ;
then (G * (1,(j + 1))) `2 = s1 by A9, A12, A14, XXREAL_0:1;
then (G * (1,(j + 1))) `2 = p `2 by A11, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; ::_thesis: verum
end;
supposethat A15: j = 0 and
A16: j + 1 <> width G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
h_strip (G,j) = { |[r,s]| where r, s is Real : s <= (G * (1,(0 + 1))) `2 } by A1, A4, A15, Th7;
then consider r1, s1 being Real such that
A17: x = |[r1,s1]| and
A18: s1 <= (G * (1,1)) `2 by A7;
j + 1 < width G by A3, A16, XXREAL_0:1;
then h_strip (G,(j + 1)) = { |[r,s]| where r, s is Real : ( (G * (1,(0 + 1))) `2 <= s & s <= (G * (1,((0 + 1) + 1))) `2 ) } by A1, A4, A15, Th5;
then consider r2, s2 being Real such that
A19: x = |[r2,s2]| and
A20: (G * (1,1)) `2 <= s2 and
s2 <= (G * (1,(1 + 1))) `2 by A8;
s1 = |[r2,s2]| `2 by A17, A19, EUCLID:52
.= s2 by EUCLID:52 ;
then (G * (1,1)) `2 = s1 by A18, A20, XXREAL_0:1;
then (G * (1,1)) `2 = p `2 by A17, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } by A15; ::_thesis: verum
end;
supposethat A21: j <> 0 and
A22: j + 1 = width G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
A23: 1 <= j by A21, NAT_1:14;
j < width G by A3, NAT_1:13;
then h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A1, A4, A23, Th5;
then consider r1, s1 being Real such that
A24: x = |[r1,s1]| and
(G * (1,j)) `2 <= s1 and
A25: s1 <= (G * (1,(j + 1))) `2 by A7;
h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } by A1, A4, Th6;
then consider r2, s2 being Real such that
A26: x = |[r2,s2]| and
A27: (G * (1,(j + 1))) `2 <= s2 by A8, A22;
s1 = |[r2,s2]| `2 by A24, A26, EUCLID:52
.= s2 by EUCLID:52 ;
then (G * (1,(j + 1))) `2 = s1 by A25, A27, XXREAL_0:1;
then (G * (1,(j + 1))) `2 = p `2 by A24, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; ::_thesis: verum
end;
supposethat A28: j <> 0 and
A29: j + 1 <> width G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }
A30: 1 <= j by A28, NAT_1:14;
j < width G by A3, NAT_1:13;
then h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A1, A4, A30, Th5;
then consider r1, s1 being Real such that
A31: x = |[r1,s1]| and
(G * (1,j)) `2 <= s1 and
A32: s1 <= (G * (1,(j + 1))) `2 by A7;
A33: 1 <= j + 1 by NAT_1:11;
j + 1 < width G by A3, A29, XXREAL_0:1;
then h_strip (G,(j + 1)) = { |[r,s]| where r, s is Real : ( (G * (1,(j + 1))) `2 <= s & s <= (G * (1,((j + 1) + 1))) `2 ) } by A1, A4, A33, Th5;
then consider r2, s2 being Real such that
A34: x = |[r2,s2]| and
A35: (G * (1,(j + 1))) `2 <= s2 and
s2 <= (G * (1,((j + 1) + 1))) `2 by A8;
s1 = |[r2,s2]| `2 by A31, A34, EUCLID:52
.= s2 by EUCLID:52 ;
then (G * (1,(j + 1))) `2 = s1 by A32, A35, XXREAL_0:1;
then (G * (1,(j + 1))) `2 = p `2 by A31, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; ::_thesis: verum
end;
end;
end;
A36: { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= h_strip (G,j)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } or x in h_strip (G,j) )
assume x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; ::_thesis: x in h_strip (G,j)
then consider p being Point of (TOP-REAL 2) such that
A37: p = x and
A38: p `2 = (G * (1,(j + 1))) `2 ;
A39: p = |[(p `1),(p `2)]| by EUCLID:53;
percases ( j = 0 or j >= 1 ) by NAT_1:14;
supposeA40: j = 0 ; ::_thesis: x in h_strip (G,j)
then h_strip (G,j) = { |[r,s]| where r, s is Real : s <= (G * (1,1)) `2 } by A1, A4, Th7;
hence x in h_strip (G,j) by A37, A38, A39, A40; ::_thesis: verum
end;
supposeA41: j >= 1 ; ::_thesis: x in h_strip (G,j)
then A42: h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A1, A4, A5, Th5;
j < j + 1 by XREAL_1:29;
then (G * (1,j)) `2 < p `2 by A2, A3, A4, A38, A41, Th4;
hence x in h_strip (G,j) by A37, A38, A39, A42; ::_thesis: verum
end;
end;
end;
{ q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= h_strip (G,(j + 1))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } or x in h_strip (G,(j + 1)) )
assume x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; ::_thesis: x in h_strip (G,(j + 1))
then consider p being Point of (TOP-REAL 2) such that
A43: p = x and
A44: p `2 = (G * (1,(j + 1))) `2 ;
A45: p = |[(p `1),(p `2)]| by EUCLID:53;
A46: 1 <= j + 1 by NAT_1:11;
percases ( j + 1 = width G or j + 1 < width G ) by A3, XXREAL_0:1;
supposeA47: j + 1 = width G ; ::_thesis: x in h_strip (G,(j + 1))
then h_strip (G,(j + 1)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } by A1, A4, Th6;
hence x in h_strip (G,(j + 1)) by A43, A44, A45, A47; ::_thesis: verum
end;
supposeA48: j + 1 < width G ; ::_thesis: x in h_strip (G,(j + 1))
then A49: h_strip (G,(j + 1)) = { |[r,s]| where r, s is Real : ( (G * (1,(j + 1))) `2 <= s & s <= (G * (1,((j + 1) + 1))) `2 ) } by A1, A4, A46, Th5;
A50: j + 1 < (j + 1) + 1 by NAT_1:13;
(j + 1) + 1 <= width G by A48, NAT_1:13;
then p `2 < (G * (1,((j + 1) + 1))) `2 by A2, A4, A44, A46, A50, Th4;
hence x in h_strip (G,(j + 1)) by A43, A44, A45, A49; ::_thesis: verum
end;
end;
end;
hence { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= (h_strip (G,j)) /\ (h_strip (G,(j + 1))) by A36, XBOOLE_1:19; ::_thesis: verum
end;
theorem Th25: :: GOBOARD5:25
for i, j being Element of NAT
for G being Go-board st i < len G & 1 <= j & j < width G holds
(cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))
proof
let i, j be Element of NAT ; ::_thesis: for G being Go-board st i < len G & 1 <= j & j < width G holds
(cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))
let G be Go-board; ::_thesis: ( i < len G & 1 <= j & j < width G implies (cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) )
assume that
A1: i < len G and
A2: 1 <= j and
A3: j < width G ; ::_thesis: (cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))
0 <= i by NAT_1:2;
then A4: 0 + 1 <= i + 1 by XREAL_1:6;
A5: i + 1 <= len G by A1, NAT_1:13;
thus (cell (G,i,j)) /\ (cell (G,(i + 1),j)) c= LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) :: according to XBOOLE_0:def_10 ::_thesis: LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= (cell (G,i,j)) /\ (cell (G,(i + 1),j))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (cell (G,i,j)) /\ (cell (G,(i + 1),j)) or x in LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) )
A6: (cell (G,i,j)) /\ (cell (G,(i + 1),j)) = (v_strip (G,i)) /\ (((v_strip (G,(i + 1))) /\ (h_strip (G,j))) /\ (h_strip (G,j))) by XBOOLE_1:16
.= (v_strip (G,i)) /\ ((v_strip (G,(i + 1))) /\ ((h_strip (G,j)) /\ (h_strip (G,j)))) by XBOOLE_1:16
.= ((v_strip (G,i)) /\ (v_strip (G,(i + 1)))) /\ (h_strip (G,j)) by XBOOLE_1:16 ;
assume A7: x in (cell (G,i,j)) /\ (cell (G,(i + 1),j)) ; ::_thesis: x in LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))
then A8: x in (v_strip (G,i)) /\ (v_strip (G,(i + 1))) by A6, XBOOLE_0:def_4;
A9: x in h_strip (G,j) by A6, A7, XBOOLE_0:def_4;
A10: j < j + 1 by NAT_1:13;
A11: j + 1 <= width G by A3, NAT_1:13;
then A12: (G * ((i + 1),j)) `2 < (G * ((i + 1),(j + 1))) `2 by A2, A4, A5, A10, Th4;
A13: G * ((i + 1),j) = |[((G * ((i + 1),j)) `1),((G * ((i + 1),j)) `2)]| by EUCLID:53;
A14: j + 1 >= 1 by NAT_1:11;
(G * ((i + 1),j)) `1 = (G * ((i + 1),1)) `1 by A2, A3, A4, A5, Th2
.= (G * ((i + 1),(j + 1))) `1 by A4, A5, A11, A14, Th2 ;
then A15: G * ((i + 1),(j + 1)) = |[((G * ((i + 1),j)) `1),((G * ((i + 1),(j + 1))) `2)]| by EUCLID:53;
reconsider p = x as Point of (TOP-REAL 2) by A7;
i + 1 <= len G by A1, NAT_1:13;
then p in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } by A8, Th23;
then ex q being Point of (TOP-REAL 2) st
( q = p & q `1 = (G * ((i + 1),1)) `1 ) ;
then A16: p `1 = (G * ((i + 1),j)) `1 by A2, A3, A4, A5, Th2;
p in { |[r,s]| where r, s is Real : ( (G * ((i + 1),j)) `2 <= s & s <= (G * ((i + 1),(j + 1))) `2 ) } by A2, A3, A4, A5, A9, Th5;
then A17: ex r, s being Real st
( p = |[r,s]| & (G * ((i + 1),j)) `2 <= s & s <= (G * ((i + 1),(j + 1))) `2 ) ;
then A18: (G * ((i + 1),j)) `2 <= p `2 by EUCLID:52;
p `2 <= (G * ((i + 1),(j + 1))) `2 by A17, EUCLID:52;
then p in { q where q is Point of (TOP-REAL 2) : ( q `1 = (G * ((i + 1),j)) `1 & (G * ((i + 1),j)) `2 <= q `2 & q `2 <= (G * ((i + 1),(j + 1))) `2 ) } by A16, A18;
hence x in LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) by A12, A13, A15, TOPREAL3:9; ::_thesis: verum
end;
A19: LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) by A1, A2, A3, Th18;
LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,(i + 1),j) by A2, A3, A4, A5, Th19;
hence LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= (cell (G,i,j)) /\ (cell (G,(i + 1),j)) by A19, XBOOLE_1:19; ::_thesis: verum
end;
theorem Th26: :: GOBOARD5:26
for j, i being Element of NAT
for G being Go-board st j < width G & 1 <= i & i < len G holds
(cell (G,i,j)) /\ (cell (G,i,(j + 1))) = LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1))))
proof
let j, i be Element of NAT ; ::_thesis: for G being Go-board st j < width G & 1 <= i & i < len G holds
(cell (G,i,j)) /\ (cell (G,i,(j + 1))) = LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1))))
let G be Go-board; ::_thesis: ( j < width G & 1 <= i & i < len G implies (cell (G,i,j)) /\ (cell (G,i,(j + 1))) = LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) )
assume that
A1: j < width G and
A2: 1 <= i and
A3: i < len G ; ::_thesis: (cell (G,i,j)) /\ (cell (G,i,(j + 1))) = LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1))))
0 <= j by NAT_1:2;
then A4: 0 + 1 <= j + 1 by XREAL_1:6;
A5: j + 1 <= width G by A1, NAT_1:13;
thus (cell (G,i,j)) /\ (cell (G,i,(j + 1))) c= LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) :: according to XBOOLE_0:def_10 ::_thesis: LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= (cell (G,i,j)) /\ (cell (G,i,(j + 1)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (cell (G,i,j)) /\ (cell (G,i,(j + 1))) or x in LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) )
A6: (cell (G,i,j)) /\ (cell (G,i,(j + 1))) = (h_strip (G,j)) /\ (((h_strip (G,(j + 1))) /\ (v_strip (G,i))) /\ (v_strip (G,i))) by XBOOLE_1:16
.= (h_strip (G,j)) /\ ((h_strip (G,(j + 1))) /\ ((v_strip (G,i)) /\ (v_strip (G,i)))) by XBOOLE_1:16
.= ((h_strip (G,j)) /\ (h_strip (G,(j + 1)))) /\ (v_strip (G,i)) by XBOOLE_1:16 ;
assume A7: x in (cell (G,i,j)) /\ (cell (G,i,(j + 1))) ; ::_thesis: x in LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1))))
then A8: x in (h_strip (G,j)) /\ (h_strip (G,(j + 1))) by A6, XBOOLE_0:def_4;
A9: x in v_strip (G,i) by A6, A7, XBOOLE_0:def_4;
A10: i < i + 1 by NAT_1:13;
A11: i + 1 <= len G by A3, NAT_1:13;
then A12: (G * (i,(j + 1))) `1 < (G * ((i + 1),(j + 1))) `1 by A2, A4, A5, A10, Th3;
A13: G * (i,(j + 1)) = |[((G * (i,(j + 1))) `1),((G * (i,(j + 1))) `2)]| by EUCLID:53;
A14: i + 1 >= 1 by NAT_1:11;
(G * (i,(j + 1))) `2 = (G * (1,(j + 1))) `2 by A2, A3, A4, A5, Th1
.= (G * ((i + 1),(j + 1))) `2 by A4, A5, A11, A14, Th1 ;
then A15: G * ((i + 1),(j + 1)) = |[((G * ((i + 1),(j + 1))) `1),((G * (i,(j + 1))) `2)]| by EUCLID:53;
reconsider p = x as Point of (TOP-REAL 2) by A7;
j + 1 <= width G by A1, NAT_1:13;
then p in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } by A8, Th24;
then ex q being Point of (TOP-REAL 2) st
( q = p & q `2 = (G * (1,(j + 1))) `2 ) ;
then A16: p `2 = (G * (i,(j + 1))) `2 by A2, A3, A4, A5, Th1;
p in { |[r,s]| where r, s is Real : ( (G * (i,(j + 1))) `1 <= r & r <= (G * ((i + 1),(j + 1))) `1 ) } by A2, A3, A4, A5, A9, Th8;
then A17: ex r, s being Real st
( p = |[r,s]| & (G * (i,(j + 1))) `1 <= r & r <= (G * ((i + 1),(j + 1))) `1 ) ;
then A18: (G * (i,(j + 1))) `1 <= p `1 by EUCLID:52;
p `1 <= (G * ((i + 1),(j + 1))) `1 by A17, EUCLID:52;
then p in { q where q is Point of (TOP-REAL 2) : ( q `2 = (G * (i,(j + 1))) `2 & (G * (i,(j + 1))) `1 <= q `1 & q `1 <= (G * ((i + 1),(j + 1))) `1 ) } by A16, A18;
hence x in LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) by A12, A13, A15, TOPREAL3:10; ::_thesis: verum
end;
A19: LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) by A1, A2, A3, Th21;
LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,(j + 1)) by A2, A3, A4, A5, Th22;
hence LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= (cell (G,i,j)) /\ (cell (G,i,(j + 1))) by A19, XBOOLE_1:19; ::_thesis: verum
end;
theorem Th27: :: GOBOARD5:27
for k, i, j being Element of NAT
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [(i + 1),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),j) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) holds
( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),(i + 1),j) )
proof
let k, i, j be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [(i + 1),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),j) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) holds
( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),(i + 1),j) )
let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f & [(i + 1),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),j) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) implies ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),(i + 1),j) ) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f and
A3: [(i + 1),j] in Indices (GoB f) and
A4: [(i + 1),(j + 1)] in Indices (GoB f) and
A5: f /. k = (GoB f) * ((i + 1),j) and
A6: f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) ; ::_thesis: ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),(i + 1),j) )
A7: j < j + 1 by XREAL_1:29;
A8: j + 1 <= (j + 1) + 1 by NAT_1:11;
hence left_cell (f,k) = cell ((GoB f),((i + 1) -' 1),j) by A1, A2, A3, A4, A5, A6, A7, Def7
.= cell ((GoB f),i,j) by NAT_D:34 ;
::_thesis: right_cell (f,k) = cell ((GoB f),(i + 1),j)
thus right_cell (f,k) = cell ((GoB f),(i + 1),j) by A1, A2, A3, A4, A5, A6, A7, A8, Def6; ::_thesis: verum
end;
theorem Th28: :: GOBOARD5:28
for k, i, j being Element of NAT
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) holds
( left_cell (f,k) = cell ((GoB f),i,(j + 1)) & right_cell (f,k) = cell ((GoB f),i,j) )
proof
let k, i, j be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) holds
( left_cell (f,k) = cell ((GoB f),i,(j + 1)) & right_cell (f,k) = cell ((GoB f),i,j) )
let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) implies ( left_cell (f,k) = cell ((GoB f),i,(j + 1)) & right_cell (f,k) = cell ((GoB f),i,j) ) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f and
A3: [i,(j + 1)] in Indices (GoB f) and
A4: [(i + 1),(j + 1)] in Indices (GoB f) and
A5: f /. k = (GoB f) * (i,(j + 1)) and
A6: f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) ; ::_thesis: ( left_cell (f,k) = cell ((GoB f),i,(j + 1)) & right_cell (f,k) = cell ((GoB f),i,j) )
A7: i < i + 1 by XREAL_1:29;
A8: i + 1 <= (i + 1) + 1 by NAT_1:11;
hence left_cell (f,k) = cell ((GoB f),i,(j + 1)) by A1, A2, A3, A4, A5, A6, A7, Def7; ::_thesis: right_cell (f,k) = cell ((GoB f),i,j)
thus right_cell (f,k) = cell ((GoB f),i,((j + 1) -' 1)) by A1, A2, A3, A4, A5, A6, A7, A8, Def6
.= cell ((GoB f),i,j) by NAT_D:34 ; ::_thesis: verum
end;
theorem Th29: :: GOBOARD5:29
for k, i, j being Element of NAT
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * (i,(j + 1)) holds
( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),i,(j + 1)) )
proof
let k, i, j be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * (i,(j + 1)) holds
( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),i,(j + 1)) )
let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * (i,(j + 1)) implies ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),i,(j + 1)) ) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f and
A3: [i,(j + 1)] in Indices (GoB f) and
A4: [(i + 1),(j + 1)] in Indices (GoB f) and
A5: f /. k = (GoB f) * ((i + 1),(j + 1)) and
A6: f /. (k + 1) = (GoB f) * (i,(j + 1)) ; ::_thesis: ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),i,(j + 1)) )
A7: i < i + 1 by XREAL_1:29;
A8: i + 1 <= (i + 1) + 1 by NAT_1:11;
hence left_cell (f,k) = cell ((GoB f),i,((j + 1) -' 1)) by A1, A2, A3, A4, A5, A6, A7, Def7
.= cell ((GoB f),i,j) by NAT_D:34 ;
::_thesis: right_cell (f,k) = cell ((GoB f),i,(j + 1))
thus right_cell (f,k) = cell ((GoB f),i,(j + 1)) by A1, A2, A3, A4, A5, A6, A7, A8, Def6; ::_thesis: verum
end;
theorem Th30: :: GOBOARD5:30
for k, i, j being Element of NAT
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [(i + 1),(j + 1)] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),j) holds
( left_cell (f,k) = cell ((GoB f),(i + 1),j) & right_cell (f,k) = cell ((GoB f),i,j) )
proof
let k, i, j be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [(i + 1),(j + 1)] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),j) holds
( left_cell (f,k) = cell ((GoB f),(i + 1),j) & right_cell (f,k) = cell ((GoB f),i,j) )
let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f & [(i + 1),(j + 1)] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),j) implies ( left_cell (f,k) = cell ((GoB f),(i + 1),j) & right_cell (f,k) = cell ((GoB f),i,j) ) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f and
A3: [(i + 1),(j + 1)] in Indices (GoB f) and
A4: [(i + 1),j] in Indices (GoB f) and
A5: f /. k = (GoB f) * ((i + 1),(j + 1)) and
A6: f /. (k + 1) = (GoB f) * ((i + 1),j) ; ::_thesis: ( left_cell (f,k) = cell ((GoB f),(i + 1),j) & right_cell (f,k) = cell ((GoB f),i,j) )
A7: j < j + 1 by XREAL_1:29;
A8: j + 1 <= (j + 1) + 1 by NAT_1:11;
hence left_cell (f,k) = cell ((GoB f),(i + 1),j) by A1, A2, A3, A4, A5, A6, A7, Def7; ::_thesis: right_cell (f,k) = cell ((GoB f),i,j)
thus right_cell (f,k) = cell ((GoB f),((i + 1) -' 1),j) by A1, A2, A3, A4, A5, A6, A7, A8, Def6
.= cell ((GoB f),i,j) by NAT_D:34 ; ::_thesis: verum
end;
theorem :: GOBOARD5:31
for k being Element of NAT
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
(left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k)
proof
let k be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
(left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k)
let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f implies (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; ::_thesis: (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k)
k <= k + 1 by NAT_1:11;
then k <= len f by A2, XXREAL_0:2;
then A3: k in dom f by A1, FINSEQ_3:25;
then consider i1, j1 being Element of NAT such that
A4: [i1,j1] in Indices (GoB f) and
A5: f /. k = (GoB f) * (i1,j1) by Th11;
k + 1 >= 1 by NAT_1:11;
then A6: k + 1 in dom f by A2, FINSEQ_3:25;
then consider i2, j2 being Element of NAT such that
A7: [i2,j2] in Indices (GoB f) and
A8: f /. (k + 1) = (GoB f) * (i2,j2) by Th11;
A9: (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A4, A5, A6, A7, A8, Th12;
A10: now__::_thesis:_(_(_abs_(i1_-_i2)_=_1_&_j1_=_j2_&_(_i1_=_i2_+_1_or_i1_+_1_=_i2_)_&_j1_=_j2_)_or_(_i1_=_i2_&_abs_(j1_-_j2)_=_1_&_(_j1_=_j2_+_1_or_j1_+_1_=_j2_)_&_i1_=_i2_)_)
percases ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( i1 = i2 & abs (j1 - j2) = 1 ) ) by A9, SEQM_3:42;
casethat A11: abs (i1 - i2) = 1 and
A12: j1 = j2 ; ::_thesis: ( ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 )
( i1 - i2 = 1 or - (i1 - i2) = 1 ) by A11, ABSVALUE:def_1;
hence ( i1 = i2 + 1 or i1 + 1 = i2 ) ; ::_thesis: j1 = j2
thus j1 = j2 by A12; ::_thesis: verum
end;
casethat A13: i1 = i2 and
A14: abs (j1 - j2) = 1 ; ::_thesis: ( ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 )
( j1 - j2 = 1 or - (j1 - j2) = 1 ) by A14, ABSVALUE:def_1;
hence ( j1 = j2 + 1 or j1 + 1 = j2 ) ; ::_thesis: i1 = i2
thus i1 = i2 by A13; ::_thesis: verum
end;
end;
end;
A15: 0 + 1 <= j1 by A4, MATRIX_1:38;
A16: j1 <= width (GoB f) by A4, MATRIX_1:38;
A17: 1 <= j2 by A7, MATRIX_1:38;
A18: j2 <= width (GoB f) by A7, MATRIX_1:38;
A19: 0 + 1 <= i1 by A4, MATRIX_1:38;
A20: i1 <= len (GoB f) by A4, MATRIX_1:38;
A21: 1 <= i2 by A7, MATRIX_1:38;
A22: i2 <= len (GoB f) by A7, MATRIX_1:38;
i1 > 0 by A19, NAT_1:13;
then consider i being Nat such that
A23: i + 1 = i1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
A24: i + 1 = i1 by A23;
A25: i < len (GoB f) by A20, A23, NAT_1:13;
j1 > 0 by A15, NAT_1:13;
then consider j being Nat such that
A26: j + 1 = j1 by NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A27: j + 1 = j1 by A26;
A28: j < width (GoB f) by A16, A26, NAT_1:13;
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10;
supposeA29: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k)
then A30: j1 < width (GoB f) by A18, NAT_1:13;
A31: left_cell (f,k) = cell ((GoB f),i,j1) by A1, A2, A4, A5, A7, A8, A23, A29, Th27;
right_cell (f,k) = cell ((GoB f),i1,j1) by A1, A2, A4, A5, A7, A8, A24, A29, Th27;
hence (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (((GoB f) * (i1,j1)),((GoB f) * (i1,(j1 + 1)))) by A15, A23, A25, A30, A31, Th25
.= LSeg (f,k) by A1, A2, A5, A8, A29, TOPREAL1:def_3 ;
::_thesis: verum
end;
supposeA32: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k)
then A33: i1 < len (GoB f) by A22, NAT_1:13;
A34: left_cell (f,k) = cell ((GoB f),i1,j1) by A1, A2, A4, A5, A7, A8, A27, A32, Th28;
right_cell (f,k) = cell ((GoB f),i1,j) by A1, A2, A4, A5, A7, A8, A26, A32, Th28;
hence (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (((GoB f) * (i1,j1)),((GoB f) * ((i1 + 1),j1))) by A19, A26, A28, A33, A34, Th26
.= LSeg (f,k) by A1, A2, A5, A8, A32, TOPREAL1:def_3 ;
::_thesis: verum
end;
supposeA35: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k)
then A36: i2 < len (GoB f) by A20, NAT_1:13;
A37: left_cell (f,k) = cell ((GoB f),i2,j) by A1, A2, A4, A5, A7, A8, A26, A35, Th29;
right_cell (f,k) = cell ((GoB f),i2,j1) by A1, A2, A4, A5, A7, A8, A27, A35, Th29;
hence (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (((GoB f) * ((i2 + 1),j1)),((GoB f) * (i2,j1))) by A21, A26, A28, A36, A37, Th26
.= LSeg (f,k) by A1, A2, A5, A8, A35, TOPREAL1:def_3 ;
::_thesis: verum
end;
supposeA38: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k)
then A39: j2 < width (GoB f) by A16, NAT_1:13;
A40: left_cell (f,k) = cell ((GoB f),i1,j2) by A1, A2, A4, A5, A7, A8, A24, A38, Th30;
right_cell (f,k) = cell ((GoB f),i,j2) by A1, A2, A4, A5, A7, A8, A23, A38, Th30;
hence (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (((GoB f) * (i1,(j2 + 1))),((GoB f) * (i1,j2))) by A17, A23, A25, A39, A40, Th25
.= LSeg (f,k) by A1, A2, A5, A8, A38, TOPREAL1:def_3 ;
::_thesis: verum
end;
end;
end;