:: JORDAN1I semantic presentation
begin
theorem Th1: :: JORDAN1I:1
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1
A1: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then 1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69;
then 1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:70, XXREAL_0:2;
then 1 < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:71, XXREAL_0:2;
then 1 < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:72, XXREAL_0:2;
then 1 < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:73, XXREAL_0:2;
hence (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A1, SPRECT_2:74, XXREAL_0:2; ::_thesis: verum
end;
theorem Th2: :: JORDAN1I:2
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1
A1: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then 1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69;
hence (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A1, SPRECT_2:70, XXREAL_0:2; ::_thesis: verum
end;
theorem Th3: :: JORDAN1I:3
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1
A1: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then 1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69;
then 1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:70, XXREAL_0:2;
then 1 < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:71, XXREAL_0:2;
hence (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A1, SPRECT_2:72, XXREAL_0:2; ::_thesis: verum
end;
begin
theorem :: JORDAN1I:4
for f being non constant standard special_circular_sequence
for p being Point of (TOP-REAL 2) st p in rng f holds
left_cell (f,(p .. f)) = left_cell ((Rotate (f,p)),1)
proof
set n = 1;
let f be non constant standard special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f holds
left_cell (f,(p .. f)) = left_cell ((Rotate (f,p)),1)
let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f implies left_cell (f,(p .. f)) = left_cell ((Rotate (f,p)),1) )
assume A1: p in rng f ; ::_thesis: left_cell (f,(p .. f)) = left_cell ((Rotate (f,p)),1)
set k = p .. f;
len f > 1 by GOBOARD7:34, XXREAL_0:2;
then p .. f < len f by A1, SPRECT_5:7;
then A2: (p .. f) + 1 <= len f by NAT_1:13;
A3: 1 <= p .. f by A1, FINSEQ_4:21;
A4: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) & (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j2) )
proof
(Rotate (f,p)) /. (((1 + 1) + (p .. f)) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1) by NAT_D:34;
then A5: (Rotate (f,p)) /. ((((p .. f) + 1) + 1) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1) ;
A6: left_cell (f,(p .. f)) = left_cell (f,(p .. f)) ;
let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) & (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) ) implies ( i1 = i2 & j1 = j2 + 1 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j2) ) )
assume that
A7: ( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) ) and
A8: (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) and
A9: (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) ; ::_thesis: ( ( i1 = i2 & j1 + 1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) ) or ( i1 + 1 = i2 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) or ( i1 = i2 + 1 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j2) ) )
A10: GoB (Rotate (f,p)) = GoB f by REVROT_1:28;
len (Rotate (f,p)) = len f by REVROT_1:14;
then (Rotate (f,p)) /. (len f) = (Rotate (f,p)) /. 1 by FINSEQ_6:def_1;
then (Rotate (f,p)) /. (((p .. f) + (len f)) -' (p .. f)) = (Rotate (f,p)) /. 1 by NAT_D:34;
then A11: f /. (p .. f) = (GoB f) * (i1,j1) by A1, A3, A8, A10, REVROT_1:18;
p .. f < (p .. f) + 1 by NAT_1:13;
then A12: f /. ((p .. f) + 1) = (GoB f) * (i2,j2) by A1, A2, A9, A10, A5, REVROT_1:10;
then A13: ( ( i1 = i2 & j1 + 1 = j2 & left_cell (f,(p .. f)) = cell ((GoB f),(i1 -' 1),j1) ) or ( i1 + 1 = i2 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB f),i1,j1) ) or ( i1 = i2 + 1 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB f),i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell (f,(p .. f)) = cell ((GoB f),i1,j2) ) ) by A3, A2, A7, A10, A11, A6, GOBOARD5:def_7;
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 A3, A2, A7, A10, A11, A12, A6, GOBOARD5:def_7;
case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1)
hence left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) by A13, REVROT_1:28; ::_thesis: verum
end;
case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1)
hence left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) by A13, REVROT_1:28; ::_thesis: verum
end;
case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1))
hence left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) by A13, REVROT_1:28; ::_thesis: verum
end;
case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j2)
hence left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j2) by A13, REVROT_1:28; ::_thesis: verum
end;
end;
end;
1 + 1 <= len (Rotate (f,p)) by GOBOARD7:34, XXREAL_0:2;
hence left_cell (f,(p .. f)) = left_cell ((Rotate (f,p)),1) by A4, GOBOARD5:def_7; ::_thesis: verum
end;
theorem Th5: :: JORDAN1I:5
for f being non constant standard special_circular_sequence
for p being Point of (TOP-REAL 2) st p in rng f holds
right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1)
proof
set n = 1;
let f be non constant standard special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f holds
right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1)
let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f implies right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1) )
assume A1: p in rng f ; ::_thesis: right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1)
set k = p .. f;
len f > 1 by GOBOARD7:34, XXREAL_0:2;
then p .. f < len f by A1, SPRECT_5:7;
then A2: (p .. f) + 1 <= len f by NAT_1:13;
A3: 1 <= p .. f by A1, FINSEQ_4:21;
A4: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) & (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2) )
proof
(Rotate (f,p)) /. (((1 + 1) + (p .. f)) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1) by NAT_D:34;
then A5: (Rotate (f,p)) /. ((((p .. f) + 1) + 1) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1) ;
A6: right_cell (f,(p .. f)) = right_cell (f,(p .. f)) ;
let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) & (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2) ) implies ( i1 = i2 & j1 = j2 + 1 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2) ) )
assume that
A7: ( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) ) and
A8: (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) and
A9: (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) ; ::_thesis: ( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2) ) )
A10: GoB (Rotate (f,p)) = GoB f by REVROT_1:28;
len (Rotate (f,p)) = len f by REVROT_1:14;
then (Rotate (f,p)) /. (len f) = (Rotate (f,p)) /. 1 by FINSEQ_6:def_1;
then (Rotate (f,p)) /. (((p .. f) + (len f)) -' (p .. f)) = (Rotate (f,p)) /. 1 by NAT_D:34;
then A11: f /. (p .. f) = (GoB f) * (i1,j1) by A1, A3, A8, A10, REVROT_1:18;
p .. f < (p .. f) + 1 by NAT_1:13;
then A12: f /. ((p .. f) + 1) = (GoB f) * (i2,j2) by A1, A2, A9, A10, A5, REVROT_1:10;
then A13: ( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,(p .. f)) = cell ((GoB f),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB f),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB f),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,(p .. f)) = cell ((GoB f),(i1 -' 1),j2) ) ) by A3, A2, A7, A10, A11, A6, GOBOARD5:def_6;
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 A3, A2, A7, A10, A11, A12, A6, GOBOARD5:def_6;
case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1)
hence right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) by A13, REVROT_1:28; ::_thesis: verum
end;
case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1))
hence right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1)) by A13, REVROT_1:28; ::_thesis: verum
end;
case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2)
hence right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2) by A13, REVROT_1:28; ::_thesis: verum
end;
case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2)
hence right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2) by A13, REVROT_1:28; ::_thesis: verum
end;
end;
end;
1 + 1 <= len (Rotate (f,p)) by GOBOARD7:34, XXREAL_0:2;
hence right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1) by A4, GOBOARD5:def_6; ::_thesis: verum
end;
theorem :: JORDAN1I:6
for n being Element of NAT
for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1)
proof
let n be Element of NAT ; ::_thesis: for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1)
let C be non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1)
set f = Cage (C,n);
set G = Gauge (C,n);
consider j being Element of NAT such that
A1: 1 <= j and
A2: j <= width (Gauge (C,n)) and
A3: W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) by JORDAN1D:30;
A4: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A5: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
set k = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n));
A6: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
then A7: ( (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) & (Cage (C,n)) . ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = W-min (L~ (Cage (C,n))) ) by FINSEQ_4:19, FINSEQ_4:20;
then A8: (Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = W-min (L~ (Cage (C,n))) by PARTFUN1:def_6;
A9: now__::_thesis:_not_(W-min_(L~_(Cage_(C,n))))_.._(Cage_(C,n))_=_len_(Cage_(C,n))
A10: 1 < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th1;
A11: 1 in dom (Cage (C,n)) by A6, FINSEQ_3:31;
assume (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n)) ; ::_thesis: contradiction
then (Cage (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by A8, FINSEQ_6:def_1;
then (Cage (C,n)) . 1 = W-min (L~ (Cage (C,n))) by A11, PARTFUN1:def_6;
hence contradiction by A11, A10, FINSEQ_4:24; ::_thesis: verum
end;
1 <= len (Gauge (C,n)) by A4, XXREAL_0:2;
then A12: [1,j] in Indices (Gauge (C,n)) by A1, A2, MATRIX_1:36;
then A13: [1,j] in Indices (GoB (Cage (C,n))) by JORDAN1H:44;
(W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= len (Cage (C,n)) by A6, FINSEQ_4:21;
then (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A9, XXREAL_0:1;
then A14: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;
(Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (1,j) by A3, A7, PARTFUN1:def_6;
then A15: (Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * (1,j) by JORDAN1H:44;
set p = W-min C;
A16: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
A17: 1 <= ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:11;
then A18: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A14, FINSEQ_3:25;
A19: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A14, A17, FINSEQ_3:25;
then consider ki, kj being Element of NAT such that
A20: [ki,kj] in Indices (Gauge (C,n)) and
A21: (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (ki,kj) by A16, GOBOARD1:def_9;
A22: ( 1 <= kj & ki <= len (Gauge (C,n)) ) by A20, MATRIX_1:38;
A23: 1 <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th1;
then A24: ((Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = W-bound (L~ (Cage (C,n))) by A8, A14, JORDAN1E:22;
then ((Gauge (C,n)) * (1,j)) `1 = ((Gauge (C,n)) * (ki,kj)) `1 by A3, A21, EUCLID:52;
then A25: ki = 1 by A20, A12, JORDAN1G:7;
2 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2;
then (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in W-most (L~ (Cage (C,n))) by A24, A19, GOBOARD1:1, SPRECT_2:12;
then ((Gauge (C,n)) * (1,j)) `2 <= ((Gauge (C,n)) * (ki,kj)) `2 by A3, A21, PSCOMP_1:31;
then A26: j <= kj by A2, A25, A22, GOBOARD5:4;
( [ki,kj] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (GoB (Cage (C,n))) * (ki,kj) ) by A20, A21, JORDAN1H:44;
then (abs (1 - ki)) + (abs (j - kj)) = 1 by A6, A18, A13, A15, FINSEQ_4:20, GOBOARD5:12;
then A27: 0 + (abs (j - kj)) = 1 by A25, ABSVALUE:2;
then A28: (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (1,(j + 1)) by A21, A25, A26, SEQM_3:41;
A29: kj = j + 1 by A26, A27, SEQM_3:41;
then ( 1 <= j + 1 & j + 1 <= width (Gauge (C,n)) ) by A20, MATRIX_1:38;
then [1,(j + 1)] in Indices (Gauge (C,n)) by A5, MATRIX_1:36;
then A30: right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),1,j) by A3, A16, A23, A8, A14, A12, A28, GOBRD13:22;
A31: now__::_thesis:_W-min_C_in_right_cell_((Cage_(C,n)),((W-min_(L~_(Cage_(C,n))))_.._(Cage_(C,n))),(Gauge_(C,n)))
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
then A32: j + 1 <= len (Gauge (C,n)) by A20, A29, MATRIX_1:38;
1 <= j + 1 by A20, A29, MATRIX_1:38;
then A33: ((Gauge (C,n)) * (2,(j + 1))) `1 = W-bound C by A32, JORDAN8:11;
assume A34: not W-min C in right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) ; ::_thesis: contradiction
j + 1 <= width (Gauge (C,n)) by A20, A29, MATRIX_1:38;
then A35: j < width (Gauge (C,n)) by NAT_1:13;
A36: 2 <= len (Gauge (C,n)) by A4, XXREAL_0:2;
1 < len (Gauge (C,n)) by A4, XXREAL_0:2;
then LSeg (((Gauge (C,n)) * ((1 + 1),j)),((Gauge (C,n)) * ((1 + 1),(j + 1)))) c= cell ((Gauge (C,n)),1,j) by A1, A35, GOBOARD5:18;
then A37: not W-min C in LSeg (((Gauge (C,n)) * (2,j)),((Gauge (C,n)) * (2,(j + 1)))) by A30, A34;
A38: ( 1 <= j + 1 & j + 1 <= width (Gauge (C,n)) ) by A20, A29, MATRIX_1:38;
j <= len (Gauge (C,n)) by A2, JORDAN8:def_1;
then A39: ((Gauge (C,n)) * (2,j)) `1 = W-bound C by A1, JORDAN8:11;
(W-min C) `1 = W-bound C by EUCLID:52;
then A40: ( (W-min C) `2 > ((Gauge (C,n)) * (2,(j + 1))) `2 or (W-min C) `2 < ((Gauge (C,n)) * (2,j)) `2 ) by A37, A39, A33, GOBOARD7:7;
percases ( (W-min C) `2 > ((Gauge (C,n)) * (1,(j + 1))) `2 or (W-min C) `2 < ((Gauge (C,n)) * (1,j)) `2 ) by A1, A2, A40, A38, A36, GOBOARD5:1;
supposeA41: (W-min C) `2 > ((Gauge (C,n)) * (1,(j + 1))) `2 ; ::_thesis: contradiction
cell ((Gauge (C,n)),1,j) meets C by A23, A14, A30, JORDAN9:31;
then (cell ((Gauge (C,n)),1,j)) /\ C <> {} by XBOOLE_0:def_7;
then consider c being set such that
A42: c in (cell ((Gauge (C,n)),1,j)) /\ C by XBOOLE_0:def_1;
reconsider c = c as Element of (TOP-REAL 2) by A42;
A43: c in cell ((Gauge (C,n)),1,j) by A42, XBOOLE_0:def_4;
A44: c in C by A42, XBOOLE_0:def_4;
then A45: c `1 >= W-bound C by PSCOMP_1:24;
A46: ( 1 + 1 <= len (Gauge (C,n)) & j + 1 <= width (Gauge (C,n)) ) by A4, A20, A29, MATRIX_1:38, XXREAL_0:2;
then c `1 <= ((Gauge (C,n)) * ((1 + 1),j)) `1 by A1, A43, JORDAN9:17;
then c in W-most C by A39, A44, A45, SPRECT_2:12, XXREAL_0:1;
then A47: c `2 >= (W-min C) `2 by PSCOMP_1:31;
c `2 <= ((Gauge (C,n)) * (1,(j + 1))) `2 by A1, A43, A46, JORDAN9:17;
hence contradiction by A41, A47, XXREAL_0:2; ::_thesis: verum
end;
supposeA48: (W-min C) `2 < ((Gauge (C,n)) * (1,j)) `2 ; ::_thesis: contradiction
west_halfline (W-min C) meets L~ (Cage (C,n)) by JORDAN1A:54, SPRECT_1:13;
then consider r being set such that
A49: r in west_halfline (W-min C) and
A50: r in L~ (Cage (C,n)) by XBOOLE_0:3;
reconsider r = r as Element of (TOP-REAL 2) by A49;
r in (west_halfline (W-min C)) /\ (L~ (Cage (C,n))) by A49, A50, XBOOLE_0:def_4;
then r `1 = W-bound (L~ (Cage (C,n))) by JORDAN1A:85, PSCOMP_1:34;
then r in W-most (L~ (Cage (C,n))) by A50, SPRECT_2:12;
then (W-min (L~ (Cage (C,n)))) `2 <= r `2 by PSCOMP_1:31;
hence contradiction by A3, A48, A49, TOPREAL1:def_13; ::_thesis: verum
end;
end;
end;
GoB (Cage (C,n)) = Gauge (C,n) by JORDAN1H:44;
then W-min C in right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A23, A14, A31, JORDAN1H:23;
hence W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1) by A6, Th5; ::_thesis: verum
end;
theorem :: JORDAN1I:7
for n being Element of NAT
for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1)
proof
let n be Element of NAT ; ::_thesis: for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1)
let C be non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1)
set f = Cage (C,n);
set G = Gauge (C,n);
consider j being Element of NAT such that
A1: 1 <= j and
A2: j <= width (Gauge (C,n)) and
A3: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by JORDAN1D:25;
A4: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A5: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
set k = (E-max (L~ (Cage (C,n)))) .. (Cage (C,n));
A6: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A7: ( (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) & (Cage (C,n)) . ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = E-max (L~ (Cage (C,n))) ) by FINSEQ_4:19, FINSEQ_4:20;
then A8: (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = E-max (L~ (Cage (C,n))) by PARTFUN1:def_6;
A9: now__::_thesis:_not_(E-max_(L~_(Cage_(C,n))))_.._(Cage_(C,n))_=_len_(Cage_(C,n))
A10: 1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th2;
A11: 1 in dom (Cage (C,n)) by A6, FINSEQ_3:31;
assume (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n)) ; ::_thesis: contradiction
then (Cage (C,n)) /. 1 = E-max (L~ (Cage (C,n))) by A8, FINSEQ_6:def_1;
then (Cage (C,n)) . 1 = E-max (L~ (Cage (C,n))) by A11, PARTFUN1:def_6;
hence contradiction by A11, A10, FINSEQ_4:24; ::_thesis: verum
end;
(Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by A3, A7, PARTFUN1:def_6;
then A12: (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * ((len (Gauge (C,n))),j) by JORDAN1H:44;
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= len (Cage (C,n)) by A6, FINSEQ_4:21;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A9, XXREAL_0:1;
then A13: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;
A14: 1 <= len (Gauge (C,n)) by A4, XXREAL_0:2;
then A15: [(len (Gauge (C,n))),j] in Indices (Gauge (C,n)) by A1, A2, MATRIX_1:36;
( 1 <= (j -' 1) + 1 & (j -' 1) + 1 <= width (Gauge (C,n)) ) by A1, A2, XREAL_1:235;
then A16: [(len (Gauge (C,n))),((j -' 1) + 1)] in Indices (Gauge (C,n)) by A14, MATRIX_1:36;
set p = E-max C;
A17: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
A18: 1 <= ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:11;
then A19: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A13, FINSEQ_3:25;
A20: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A13, A18, FINSEQ_3:25;
then consider ki, kj being Element of NAT such that
A21: [ki,kj] in Indices (Gauge (C,n)) and
A22: (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (ki,kj) by A17, GOBOARD1:def_9;
A23: ( [ki,kj] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (GoB (Cage (C,n))) * (ki,kj) ) by A21, A22, JORDAN1H:44;
A24: 1 <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th2;
then A25: ((Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = E-bound (L~ (Cage (C,n))) by A8, A13, JORDAN1E:20;
then ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 = ((Gauge (C,n)) * (ki,kj)) `1 by A3, A22, EUCLID:52;
then A26: ki = len (Gauge (C,n)) by A21, A15, JORDAN1G:7;
A27: ( kj <= width (Gauge (C,n)) & 1 <= ki ) by A21, MATRIX_1:38;
[(len (Gauge (C,n))),j] in Indices (GoB (Cage (C,n))) by A15, JORDAN1H:44;
then (abs ((len (Gauge (C,n))) - ki)) + (abs (j - kj)) = 1 by A6, A19, A12, A23, FINSEQ_4:20, GOBOARD5:12;
then A28: 0 + (abs (j - kj)) = 1 by A26, ABSVALUE:2;
2 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2;
then (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in E-most (L~ (Cage (C,n))) by A25, A20, GOBOARD1:1, SPRECT_2:13;
then ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 >= ((Gauge (C,n)) * (ki,kj)) `2 by A3, A22, PSCOMP_1:47;
then j >= kj by A1, A26, A27, GOBOARD5:4;
then j = kj + 1 by A28, SEQM_3:41;
then kj = j - 1 ;
then A29: kj = j -' 1 by A1, XREAL_1:233;
then A30: 1 <= j -' 1 by A21, MATRIX_1:38;
A31: j -' 1 <= width (Gauge (C,n)) by A21, A29, MATRIX_1:38;
(Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),((j -' 1) + 1)) by A1, A3, A8, XREAL_1:235;
then A32: right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by A17, A24, A13, A21, A22, A26, A29, A16, GOBRD13:28;
A33: now__::_thesis:_E-max_C_in_right_cell_((Cage_(C,n)),((E-max_(L~_(Cage_(C,n))))_.._(Cage_(C,n))),(Gauge_(C,n)))
j -' 1 <= len (Gauge (C,n)) by A31, JORDAN8:def_1;
then A34: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `1 = E-bound C by A30, JORDAN8:12;
j <= len (Gauge (C,n)) by A2, JORDAN8:def_1;
then A35: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `1 = E-bound C by A1, JORDAN8:12;
assume A36: not E-max C in right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) ; ::_thesis: contradiction
A37: 1 < len (Gauge (C,n)) by A4, XXREAL_0:2;
then A38: 1 <= (len (Gauge (C,n))) -' 1 by NAT_D:49;
A39: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:50;
then A40: ( ((Gauge (C,n)) * (1,j)) `2 = ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `2 & ((Gauge (C,n)) * (1,(j -' 1))) `2 = ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 ) by A1, A2, A30, A31, A38, GOBOARD5:1;
j -' 1 < j by A30, NAT_D:51;
then j -' 1 < width (Gauge (C,n)) by A2, XXREAL_0:2;
then LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),((j -' 1) + 1)))) c= cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by A30, A38, A39, GOBOARD5:19;
then not E-max C in LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),((j -' 1) + 1)))) by A32, A36;
then A41: not E-max C in LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j))) by A1, XREAL_1:235;
(E-max C) `1 = E-bound C by EUCLID:52;
then A42: ( (E-max C) `2 > ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `2 or (E-max C) `2 < ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 ) by A41, A34, A35, GOBOARD7:7;
percases ( (E-max C) `2 < ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 or (E-max C) `2 > ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 ) by A1, A2, A5, A30, A31, A42, A40, GOBOARD5:1;
supposeA43: (E-max C) `2 < ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 ; ::_thesis: contradiction
A44: ( 1 <= j -' 1 & (j -' 1) + 1 <= width (Gauge (C,n)) ) by A1, A2, A21, A29, MATRIX_1:38, XREAL_1:235;
cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) meets C by A24, A13, A32, JORDAN9:31;
then (cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1))) /\ C <> {} by XBOOLE_0:def_7;
then consider c being set such that
A45: c in (cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1))) /\ C by XBOOLE_0:def_1;
reconsider c = c as Element of (TOP-REAL 2) by A45;
A46: ( 1 <= (len (Gauge (C,n))) -' 1 & ((len (Gauge (C,n))) -' 1) + 1 <= len (Gauge (C,n)) ) by A37, NAT_D:49, XREAL_1:235;
A47: c in cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by A45, XBOOLE_0:def_4;
then A48: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `1 <= c `1 by A46, A44, JORDAN9:17;
A49: c in C by A45, XBOOLE_0:def_4;
then c `1 <= E-bound C by PSCOMP_1:24;
then c in E-most C by A34, A49, A48, SPRECT_2:13, XXREAL_0:1;
then A50: c `2 <= (E-max C) `2 by PSCOMP_1:47;
((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 <= c `2 by A47, A46, A44, JORDAN9:17;
then ((Gauge (C,n)) * (1,(j -' 1))) `2 <= c `2 by A30, A31, A38, A39, GOBOARD5:1;
then ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 <= c `2 by A5, A30, A31, GOBOARD5:1;
hence contradiction by A43, A50, XXREAL_0:2; ::_thesis: verum
end;
supposeA51: (E-max C) `2 > ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 ; ::_thesis: contradiction
east_halfline (E-max C) meets L~ (Cage (C,n)) by JORDAN1A:52, SPRECT_1:14;
then consider r being set such that
A52: r in east_halfline (E-max C) and
A53: r in L~ (Cage (C,n)) by XBOOLE_0:3;
reconsider r = r as Element of (TOP-REAL 2) by A52;
r in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A52, A53, XBOOLE_0:def_4;
then r `1 = E-bound (L~ (Cage (C,n))) by JORDAN1A:83, PSCOMP_1:50;
then r in E-most (L~ (Cage (C,n))) by A53, SPRECT_2:13;
then (E-max (L~ (Cage (C,n)))) `2 >= r `2 by PSCOMP_1:47;
hence contradiction by A3, A51, A52, TOPREAL1:def_11; ::_thesis: verum
end;
end;
end;
GoB (Cage (C,n)) = Gauge (C,n) by JORDAN1H:44;
then E-max C in right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A24, A13, A33, JORDAN1H:23;
hence E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) by A6, Th5; ::_thesis: verum
end;
theorem :: JORDAN1I:8
for n being Element of NAT
for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (L~ (Cage (C,n)))))),1)
proof
let n be Element of NAT ; ::_thesis: for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (L~ (Cage (C,n)))))),1)
let C be non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (L~ (Cage (C,n)))))),1)
set f = Cage (C,n);
set G = Gauge (C,n);
consider j being Element of NAT such that
A1: 1 <= j and
A2: j <= len (Gauge (C,n)) and
A3: S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (j,1) by JORDAN1D:28;
A4: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
set k = (S-max (L~ (Cage (C,n)))) .. (Cage (C,n));
A5: S-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:42;
then A6: ( (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) & (Cage (C,n)) . ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = S-max (L~ (Cage (C,n))) ) by FINSEQ_4:19, FINSEQ_4:20;
then A7: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = S-max (L~ (Cage (C,n))) by PARTFUN1:def_6;
A8: now__::_thesis:_not_(S-max_(L~_(Cage_(C,n))))_.._(Cage_(C,n))_=_len_(Cage_(C,n))
A9: 1 < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th3;
A10: 1 in dom (Cage (C,n)) by A5, FINSEQ_3:31;
assume (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n)) ; ::_thesis: contradiction
then (Cage (C,n)) /. 1 = S-max (L~ (Cage (C,n))) by A7, FINSEQ_6:def_1;
then (Cage (C,n)) . 1 = S-max (L~ (Cage (C,n))) by A10, PARTFUN1:def_6;
hence contradiction by A10, A9, FINSEQ_4:24; ::_thesis: verum
end;
(S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= len (Cage (C,n)) by A5, FINSEQ_4:21;
then (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A8, XXREAL_0:1;
then A11: ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;
A12: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (((j -' 1) + 1),1) by A1, A3, A7, XREAL_1:235;
(Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (j,1) by A3, A6, PARTFUN1:def_6;
then A13: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * (j,1) by JORDAN1H:44;
set p = S-max C;
A14: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A15: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A16: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
A17: 1 <= ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:11;
then A18: ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A11, FINSEQ_3:25;
A19: ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A11, A17, FINSEQ_3:25;
then consider kj, ki being Element of NAT such that
A20: [kj,ki] in Indices (Gauge (C,n)) and
A21: (Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (kj,ki) by A4, GOBOARD1:def_9;
A22: ( [kj,ki] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (GoB (Cage (C,n))) * (kj,ki) ) by A20, A21, JORDAN1H:44;
A23: ki <= width (Gauge (C,n)) by A20, MATRIX_1:38;
A24: 1 <= kj by A20, MATRIX_1:38;
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
then A25: [j,1] in Indices (Gauge (C,n)) by A1, A2, A16, MATRIX_1:36;
then A26: [((j -' 1) + 1),1] in Indices (Gauge (C,n)) by A1, XREAL_1:235;
A27: 1 <= (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th3;
then A28: ((Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `2 = S-bound (L~ (Cage (C,n))) by A7, A11, JORDAN1E:21;
then ((Gauge (C,n)) * (j,1)) `2 = ((Gauge (C,n)) * (kj,ki)) `2 by A3, A21, EUCLID:52;
then A29: ki = 1 by A20, A25, JORDAN1G:6;
[j,1] in Indices (GoB (Cage (C,n))) by A25, JORDAN1H:44;
then (abs (1 - ki)) + (abs (j - kj)) = 1 by A5, A18, A13, A22, FINSEQ_4:20, GOBOARD5:12;
then A30: 0 + (abs (j - kj)) = 1 by A29, ABSVALUE:2;
A31: kj <= len (Gauge (C,n)) by A20, MATRIX_1:38;
2 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2;
then (Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in S-most (L~ (Cage (C,n))) by A28, A19, GOBOARD1:1, SPRECT_2:11;
then ((Gauge (C,n)) * (j,1)) `1 >= ((Gauge (C,n)) * (kj,ki)) `1 by A3, A21, PSCOMP_1:55;
then kj <= j by A1, A29, A23, A31, GOBOARD5:3;
then kj + 1 = j by A30, SEQM_3:41;
then A32: kj = j - 1 ;
then kj = j -' 1 by A24, NAT_D:39;
then A33: [(j -' 1),1] in Indices (Gauge (C,n)) by A16, A24, A31, A14, MATRIX_1:36;
(Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * ((j -' 1),1) by A21, A29, A24, A32, NAT_D:39;
then A34: right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),(j -' 1),1) by A4, A27, A11, A33, A26, A12, GOBRD13:26;
A35: now__::_thesis:_S-max_C_in_right_cell_((Cage_(C,n)),((S-max_(L~_(Cage_(C,n))))_.._(Cage_(C,n))),(Gauge_(C,n)))
1 < len (Gauge (C,n)) by A15, XXREAL_0:2;
then A36: 1 < width (Gauge (C,n)) by JORDAN8:def_1;
assume A37: not S-max C in right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) ; ::_thesis: contradiction
A38: 1 <= j -' 1 by A24, A32, NAT_D:39;
then j -' 1 < j by NAT_D:51;
then j -' 1 < len (Gauge (C,n)) by A2, XXREAL_0:2;
then LSeg (((Gauge (C,n)) * ((j -' 1),(1 + 1))),((Gauge (C,n)) * (((j -' 1) + 1),(1 + 1)))) c= cell ((Gauge (C,n)),(j -' 1),1) by A36, A38, GOBOARD5:21;
then LSeg (((Gauge (C,n)) * ((j -' 1),2)),((Gauge (C,n)) * (j,2))) c= cell ((Gauge (C,n)),(j -' 1),1) by A1, XREAL_1:235;
then A39: not S-max C in LSeg (((Gauge (C,n)) * ((j -' 1),2)),((Gauge (C,n)) * (j,2))) by A34, A37;
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
then A40: 2 <= width (Gauge (C,n)) by A15, XXREAL_0:2;
A41: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A42: j -' 1 <= len (Gauge (C,n)) by A24, A31, A32, NAT_D:39;
then A43: ((Gauge (C,n)) * ((j -' 1),2)) `2 = S-bound C by A38, JORDAN8:13;
( ((Gauge (C,n)) * (j,2)) `2 = S-bound C & (S-max C) `2 = S-bound C ) by A1, A2, EUCLID:52, JORDAN8:13;
then A44: ( (S-max C) `1 > ((Gauge (C,n)) * (j,2)) `1 or (S-max C) `1 < ((Gauge (C,n)) * ((j -' 1),2)) `1 ) by A39, A43, GOBOARD7:8;
percases ( (S-max C) `1 < ((Gauge (C,n)) * ((j -' 1),1)) `1 or (S-max C) `1 > ((Gauge (C,n)) * (j,1)) `1 ) by A1, A2, A38, A42, A44, A40, GOBOARD5:2;
supposeA45: (S-max C) `1 < ((Gauge (C,n)) * ((j -' 1),1)) `1 ; ::_thesis: contradiction
cell ((Gauge (C,n)),(j -' 1),1) meets C by A27, A11, A34, JORDAN9:31;
then (cell ((Gauge (C,n)),(j -' 1),1)) /\ C <> {} by XBOOLE_0:def_7;
then consider c being set such that
A46: c in (cell ((Gauge (C,n)),(j -' 1),1)) /\ C by XBOOLE_0:def_1;
reconsider c = c as Element of (TOP-REAL 2) by A46;
A47: c in cell ((Gauge (C,n)),(j -' 1),1) by A46, XBOOLE_0:def_4;
A48: c in C by A46, XBOOLE_0:def_4;
then A49: c `2 >= S-bound C by PSCOMP_1:24;
A50: ( (j -' 1) + 1 <= len (Gauge (C,n)) & 1 + 1 <= width (Gauge (C,n)) ) by A1, A2, A15, A41, XREAL_1:235, XXREAL_0:2;
then c `2 <= ((Gauge (C,n)) * ((j -' 1),(1 + 1))) `2 by A38, A47, JORDAN9:17;
then c in S-most C by A43, A48, A49, SPRECT_2:11, XXREAL_0:1;
then A51: c `1 <= (S-max C) `1 by PSCOMP_1:55;
((Gauge (C,n)) * ((j -' 1),1)) `1 <= c `1 by A38, A47, A50, JORDAN9:17;
hence contradiction by A45, A51, XXREAL_0:2; ::_thesis: verum
end;
supposeA52: (S-max C) `1 > ((Gauge (C,n)) * (j,1)) `1 ; ::_thesis: contradiction
south_halfline (S-max C) meets L~ (Cage (C,n)) by JORDAN1A:53, SPRECT_1:12;
then consider r being set such that
A53: r in south_halfline (S-max C) and
A54: r in L~ (Cage (C,n)) by XBOOLE_0:3;
reconsider r = r as Element of (TOP-REAL 2) by A53;
r in (south_halfline (S-max C)) /\ (L~ (Cage (C,n))) by A53, A54, XBOOLE_0:def_4;
then r `2 = S-bound (L~ (Cage (C,n))) by JORDAN1A:84, PSCOMP_1:58;
then r in S-most (L~ (Cage (C,n))) by A54, SPRECT_2:11;
then (S-max (L~ (Cage (C,n)))) `1 >= r `1 by PSCOMP_1:55;
hence contradiction by A3, A52, A53, TOPREAL1:def_12; ::_thesis: verum
end;
end;
end;
GoB (Cage (C,n)) = Gauge (C,n) by JORDAN1H:44;
then S-max C in right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A27, A11, A35, JORDAN1H:23;
hence S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (L~ (Cage (C,n)))))),1) by A5, Th5; ::_thesis: verum
end;
begin
theorem Th9: :: JORDAN1I:9
for f being non constant standard clockwise_oriented special_circular_sequence
for p being Point of (TOP-REAL 2) st p `1 < W-bound (L~ f) holds
p in LeftComp f
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st p `1 < W-bound (L~ f) holds
p in LeftComp f
let p be Point of (TOP-REAL 2); ::_thesis: ( p `1 < W-bound (L~ f) implies p in LeftComp f )
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
assume A2: p `1 < W-bound (L~ f) ; ::_thesis: p in LeftComp f
N-min (L~ f) in rng f by SPRECT_2:39;
then (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
then p in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:110;
hence p in LeftComp f by REVROT_1:36; ::_thesis: verum
end;
theorem Th10: :: JORDAN1I:10
for f being non constant standard clockwise_oriented special_circular_sequence
for p being Point of (TOP-REAL 2) st p `1 > E-bound (L~ f) holds
p in LeftComp f
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st p `1 > E-bound (L~ f) holds
p in LeftComp f
let p be Point of (TOP-REAL 2); ::_thesis: ( p `1 > E-bound (L~ f) implies p in LeftComp f )
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
assume A2: p `1 > E-bound (L~ f) ; ::_thesis: p in LeftComp f
N-min (L~ f) in rng f by SPRECT_2:39;
then (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
then p in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:111;
hence p in LeftComp f by REVROT_1:36; ::_thesis: verum
end;
theorem Th11: :: JORDAN1I:11
for f being non constant standard clockwise_oriented special_circular_sequence
for p being Point of (TOP-REAL 2) st p `2 < S-bound (L~ f) holds
p in LeftComp f
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st p `2 < S-bound (L~ f) holds
p in LeftComp f
let p be Point of (TOP-REAL 2); ::_thesis: ( p `2 < S-bound (L~ f) implies p in LeftComp f )
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
assume A2: p `2 < S-bound (L~ f) ; ::_thesis: p in LeftComp f
N-min (L~ f) in rng f by SPRECT_2:39;
then (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
then p in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:112;
hence p in LeftComp f by REVROT_1:36; ::_thesis: verum
end;
theorem Th12: :: JORDAN1I:12
for f being non constant standard clockwise_oriented special_circular_sequence
for p being Point of (TOP-REAL 2) st p `2 > N-bound (L~ f) holds
p in LeftComp f
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st p `2 > N-bound (L~ f) holds
p in LeftComp f
let p be Point of (TOP-REAL 2); ::_thesis: ( p `2 > N-bound (L~ f) implies p in LeftComp f )
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
assume A2: p `2 > N-bound (L~ f) ; ::_thesis: p in LeftComp f
N-min (L~ f) in rng f by SPRECT_2:39;
then (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
then p in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:113;
hence p in LeftComp f by REVROT_1:36; ::_thesis: verum
end;
theorem Th13: :: JORDAN1I:13
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds
j < width G
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds
j < width G
let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds
j < width G )
assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds
j < width G
let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) implies j < width G )
assume that
A2: ( 1 <= k & k + 1 <= len f ) and
A3: [i,j] in Indices G and
A4: ( [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) ) ; ::_thesis: j < width G
assume A5: j >= width G ; ::_thesis: contradiction
j <= width G by A3, MATRIX_1:38;
then A6: j = width G by A5, XXREAL_0:1;
A7: i <= len G by A3, MATRIX_1:38;
right_cell (f,k,G) = cell (G,i,j) by A1, A2, A3, A4, GOBRD13:26;
then not (right_cell (f,k,G)) \ (L~ f) is bounded by A7, A6, JORDAN1A:27, TOPREAL6:90;
then not RightComp f is bounded by A1, A2, JORDAN9:27, RLTOPSP1:42;
then not BDD (L~ f) is bounded by GOBRD14:37;
hence contradiction by JORDAN2C:106; ::_thesis: verum
end;
theorem Th14: :: JORDAN1I:14
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
i < len G
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
i < len G
let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
i < len G )
assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
i < len G
let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) implies i < len G )
assume that
A2: ( 1 <= k & k + 1 <= len f ) and
A3: [i,j] in Indices G and
A4: ( [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) ) ; ::_thesis: i < len G
assume A5: i >= len G ; ::_thesis: contradiction
i <= len G by A3, MATRIX_1:38;
then A6: i = len G by A5, XXREAL_0:1;
A7: j <= width G by A3, MATRIX_1:38;
right_cell (f,k,G) = cell (G,i,j) by A1, A2, A3, A4, GOBRD13:22;
then not (right_cell (f,k,G)) \ (L~ f) is bounded by A7, A6, JORDAN1B:34, TOPREAL6:90;
then not RightComp f is bounded by A1, A2, JORDAN9:27, RLTOPSP1:42;
then not BDD (L~ f) is bounded by GOBRD14:37;
hence contradiction by JORDAN2C:106; ::_thesis: verum
end;
theorem Th15: :: JORDAN1I:15
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds
j > 1
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds
j > 1
let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds
j > 1 )
assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds
j > 1
let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) implies j > 1 )
assume that
A2: ( 1 <= k & k + 1 <= len f ) and
A3: [i,j] in Indices G and
A4: ( [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) ) ; ::_thesis: j > 1
assume A5: j <= 1 ; ::_thesis: contradiction
1 <= j by A3, MATRIX_1:38;
then j = 1 by A5, XXREAL_0:1;
then A6: j -' 1 = 0 by XREAL_1:232;
A7: i <= len G by A3, MATRIX_1:38;
right_cell (f,k,G) = cell (G,i,(j -' 1)) by A1, A2, A3, A4, GOBRD13:24;
then not (right_cell (f,k,G)) \ (L~ f) is bounded by A7, A6, JORDAN1A:26, TOPREAL6:90;
then not RightComp f is bounded by A1, A2, JORDAN9:27, RLTOPSP1:42;
then not BDD (L~ f) is bounded by GOBRD14:37;
hence contradiction by JORDAN2C:106; ::_thesis: verum
end;
theorem Th16: :: JORDAN1I:16
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
i > 1
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
i > 1
let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
i > 1 )
assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
i > 1
let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) implies i > 1 )
assume that
A2: ( 1 <= k & k + 1 <= len f ) and
A3: [i,j] in Indices G and
A4: ( [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) ) ; ::_thesis: i > 1
assume A5: i <= 1 ; ::_thesis: contradiction
1 <= i by A3, MATRIX_1:38;
then i = 1 by A5, XXREAL_0:1;
then A6: i -' 1 = 0 by XREAL_1:232;
A7: j <= width G by A3, MATRIX_1:38;
right_cell (f,k,G) = cell (G,(i -' 1),j) by A1, A2, A3, A4, GOBRD13:28;
then not (right_cell (f,k,G)) \ (L~ f) is bounded by A7, A6, JORDAN1B:33, TOPREAL6:90;
then not RightComp f is bounded by A1, A2, JORDAN9:27, RLTOPSP1:42;
then not BDD (L~ f) is bounded by GOBRD14:37;
hence contradiction by JORDAN2C:106; ::_thesis: verum
end;
theorem Th17: :: JORDAN1I:17
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds
(f /. k) `2 <> N-bound (L~ f)
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds
(f /. k) `2 <> N-bound (L~ f)
let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds
(f /. k) `2 <> N-bound (L~ f) )
assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds
(f /. k) `2 <> N-bound (L~ f)
let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) implies (f /. k) `2 <> N-bound (L~ f) )
assume that
A2: ( 1 <= k & k + 1 <= len f ) and
A3: [i,j] in Indices G and
A4: [(i + 1),j] in Indices G and
A5: f /. k = G * ((i + 1),j) and
A6: f /. (k + 1) = G * (i,j) and
A7: (f /. k) `2 = N-bound (L~ f) ; ::_thesis: contradiction
A8: right_cell (f,k,G) = cell (G,i,j) by A1, A2, A3, A4, A5, A6, GOBRD13:26;
A9: j <= width G by A4, MATRIX_1:38;
A10: ( 1 <= i + 1 & 1 <= j ) by A4, MATRIX_1:38;
set p = (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))));
A11: ( 0 + 1 <= i & 1 <= j ) by A3, MATRIX_1:38;
A12: j <= width G by A3, MATRIX_1:38;
A13: i + 1 <= len G by A4, MATRIX_1:38;
percases ( j = width G or j < width G ) by A12, XXREAL_0:1;
suppose j = width G ; ::_thesis: contradiction
hence contradiction by A1, A2, A3, A4, A5, A6, Th13; ::_thesis: verum
end;
supposeA14: j < width G ; ::_thesis: contradiction
i < len G by A13, NAT_1:13;
then A15: Int (cell (G,i,j)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } by A11, A14, GOBOARD6:26;
j + 1 <= width G by A14, NAT_1:13;
then A16: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in Int (right_cell (f,k,G)) by A11, A13, A8, GOBOARD6:31;
then consider r, s being Real such that
A17: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) = |[r,s]| and
(G * (i,1)) `1 < r and
r < (G * ((i + 1),1)) `1 and
A18: (G * (1,j)) `2 < s and
s < (G * (1,(j + 1))) `2 by A8, A15;
((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `2 = s by A17, EUCLID:52;
then ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `2 > N-bound (L~ f) by A5, A7, A13, A10, A9, A18, GOBOARD5:1;
then A19: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in LeftComp f by Th12;
Int (right_cell (f,k,G)) c= RightComp f by A1, A2, JORDAN1H:25;
then (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in (LeftComp f) /\ (RightComp f) by A16, A19, XBOOLE_0:def_4;
then LeftComp f meets RightComp f by XBOOLE_0:def_7;
hence contradiction by GOBRD14:14; ::_thesis: verum
end;
end;
end;
theorem Th18: :: JORDAN1I:18
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
(f /. k) `1 <> E-bound (L~ f)
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
(f /. k) `1 <> E-bound (L~ f)
let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
(f /. k) `1 <> E-bound (L~ f) )
assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
(f /. k) `1 <> E-bound (L~ f)
let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) implies (f /. k) `1 <> E-bound (L~ f) )
assume that
A2: ( 1 <= k & k + 1 <= len f ) and
A3: [i,j] in Indices G and
A4: [i,(j + 1)] in Indices G and
A5: f /. k = G * (i,j) and
A6: f /. (k + 1) = G * (i,(j + 1)) and
A7: (f /. k) `1 = E-bound (L~ f) ; ::_thesis: contradiction
A8: right_cell (f,k,G) = cell (G,i,j) by A1, A2, A3, A4, A5, A6, GOBRD13:22;
A9: j <= width G by A3, MATRIX_1:38;
A10: ( 0 + 1 <= i & 1 <= j ) by A3, MATRIX_1:38;
set p = (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))));
A11: i <= len G by A3, MATRIX_1:38;
A12: j + 1 <= width G by A4, MATRIX_1:38;
percases ( i = len G or i < len G ) by A11, XXREAL_0:1;
suppose i = len G ; ::_thesis: contradiction
hence contradiction by A1, A2, A3, A4, A5, A6, Th14; ::_thesis: verum
end;
supposeA13: i < len G ; ::_thesis: contradiction
j < width G by A12, NAT_1:13;
then A14: Int (cell (G,i,j)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } by A10, A13, GOBOARD6:26;
i + 1 <= len G by A13, NAT_1:13;
then A15: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in Int (right_cell (f,k,G)) by A10, A12, A8, GOBOARD6:31;
then consider r, s being Real such that
A16: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) = |[r,s]| and
A17: (G * (i,1)) `1 < r and
r < (G * ((i + 1),1)) `1 and
(G * (1,j)) `2 < s and
s < (G * (1,(j + 1))) `2 by A8, A14;
((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `1 = r by A16, EUCLID:52;
then ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `1 > E-bound (L~ f) by A5, A7, A11, A10, A9, A17, GOBOARD5:2;
then A18: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in LeftComp f by Th10;
Int (right_cell (f,k,G)) c= RightComp f by A1, A2, JORDAN1H:25;
then (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in (LeftComp f) /\ (RightComp f) by A15, A18, XBOOLE_0:def_4;
then LeftComp f meets RightComp f by XBOOLE_0:def_7;
hence contradiction by GOBRD14:14; ::_thesis: verum
end;
end;
end;
theorem Th19: :: JORDAN1I:19
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds
(f /. k) `2 <> S-bound (L~ f)
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds
(f /. k) `2 <> S-bound (L~ f)
let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds
(f /. k) `2 <> S-bound (L~ f) )
assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds
(f /. k) `2 <> S-bound (L~ f)
let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) implies (f /. k) `2 <> S-bound (L~ f) )
assume that
A2: ( 1 <= k & k + 1 <= len f ) and
A3: [i,j] in Indices G and
A4: [(i + 1),j] in Indices G and
A5: f /. k = G * (i,j) and
A6: f /. (k + 1) = G * ((i + 1),j) and
A7: (f /. k) `2 = S-bound (L~ f) ; ::_thesis: contradiction
A8: right_cell (f,k,G) = cell (G,i,(j -' 1)) by A1, A2, A3, A4, A5, A6, GOBRD13:24;
A9: i <= len G by A3, MATRIX_1:38;
A10: j <= width G by A3, MATRIX_1:38;
A11: i + 1 <= len G by A4, MATRIX_1:38;
set p = (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j)));
A12: 0 + 1 <= i by A3, MATRIX_1:38;
A13: 1 <= j by A3, MATRIX_1:38;
then A14: (j -' 1) + 1 = j by XREAL_1:235;
percases ( j = 1 or j > 1 ) by A13, XXREAL_0:1;
suppose j = 1 ; ::_thesis: contradiction
hence contradiction by A1, A2, A3, A4, A5, A6, Th15; ::_thesis: verum
end;
suppose j > 1 ; ::_thesis: contradiction
then j >= 1 + 1 by NAT_1:13;
then A15: j - 1 >= (1 + 1) - 1 by XREAL_1:9;
j < (width G) + 1 by A10, NAT_1:13;
then A16: j - 1 < ((width G) + 1) - 1 by XREAL_1:9;
i < len G by A11, NAT_1:13;
then A17: Int (cell (G,i,(j -' 1))) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,(j -' 1))) `2 < s & s < (G * (1,j)) `2 ) } by A12, A14, A15, A16, GOBOARD6:26;
A18: (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))) in Int (right_cell (f,k,G)) by A12, A10, A11, A8, A14, A15, GOBOARD6:31;
then consider r, s being Real such that
A19: (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))) = |[r,s]| and
(G * (i,1)) `1 < r and
r < (G * ((i + 1),1)) `1 and
(G * (1,(j -' 1))) `2 < s and
A20: s < (G * (1,j)) `2 by A8, A17;
((1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j)))) `2 = s by A19, EUCLID:52;
then ((1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j)))) `2 < S-bound (L~ f) by A5, A7, A12, A9, A13, A10, A20, GOBOARD5:1;
then A21: (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))) in LeftComp f by Th11;
Int (right_cell (f,k,G)) c= RightComp f by A1, A2, JORDAN1H:25;
then (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))) in (LeftComp f) /\ (RightComp f) by A18, A21, XBOOLE_0:def_4;
then LeftComp f meets RightComp f by XBOOLE_0:def_7;
hence contradiction by GOBRD14:14; ::_thesis: verum
end;
end;
end;
theorem Th20: :: JORDAN1I:20
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
(f /. k) `1 <> W-bound (L~ f)
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
(f /. k) `1 <> W-bound (L~ f)
let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
(f /. k) `1 <> W-bound (L~ f) )
assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
(f /. k) `1 <> W-bound (L~ f)
let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) implies (f /. k) `1 <> W-bound (L~ f) )
assume that
A2: ( 1 <= k & k + 1 <= len f ) and
A3: [i,j] in Indices G and
A4: [i,(j + 1)] in Indices G and
A5: f /. k = G * (i,(j + 1)) and
A6: f /. (k + 1) = G * (i,j) and
A7: (f /. k) `1 = W-bound (L~ f) ; ::_thesis: contradiction
A8: right_cell (f,k,G) = cell (G,(i -' 1),j) by A1, A2, A3, A4, A5, A6, GOBRD13:28;
A9: ( 1 <= i & i <= len G ) by A4, MATRIX_1:38;
A10: 1 <= j by A3, MATRIX_1:38;
A11: 1 <= j + 1 by A4, MATRIX_1:38;
A12: j + 1 <= width G by A4, MATRIX_1:38;
set p = (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))));
A13: i <= len G by A3, MATRIX_1:38;
A14: 0 + 1 <= i by A3, MATRIX_1:38;
then A15: (i -' 1) + 1 = i by XREAL_1:235;
percases ( i = 1 or i > 1 ) by A14, XXREAL_0:1;
suppose i = 1 ; ::_thesis: contradiction
hence contradiction by A1, A2, A3, A4, A5, A6, Th16; ::_thesis: verum
end;
suppose i > 1 ; ::_thesis: contradiction
then i >= 1 + 1 by NAT_1:13;
then A16: i - 1 >= (1 + 1) - 1 by XREAL_1:9;
i < (len G) + 1 by A13, NAT_1:13;
then A17: i - 1 < ((len G) + 1) - 1 by XREAL_1:9;
j < width G by A12, NAT_1:13;
then A18: Int (cell (G,(i -' 1),j)) = { |[r,s]| where r, s is Real : ( (G * ((i -' 1),1)) `1 < r & r < (G * (i,1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } by A10, A15, A16, A17, GOBOARD6:26;
A19: (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in Int (right_cell (f,k,G)) by A13, A10, A12, A8, A15, A16, GOBOARD6:31;
then consider r, s being Real such that
A20: (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) = |[r,s]| and
(G * ((i -' 1),1)) `1 < r and
A21: r < (G * (i,1)) `1 and
(G * (1,j)) `2 < s and
s < (G * (1,(j + 1))) `2 by A8, A18;
((1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))))) `1 = r by A20, EUCLID:52;
then ((1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))))) `1 < W-bound (L~ f) by A5, A7, A9, A11, A12, A21, GOBOARD5:2;
then A22: (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in LeftComp f by Th9;
Int (right_cell (f,k,G)) c= RightComp f by A1, A2, JORDAN1H:25;
then (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in (LeftComp f) /\ (RightComp f) by A19, A22, XBOOLE_0:def_4;
then LeftComp f meets RightComp f by XBOOLE_0:def_7;
hence contradiction by GOBRD14:14; ::_thesis: verum
end;
end;
end;
theorem Th21: :: JORDAN1I:21
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board
for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = W-min (L~ f) holds
ex i, j being Element of NAT st
( [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) )
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board
for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = W-min (L~ f) holds
ex i, j being Element of NAT st
( [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) )
let G be Go-board; ::_thesis: for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = W-min (L~ f) holds
ex i, j being Element of NAT st
( [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) )
let k be Element of NAT ; ::_thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = W-min (L~ f) implies ex i, j being Element of NAT st
( [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) ) )
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k + 1 <= len f and
A4: f /. k = W-min (L~ f) ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) )
consider i1, j1, i2, j2 being Element of NAT such that
A5: [i1,j1] in Indices G and
A6: f /. k = G * (i1,j1) and
A7: [i2,j2] in Indices G and
A8: f /. (k + 1) = G * (i2,j2) and
A9: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A2, A3, JORDAN8:3;
A10: (G * (i1,j1)) `1 = W-bound (L~ f) by A4, A6, EUCLID:52;
A11: 1 <= j2 by A7, MATRIX_1:38;
A12: 1 <= i2 by A7, MATRIX_1:38;
take i1 ; ::_thesis: ex j being Element of NAT st
( [i1,j] in Indices G & [i1,(j + 1)] in Indices G & f /. k = G * (i1,j) & f /. (k + 1) = G * (i1,(j + 1)) )
take j1 ; ::_thesis: ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) )
A13: 1 <= i1 by A5, MATRIX_1:38;
A14: k + 1 >= 1 + 1 by A2, XREAL_1:7;
then A15: len f >= 2 by A3, XXREAL_0:2;
k + 1 >= 1 by NAT_1:11;
then A16: k + 1 in dom f by A3, FINSEQ_3:25;
then f /. (k + 1) in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2;
then A17: (G * (i1,j1)) `1 <= (G * (i2,j2)) `1 by A8, A10, PSCOMP_1:24;
A18: ( i1 <= len G & j1 <= width G ) by A5, MATRIX_1:38;
A19: k < len f by A3, NAT_1:13;
then A20: k in dom f by A2, FINSEQ_3:25;
A21: ( i2 <= len G & j2 <= width G ) by A7, MATRIX_1:38;
A22: 1 <= j1 by A5, MATRIX_1:38;
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 & k <> 1 ) or ( i1 + 1 = i2 & j1 = j2 & k = 1 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A9;
supposeA23: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) )
thus [i1,j1] in Indices G by A5; ::_thesis: ( [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) )
thus [i1,(j1 + 1)] in Indices G by A7, A23; ::_thesis: ( f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) )
thus f /. k = G * (i1,j1) by A6; ::_thesis: f /. (k + 1) = G * (i1,(j1 + 1))
thus f /. (k + 1) = G * (i1,(j1 + 1)) by A8, A23; ::_thesis: verum
end;
supposeA24: ( i1 + 1 = i2 & j1 = j2 & k <> 1 ) ; ::_thesis: ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) )
reconsider k9 = k - 1 as Element of NAT by A20, FINSEQ_3:26;
k > 1 by A2, A24, XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then A25: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Element of NAT such that
A26: [i3,j3] in Indices G and
A27: f /. k9 = G * (i3,j3) and
A28: [i4,j4] in Indices G and
A29: f /. (k9 + 1) = G * (i4,j4) and
A30: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A19, JORDAN8:3;
A31: i1 = i4 by A5, A6, A28, A29, GOBOARD1:5;
k9 + 1 < len f by A3, NAT_1:13;
then k9 < len f by NAT_1:13;
then A32: k9 in dom f by A25, FINSEQ_3:25;
A33: 1 <= i3 by A26, MATRIX_1:38;
A34: j1 = j4 by A5, A6, A28, A29, GOBOARD1:5;
A35: 1 <= j3 by A26, MATRIX_1:38;
A36: ( i3 <= len G & j3 <= width G ) by A26, MATRIX_1:38;
A37: j3 = j4
proof
assume A38: j3 <> j4 ; ::_thesis: contradiction
percases ( ( i3 = i4 & j3 = j4 + 1 ) or ( i3 = i4 & j3 + 1 = j4 ) ) by A30, A38;
supposeA39: ( i3 = i4 & j3 = j4 + 1 ) ; ::_thesis: contradiction
then (G * (i3,j3)) `1 <> W-bound (L~ f) by A1, A19, A25, A26, A27, A28, A29, Th20;
then (G * (i3,1)) `1 <> W-bound (L~ f) by A33, A35, A36, GOBOARD5:2;
then (W-min (L~ f)) `1 <> W-bound (L~ f) by A4, A6, A13, A22, A18, A31, A39, GOBOARD5:2;
hence contradiction by EUCLID:52; ::_thesis: verum
end;
supposeA40: ( i3 = i4 & j3 + 1 = j4 ) ; ::_thesis: contradiction
(G * (i3,j3)) `1 = (G * (i3,1)) `1 by A33, A35, A36, GOBOARD5:2
.= (W-min (L~ f)) `1 by A4, A6, A13, A22, A18, A31, A40, GOBOARD5:2
.= W-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in W-most (L~ f) by A15, A27, A32, GOBOARD1:1, SPRECT_2:12;
then (G * (i4,j4)) `2 <= (G * (i3,j3)) `2 by A4, A29, PSCOMP_1:31;
then j3 >= j3 + 1 by A13, A18, A31, A34, A35, A40, GOBOARD5:4;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
A41: k9 + 1 = k ;
f /. k9 in L~ f by A3, A14, A32, GOBOARD1:1, XXREAL_0:2;
then A42: (G * (i1,j1)) `1 <= (G * (i3,j3)) `1 by A10, A27, PSCOMP_1:24;
now__::_thesis:_contradiction
percases ( i3 + 1 = i4 or i3 = i4 + 1 ) by A30, A37;
suppose i3 + 1 = i4 ; ::_thesis: contradiction
then i3 >= i3 + 1 by A22, A18, A31, A34, A33, A42, A37, GOBOARD5:3;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
supposeA43: i3 = i4 + 1 ; ::_thesis: contradiction
k9 + (1 + 1) <= len f by A3;
then A44: (LSeg (f,k9)) /\ (LSeg (f,k)) = {(f /. k)} by A25, A41, TOPREAL1:def_6;
( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A19, A25, A41, TOPREAL1:21;
then f /. (k + 1) in {(f /. k)} by A8, A24, A27, A31, A34, A37, A43, A44, XBOOLE_0:def_4;
then A45: f /. (k + 1) = f /. k by TARSKI:def_1;
i1 <> i2 by A24;
hence contradiction by A5, A6, A7, A8, A45, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
hence ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) ; ::_thesis: verum
end;
supposeA46: ( i1 + 1 = i2 & j1 = j2 & k = 1 ) ; ::_thesis: ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) )
set k1 = len f;
k < len f by A3, NAT_1:13;
then A47: len f > 1 + 0 by A2, XXREAL_0:2;
then len f in dom f by FINSEQ_3:25;
then reconsider k9 = (len f) - 1 as Element of NAT by FINSEQ_3:26;
k + 1 >= 1 + 1 by A2, XREAL_1:7;
then len f >= 1 + 1 by A3, XXREAL_0:2;
then A48: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Element of NAT such that
A49: [i3,j3] in Indices G and
A50: f /. k9 = G * (i3,j3) and
A51: [i4,j4] in Indices G and
A52: f /. (k9 + 1) = G * (i4,j4) and
A53: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, JORDAN8:3;
A54: f /. (len f) = f /. 1 by FINSEQ_6:def_1;
then A55: i1 = i4 by A5, A6, A46, A51, A52, GOBOARD1:5;
A56: j1 = j4 by A5, A6, A46, A54, A51, A52, GOBOARD1:5;
A57: 1 <= j3 by A49, MATRIX_1:38;
k9 + 1 <= len f ;
then k9 < len f by NAT_1:13;
then A58: k9 in dom f by A48, FINSEQ_3:25;
then f /. k9 in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2;
then A59: (G * (i1,j1)) `1 <= (G * (i3,j3)) `1 by A10, A50, PSCOMP_1:24;
A60: 1 <= i3 by A49, MATRIX_1:38;
A61: ( i3 <= len G & j3 <= width G ) by A49, MATRIX_1:38;
A62: j3 = j4
proof
assume A63: j3 <> j4 ; ::_thesis: contradiction
percases ( ( i3 = i4 & j3 = j4 + 1 ) or ( i3 = i4 & j3 + 1 = j4 ) ) by A53, A63;
supposeA64: ( i3 = i4 & j3 = j4 + 1 ) ; ::_thesis: contradiction
then (G * (i3,j3)) `1 <> W-bound (L~ f) by A1, A48, A49, A50, A51, A52, Th20;
then (G * (i3,1)) `1 <> W-bound (L~ f) by A60, A57, A61, GOBOARD5:2;
then (W-min (L~ f)) `1 <> W-bound (L~ f) by A4, A6, A13, A22, A18, A55, A64, GOBOARD5:2;
hence contradiction by EUCLID:52; ::_thesis: verum
end;
supposeA65: ( i3 = i4 & j3 + 1 = j4 ) ; ::_thesis: contradiction
(G * (i3,j3)) `1 = (G * (i3,1)) `1 by A60, A57, A61, GOBOARD5:2
.= (W-min (L~ f)) `1 by A4, A6, A13, A22, A18, A55, A65, GOBOARD5:2
.= W-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in W-most (L~ f) by A15, A50, A58, GOBOARD1:1, SPRECT_2:12;
then (G * (i4,j4)) `2 <= (G * (i3,j3)) `2 by A4, A46, A54, A52, PSCOMP_1:31;
then j3 >= j3 + 1 by A13, A18, A55, A56, A57, A65, GOBOARD5:4;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
A66: k9 + 1 = len f ;
now__::_thesis:_contradiction
percases ( i3 + 1 = i4 or i3 = i4 + 1 ) by A53, A62;
suppose i3 + 1 = i4 ; ::_thesis: contradiction
then i3 >= i3 + 1 by A22, A18, A55, A56, A60, A59, A62, GOBOARD5:3;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
supposeA67: i3 = i4 + 1 ; ::_thesis: contradiction
(len f) - 1 >= 0 by A47, XREAL_1:19;
then (len f) -' 1 = (len f) - 1 by XREAL_0:def_2;
then A68: (LSeg (f,k)) /\ (LSeg (f,k9)) = {(f . k)} by A46, JORDAN4:42
.= {(f /. k)} by A20, PARTFUN1:def_6 ;
( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A48, A66, TOPREAL1:21;
then f /. (k + 1) in {(f /. k)} by A8, A46, A50, A55, A56, A62, A67, A68, XBOOLE_0:def_4;
then A69: f /. (k + 1) = f /. k by TARSKI:def_1;
i1 <> i2 by A46;
hence contradiction by A5, A6, A7, A8, A69, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
hence ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) ; ::_thesis: verum
end;
suppose ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) )
then i2 >= i2 + 1 by A22, A18, A12, A17, GOBOARD5:3;
hence ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) by NAT_1:13; ::_thesis: verum
end;
supposeA70: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) )
(G * (i2,j2)) `1 = (G * (i2,1)) `1 by A12, A11, A21, GOBOARD5:2
.= W-bound (L~ f) by A13, A22, A18, A10, A70, GOBOARD5:2 ;
then G * (i2,j2) in W-most (L~ f) by A8, A15, A16, GOBOARD1:1, SPRECT_2:12;
then (G * (i1,j1)) `2 <= (G * (i2,j2)) `2 by A4, A6, PSCOMP_1:31;
then j2 >= j2 + 1 by A13, A18, A11, A70, GOBOARD5:4;
hence ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) by NAT_1:13; ::_thesis: verum
end;
end;
end;
theorem :: JORDAN1I:22
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board
for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) holds
ex i, j being Element of NAT st
( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) )
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board
for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) holds
ex i, j being Element of NAT st
( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) )
let G be Go-board; ::_thesis: for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) holds
ex i, j being Element of NAT st
( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) )
let k be Element of NAT ; ::_thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) implies ex i, j being Element of NAT st
( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) ) )
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k + 1 <= len f and
A4: f /. k = N-min (L~ f) ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) )
consider i1, j1, i2, j2 being Element of NAT such that
A5: [i1,j1] in Indices G and
A6: f /. k = G * (i1,j1) and
A7: [i2,j2] in Indices G and
A8: f /. (k + 1) = G * (i2,j2) and
A9: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A2, A3, JORDAN8:3;
A10: (G * (i1,j1)) `2 = N-bound (L~ f) by A4, A6, EUCLID:52;
A11: j2 <= width G by A7, MATRIX_1:38;
A12: 1 <= i2 by A7, MATRIX_1:38;
take i1 ; ::_thesis: ex j being Element of NAT st
( [i1,j] in Indices G & [(i1 + 1),j] in Indices G & f /. k = G * (i1,j) & f /. (k + 1) = G * ((i1 + 1),j) )
take j1 ; ::_thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) )
A13: 1 <= i1 by A5, MATRIX_1:38;
A14: k + 1 >= 1 + 1 by A2, XREAL_1:7;
then A15: len f >= 2 by A3, XXREAL_0:2;
k + 1 >= 1 by NAT_1:11;
then A16: k + 1 in dom f by A3, FINSEQ_3:25;
then f /. (k + 1) in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2;
then A17: (G * (i1,j1)) `2 >= (G * (i2,j2)) `2 by A8, A10, PSCOMP_1:24;
A18: j1 <= width G by A5, MATRIX_1:38;
A19: k < len f by A3, NAT_1:13;
then A20: k in dom f by A2, FINSEQ_3:25;
A21: ( i2 <= len G & 1 <= j2 ) by A7, MATRIX_1:38;
A22: ( i1 <= len G & 1 <= j1 ) by A5, MATRIX_1:38;
percases ( ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 & j2 + 1 = j1 & k <> 1 ) or ( i1 = i2 & j2 + 1 = j1 & k = 1 ) or ( i1 = i2 & j2 = j1 + 1 ) or ( i1 = i2 + 1 & j1 = j2 ) ) by A9;
supposeA23: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) )
thus [i1,j1] in Indices G by A5; ::_thesis: ( [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) )
thus [(i1 + 1),j1] in Indices G by A7, A23; ::_thesis: ( f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) )
thus f /. k = G * (i1,j1) by A6; ::_thesis: f /. (k + 1) = G * ((i1 + 1),j1)
thus f /. (k + 1) = G * ((i1 + 1),j1) by A8, A23; ::_thesis: verum
end;
supposeA24: ( i1 = i2 & j2 + 1 = j1 & k <> 1 ) ; ::_thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) )
reconsider k9 = k - 1 as Element of NAT by A20, FINSEQ_3:26;
k > 1 by A2, A24, XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then A25: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Element of NAT such that
A26: [i3,j3] in Indices G and
A27: f /. k9 = G * (i3,j3) and
A28: [i4,j4] in Indices G and
A29: f /. (k9 + 1) = G * (i4,j4) and
A30: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A19, JORDAN8:3;
A31: i1 = i4 by A5, A6, A28, A29, GOBOARD1:5;
k9 + 1 < len f by A3, NAT_1:13;
then k9 < len f by NAT_1:13;
then A32: k9 in dom f by A25, FINSEQ_3:25;
A33: 1 <= i3 by A26, MATRIX_1:38;
A34: j3 <= width G by A26, MATRIX_1:38;
A35: j1 = j4 by A5, A6, A28, A29, GOBOARD1:5;
A36: ( i3 <= len G & 1 <= j3 ) by A26, MATRIX_1:38;
A37: i3 = i4
proof
assume A38: i3 <> i4 ; ::_thesis: contradiction
percases ( ( j3 = j4 & i3 = i4 + 1 ) or ( j3 = j4 & i3 + 1 = i4 ) ) by A30, A38;
supposeA39: ( j3 = j4 & i3 = i4 + 1 ) ; ::_thesis: contradiction
then (G * (i3,j3)) `2 <> N-bound (L~ f) by A1, A19, A25, A26, A27, A28, A29, Th17;
then (G * (1,j3)) `2 <> N-bound (L~ f) by A33, A36, A34, GOBOARD5:1;
then (N-min (L~ f)) `2 <> N-bound (L~ f) by A4, A6, A13, A22, A18, A35, A39, GOBOARD5:1;
hence contradiction by EUCLID:52; ::_thesis: verum
end;
supposeA40: ( j3 = j4 & i3 + 1 = i4 ) ; ::_thesis: contradiction
(G * (i3,j3)) `2 = (G * (1,j3)) `2 by A33, A36, A34, GOBOARD5:1
.= (N-min (L~ f)) `2 by A4, A6, A13, A22, A18, A35, A40, GOBOARD5:1
.= N-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in N-most (L~ f) by A15, A27, A32, GOBOARD1:1, SPRECT_2:10;
then (G * (i4,j4)) `1 <= (G * (i3,j3)) `1 by A4, A29, PSCOMP_1:39;
then i3 >= i3 + 1 by A22, A18, A31, A35, A33, A40, GOBOARD5:3;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
A41: k9 + 1 = k ;
f /. k9 in L~ f by A3, A14, A32, GOBOARD1:1, XXREAL_0:2;
then A42: (G * (i1,j1)) `2 >= (G * (i3,j3)) `2 by A10, A27, PSCOMP_1:24;
now__::_thesis:_contradiction
percases ( j4 + 1 = j3 or j4 = j3 + 1 ) by A30, A37;
suppose j4 + 1 = j3 ; ::_thesis: contradiction
then j4 >= j4 + 1 by A13, A22, A31, A35, A34, A42, A37, GOBOARD5:4;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
supposeA43: j4 = j3 + 1 ; ::_thesis: contradiction
k9 + (1 + 1) <= len f by A3;
then A44: (LSeg (f,k9)) /\ (LSeg (f,k)) = {(f /. k)} by A25, A41, TOPREAL1:def_6;
( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A19, A25, A41, TOPREAL1:21;
then f /. (k + 1) in {(f /. k)} by A8, A24, A27, A31, A35, A37, A43, A44, XBOOLE_0:def_4;
then A45: f /. (k + 1) = f /. k by TARSKI:def_1;
j1 <> j2 by A24;
hence contradiction by A5, A6, A7, A8, A45, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
hence ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) ; ::_thesis: verum
end;
supposeA46: ( i1 = i2 & j2 + 1 = j1 & k = 1 ) ; ::_thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) )
set k1 = len f;
k < len f by A3, NAT_1:13;
then A47: len f > 1 + 0 by A2, XXREAL_0:2;
then len f in dom f by FINSEQ_3:25;
then reconsider k9 = (len f) - 1 as Element of NAT by FINSEQ_3:26;
k + 1 >= 1 + 1 by A2, XREAL_1:7;
then len f >= 1 + 1 by A3, XXREAL_0:2;
then A48: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Element of NAT such that
A49: [i3,j3] in Indices G and
A50: f /. k9 = G * (i3,j3) and
A51: [i4,j4] in Indices G and
A52: f /. (k9 + 1) = G * (i4,j4) and
A53: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, JORDAN8:3;
A54: f /. (len f) = f /. 1 by FINSEQ_6:def_1;
then A55: i1 = i4 by A5, A6, A46, A51, A52, GOBOARD1:5;
k9 + 1 <= len f ;
then k9 < len f by NAT_1:13;
then A56: k9 in dom f by A48, FINSEQ_3:25;
then f /. k9 in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2;
then A57: (G * (i1,j1)) `2 >= (G * (i3,j3)) `2 by A10, A50, PSCOMP_1:24;
A58: 1 <= i3 by A49, MATRIX_1:38;
A59: j1 = j4 by A5, A6, A46, A54, A51, A52, GOBOARD1:5;
A60: j3 <= width G by A49, MATRIX_1:38;
A61: ( i3 <= len G & 1 <= j3 ) by A49, MATRIX_1:38;
A62: i3 = i4
proof
assume A63: i3 <> i4 ; ::_thesis: contradiction
percases ( ( j3 = j4 & i3 = i4 + 1 ) or ( j3 = j4 & i3 + 1 = i4 ) ) by A53, A63;
supposeA64: ( j3 = j4 & i3 = i4 + 1 ) ; ::_thesis: contradiction
then (G * (i3,j3)) `2 <> N-bound (L~ f) by A1, A48, A49, A50, A51, A52, Th17;
then (G * (1,j3)) `2 <> N-bound (L~ f) by A58, A61, A60, GOBOARD5:1;
then (N-min (L~ f)) `2 <> N-bound (L~ f) by A4, A6, A13, A22, A18, A59, A64, GOBOARD5:1;
hence contradiction by EUCLID:52; ::_thesis: verum
end;
supposeA65: ( j3 = j4 & i3 + 1 = i4 ) ; ::_thesis: contradiction
(G * (i3,j3)) `2 = (G * (1,j3)) `2 by A58, A61, A60, GOBOARD5:1
.= (N-min (L~ f)) `2 by A4, A6, A13, A22, A18, A59, A65, GOBOARD5:1
.= N-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in N-most (L~ f) by A15, A50, A56, GOBOARD1:1, SPRECT_2:10;
then (G * (i4,j4)) `1 <= (G * (i3,j3)) `1 by A4, A46, A54, A52, PSCOMP_1:39;
then i3 >= i3 + 1 by A22, A18, A55, A59, A58, A65, GOBOARD5:3;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
A66: k9 + 1 = len f ;
now__::_thesis:_contradiction
percases ( j4 + 1 = j3 or j4 = j3 + 1 ) by A53, A62;
suppose j4 + 1 = j3 ; ::_thesis: contradiction
then j4 >= j4 + 1 by A13, A22, A55, A59, A60, A57, A62, GOBOARD5:4;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
supposeA67: j4 = j3 + 1 ; ::_thesis: contradiction
(len f) - 1 >= 0 by A47, XREAL_1:19;
then (len f) -' 1 = (len f) - 1 by XREAL_0:def_2;
then A68: (LSeg (f,k)) /\ (LSeg (f,k9)) = {(f . k)} by A46, JORDAN4:42
.= {(f /. k)} by A20, PARTFUN1:def_6 ;
( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A48, A66, TOPREAL1:21;
then f /. (k + 1) in {(f /. k)} by A8, A46, A50, A55, A59, A62, A67, A68, XBOOLE_0:def_4;
then A69: f /. (k + 1) = f /. k by TARSKI:def_1;
j1 <> j2 by A46;
hence contradiction by A5, A6, A7, A8, A69, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
hence ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) ; ::_thesis: verum
end;
suppose ( i1 = i2 & j2 = j1 + 1 ) ; ::_thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) )
then j1 >= j1 + 1 by A13, A22, A11, A17, GOBOARD5:4;
hence ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) by NAT_1:13; ::_thesis: verum
end;
supposeA70: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) )
(G * (i2,j2)) `2 = (G * (1,j2)) `2 by A12, A21, A11, GOBOARD5:1
.= N-bound (L~ f) by A13, A22, A18, A10, A70, GOBOARD5:1 ;
then G * (i2,j2) in N-most (L~ f) by A8, A15, A16, GOBOARD1:1, SPRECT_2:10;
then (G * (i1,j1)) `1 <= (G * (i2,j2)) `1 by A4, A6, PSCOMP_1:39;
then i2 >= i2 + 1 by A22, A18, A12, A70, GOBOARD5:3;
hence ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) by NAT_1:13; ::_thesis: verum
end;
end;
end;
theorem Th23: :: JORDAN1I:23
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board
for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) holds
ex i, j being Element of NAT st
( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) )
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board
for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) holds
ex i, j being Element of NAT st
( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) )
let G be Go-board; ::_thesis: for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) holds
ex i, j being Element of NAT st
( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) )
let k be Element of NAT ; ::_thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) implies ex i, j being Element of NAT st
( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) ) )
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k + 1 <= len f and
A4: f /. k = E-max (L~ f) ; ::_thesis: ex i, j being Element of NAT st
( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) )
consider i1, j1, i2, j2 being Element of NAT such that
A5: [i1,j1] in Indices G and
A6: f /. k = G * (i1,j1) and
A7: [i2,j2] in Indices G and
A8: f /. (k + 1) = G * (i2,j2) and
A9: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A2, A3, JORDAN8:3;
A10: (G * (i1,j1)) `1 = E-bound (L~ f) by A4, A6, EUCLID:52;
A11: j2 <= width G by A7, MATRIX_1:38;
take i2 ; ::_thesis: ex j being Element of NAT st
( [i2,(j + 1)] in Indices G & [i2,j] in Indices G & f /. k = G * (i2,(j + 1)) & f /. (k + 1) = G * (i2,j) )
take j2 ; ::_thesis: ( [i2,(j2 + 1)] in Indices G & [i2,j2] in Indices G & f /. k = G * (i2,(j2 + 1)) & f /. (k + 1) = G * (i2,j2) )
A12: i1 <= len G by A5, MATRIX_1:38;
A13: k + 1 >= 1 + 1 by A2, XREAL_1:7;
then A14: len f >= 2 by A3, XXREAL_0:2;
k + 1 >= 1 by NAT_1:11;
then A15: k + 1 in dom f by A3, FINSEQ_3:25;
then f /. (k + 1) in L~ f by A3, A13, GOBOARD1:1, XXREAL_0:2;
then A16: (G * (i1,j1)) `1 >= (G * (i2,j2)) `1 by A8, A10, PSCOMP_1:24;
A17: ( 1 <= i1 & 1 <= j1 ) by A5, MATRIX_1:38;
A18: k < len f by A3, NAT_1:13;
then A19: k in dom f by A2, FINSEQ_3:25;
A20: i2 <= len G by A7, MATRIX_1:38;
A21: j1 <= width G by A5, MATRIX_1:38;
A22: ( 1 <= i2 & 1 <= j2 ) by A7, MATRIX_1:38;
now__::_thesis:_(_[i2,j2]_in_Indices_G_&_[i2,(j2_+_1)]_in_Indices_G_&_f_/._k_=_G_*_(i2,(j2_+_1))_)
percases ( ( i1 = i2 & j2 + 1 = j1 ) or ( i2 + 1 = i1 & j2 = j1 & k <> 1 ) or ( i2 + 1 = i1 & j2 = j1 & k = 1 ) or ( i2 = i1 + 1 & j1 = j2 ) or ( i1 = i2 & j2 = j1 + 1 ) ) by A9;
suppose ( i1 = i2 & j2 + 1 = j1 ) ; ::_thesis: ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) )
hence ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) by A5, A6, A7; ::_thesis: verum
end;
supposeA23: ( i2 + 1 = i1 & j2 = j1 & k <> 1 ) ; ::_thesis: ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) )
reconsider k9 = k - 1 as Element of NAT by A19, FINSEQ_3:26;
k > 1 by A2, A23, XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then A24: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Element of NAT such that
A25: [i3,j3] in Indices G and
A26: f /. k9 = G * (i3,j3) and
A27: [i4,j4] in Indices G and
A28: f /. (k9 + 1) = G * (i4,j4) and
A29: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A18, JORDAN8:3;
A30: i1 = i4 by A5, A6, A27, A28, GOBOARD1:5;
k9 + 1 < len f by A3, NAT_1:13;
then k9 < len f by NAT_1:13;
then A31: k9 in dom f by A24, FINSEQ_3:25;
A32: i3 <= len G by A25, MATRIX_1:38;
A33: j1 = j4 by A5, A6, A27, A28, GOBOARD1:5;
A34: j3 <= width G by A25, MATRIX_1:38;
A35: ( 1 <= i3 & 1 <= j3 ) by A25, MATRIX_1:38;
A36: j3 = j4
proof
assume A37: j3 <> j4 ; ::_thesis: contradiction
percases ( ( i3 = i4 & j4 = j3 + 1 ) or ( i3 = i4 & j4 + 1 = j3 ) ) by A29, A37;
supposeA38: ( i3 = i4 & j4 = j3 + 1 ) ; ::_thesis: contradiction
then (G * (i3,j3)) `1 <> E-bound (L~ f) by A1, A18, A24, A25, A26, A27, A28, Th18;
then (G * (i3,1)) `1 <> E-bound (L~ f) by A32, A35, A34, GOBOARD5:2;
then (E-max (L~ f)) `1 <> E-bound (L~ f) by A4, A6, A12, A17, A21, A30, A38, GOBOARD5:2;
hence contradiction by EUCLID:52; ::_thesis: verum
end;
supposeA39: ( i3 = i4 & j4 + 1 = j3 ) ; ::_thesis: contradiction
(G * (i3,j3)) `1 = (G * (i3,1)) `1 by A32, A35, A34, GOBOARD5:2
.= (E-max (L~ f)) `1 by A4, A6, A12, A17, A21, A30, A39, GOBOARD5:2
.= E-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in E-most (L~ f) by A14, A26, A31, GOBOARD1:1, SPRECT_2:13;
then (G * (i4,j4)) `2 >= (G * (i3,j3)) `2 by A4, A28, PSCOMP_1:47;
then j4 >= j4 + 1 by A12, A17, A30, A33, A34, A39, GOBOARD5:4;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
A40: k9 + 1 = k ;
f /. k9 in L~ f by A3, A13, A31, GOBOARD1:1, XXREAL_0:2;
then A41: (G * (i1,j1)) `1 >= (G * (i3,j3)) `1 by A10, A26, PSCOMP_1:24;
now__::_thesis:_contradiction
percases ( i4 + 1 = i3 or i4 = i3 + 1 ) by A29, A36;
suppose i4 + 1 = i3 ; ::_thesis: contradiction
then i4 >= i4 + 1 by A17, A21, A30, A33, A32, A41, A36, GOBOARD5:3;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
supposeA42: i4 = i3 + 1 ; ::_thesis: contradiction
k9 + (1 + 1) <= len f by A3;
then A43: (LSeg (f,k9)) /\ (LSeg (f,k)) = {(f /. k)} by A24, A40, TOPREAL1:def_6;
( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A18, A24, A40, TOPREAL1:21;
then f /. (k + 1) in {(f /. k)} by A8, A23, A26, A30, A33, A36, A42, A43, XBOOLE_0:def_4;
then A44: f /. (k + 1) = f /. k by TARSKI:def_1;
i1 <> i2 by A23;
hence contradiction by A5, A6, A7, A8, A44, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
hence ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) ; ::_thesis: verum
end;
supposeA45: ( i2 + 1 = i1 & j2 = j1 & k = 1 ) ; ::_thesis: ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) )
set k1 = len f;
k < len f by A3, NAT_1:13;
then A46: len f > 1 + 0 by A2, XXREAL_0:2;
then len f in dom f by FINSEQ_3:25;
then reconsider k9 = (len f) - 1 as Element of NAT by FINSEQ_3:26;
k + 1 >= 1 + 1 by A2, XREAL_1:7;
then len f >= 1 + 1 by A3, XXREAL_0:2;
then A47: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Element of NAT such that
A48: [i3,j3] in Indices G and
A49: f /. k9 = G * (i3,j3) and
A50: [i4,j4] in Indices G and
A51: f /. (k9 + 1) = G * (i4,j4) and
A52: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, JORDAN8:3;
A53: f /. (len f) = f /. 1 by FINSEQ_6:def_1;
then A54: i1 = i4 by A5, A6, A45, A50, A51, GOBOARD1:5;
A55: j1 = j4 by A5, A6, A45, A53, A50, A51, GOBOARD1:5;
A56: j3 <= width G by A48, MATRIX_1:38;
k9 + 1 <= len f ;
then k9 < len f by NAT_1:13;
then A57: k9 in dom f by A47, FINSEQ_3:25;
then f /. k9 in L~ f by A3, A13, GOBOARD1:1, XXREAL_0:2;
then A58: (G * (i1,j1)) `1 >= (G * (i3,j3)) `1 by A10, A49, PSCOMP_1:24;
A59: i3 <= len G by A48, MATRIX_1:38;
A60: ( 1 <= i3 & 1 <= j3 ) by A48, MATRIX_1:38;
A61: j3 = j4
proof
assume A62: j3 <> j4 ; ::_thesis: contradiction
percases ( ( i3 = i4 & j4 = j3 + 1 ) or ( i3 = i4 & j4 + 1 = j3 ) ) by A52, A62;
supposeA63: ( i3 = i4 & j4 = j3 + 1 ) ; ::_thesis: contradiction
then (G * (i3,j3)) `1 <> E-bound (L~ f) by A1, A47, A48, A49, A50, A51, Th18;
then (G * (i3,1)) `1 <> E-bound (L~ f) by A59, A60, A56, GOBOARD5:2;
then (E-max (L~ f)) `1 <> E-bound (L~ f) by A4, A6, A12, A17, A21, A54, A63, GOBOARD5:2;
hence contradiction by EUCLID:52; ::_thesis: verum
end;
supposeA64: ( i3 = i4 & j4 + 1 = j3 ) ; ::_thesis: contradiction
(G * (i3,j3)) `1 = (G * (i3,1)) `1 by A59, A60, A56, GOBOARD5:2
.= (E-max (L~ f)) `1 by A4, A6, A12, A17, A21, A54, A64, GOBOARD5:2
.= E-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in E-most (L~ f) by A14, A49, A57, GOBOARD1:1, SPRECT_2:13;
then (G * (i4,j4)) `2 >= (G * (i3,j3)) `2 by A4, A45, A53, A51, PSCOMP_1:47;
then j4 >= j4 + 1 by A12, A17, A54, A55, A56, A64, GOBOARD5:4;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
A65: k9 + 1 = len f ;
now__::_thesis:_contradiction
percases ( i4 + 1 = i3 or i4 = i3 + 1 ) by A52, A61;
suppose i4 + 1 = i3 ; ::_thesis: contradiction
then i4 >= i4 + 1 by A17, A21, A54, A55, A59, A58, A61, GOBOARD5:3;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
supposeA66: i4 = i3 + 1 ; ::_thesis: contradiction
(len f) - 1 >= 0 by A46, XREAL_1:19;
then (len f) -' 1 = (len f) - 1 by XREAL_0:def_2;
then A67: (LSeg (f,k)) /\ (LSeg (f,k9)) = {(f . k)} by A45, JORDAN4:42
.= {(f /. k)} by A19, PARTFUN1:def_6 ;
( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A47, A65, TOPREAL1:21;
then f /. (k + 1) in {(f /. k)} by A8, A45, A49, A54, A55, A61, A66, A67, XBOOLE_0:def_4;
then A68: f /. (k + 1) = f /. k by TARSKI:def_1;
i1 <> i2 by A45;
hence contradiction by A5, A6, A7, A8, A68, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
hence ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) ; ::_thesis: verum
end;
suppose ( i2 = i1 + 1 & j1 = j2 ) ; ::_thesis: ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) )
then i1 >= i1 + 1 by A17, A21, A20, A16, GOBOARD5:3;
hence ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) by NAT_1:13; ::_thesis: verum
end;
supposeA69: ( i1 = i2 & j2 = j1 + 1 ) ; ::_thesis: ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) )
(G * (i2,j2)) `1 = (G * (i2,1)) `1 by A20, A22, A11, GOBOARD5:2
.= E-bound (L~ f) by A12, A17, A21, A10, A69, GOBOARD5:2 ;
then G * (i2,j2) in E-most (L~ f) by A8, A14, A15, GOBOARD1:1, SPRECT_2:13;
then (G * (i1,j1)) `2 >= (G * (i2,j2)) `2 by A4, A6, PSCOMP_1:47;
then j1 >= j1 + 1 by A12, A17, A11, A69, GOBOARD5:4;
hence ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) by NAT_1:13; ::_thesis: verum
end;
end;
end;
hence ( [i2,(j2 + 1)] in Indices G & [i2,j2] in Indices G & f /. k = G * (i2,(j2 + 1)) ) ; ::_thesis: f /. (k + 1) = G * (i2,j2)
thus f /. (k + 1) = G * (i2,j2) by A8; ::_thesis: verum
end;
theorem Th24: :: JORDAN1I:24
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board
for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) holds
ex i, j being Element of NAT st
( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) )
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board
for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) holds
ex i, j being Element of NAT st
( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) )
let G be Go-board; ::_thesis: for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) holds
ex i, j being Element of NAT st
( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) )
let k be Element of NAT ; ::_thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) implies ex i, j being Element of NAT st
( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) ) )
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k + 1 <= len f and
A4: f /. k = S-max (L~ f) ; ::_thesis: ex i, j being Element of NAT st
( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) )
consider i1, j1, i2, j2 being Element of NAT such that
A5: [i1,j1] in Indices G and
A6: f /. k = G * (i1,j1) and
A7: [i2,j2] in Indices G and
A8: f /. (k + 1) = G * (i2,j2) and
A9: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A2, A3, JORDAN8:3;
A10: (G * (i1,j1)) `2 = S-bound (L~ f) by A4, A6, EUCLID:52;
A11: 1 <= j2 by A7, MATRIX_1:38;
take i2 ; ::_thesis: ex j being Element of NAT st
( [(i2 + 1),j] in Indices G & [i2,j] in Indices G & f /. k = G * ((i2 + 1),j) & f /. (k + 1) = G * (i2,j) )
take j2 ; ::_thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) & f /. (k + 1) = G * (i2,j2) )
A12: i1 <= len G by A5, MATRIX_1:38;
A13: k + 1 >= 1 + 1 by A2, XREAL_1:7;
then A14: len f >= 2 by A3, XXREAL_0:2;
k + 1 >= 1 by NAT_1:11;
then A15: k + 1 in dom f by A3, FINSEQ_3:25;
then f /. (k + 1) in L~ f by A3, A13, GOBOARD1:1, XXREAL_0:2;
then A16: (G * (i1,j1)) `2 <= (G * (i2,j2)) `2 by A8, A10, PSCOMP_1:24;
A17: 1 <= j1 by A5, MATRIX_1:38;
A18: k < len f by A3, NAT_1:13;
then A19: k in dom f by A2, FINSEQ_3:25;
A20: i2 <= len G by A7, MATRIX_1:38;
A21: ( 1 <= i1 & j1 <= width G ) by A5, MATRIX_1:38;
A22: ( 1 <= i2 & j2 <= width G ) by A7, MATRIX_1:38;
now__::_thesis:_(_[(i2_+_1),j2]_in_Indices_G_&_[i2,j2]_in_Indices_G_&_f_/._k_=_G_*_((i2_+_1),j2)_)
percases ( ( i2 + 1 = i1 & j1 = j2 ) or ( i1 = i2 & j1 + 1 = j2 & k <> 1 ) or ( i1 = i2 & j1 + 1 = j2 & k = 1 ) or ( i1 = i2 & j1 = j2 + 1 ) or ( i2 = i1 + 1 & j1 = j2 ) ) by A9;
suppose ( i2 + 1 = i1 & j1 = j2 ) ; ::_thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) )
hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) by A5, A6, A7; ::_thesis: verum
end;
supposeA23: ( i1 = i2 & j1 + 1 = j2 & k <> 1 ) ; ::_thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) )
reconsider k9 = k - 1 as Element of NAT by A19, FINSEQ_3:26;
k > 1 by A2, A23, XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then A24: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Element of NAT such that
A25: [i3,j3] in Indices G and
A26: f /. k9 = G * (i3,j3) and
A27: [i4,j4] in Indices G and
A28: f /. (k9 + 1) = G * (i4,j4) and
A29: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A18, JORDAN8:3;
A30: i1 = i4 by A5, A6, A27, A28, GOBOARD1:5;
k9 + 1 < len f by A3, NAT_1:13;
then k9 < len f by NAT_1:13;
then A31: k9 in dom f by A24, FINSEQ_3:25;
A32: i3 <= len G by A25, MATRIX_1:38;
A33: 1 <= j3 by A25, MATRIX_1:38;
A34: j1 = j4 by A5, A6, A27, A28, GOBOARD1:5;
A35: ( 1 <= i3 & j3 <= width G ) by A25, MATRIX_1:38;
A36: i3 = i4
proof
assume A37: i3 <> i4 ; ::_thesis: contradiction
percases ( ( j3 = j4 & i4 = i3 + 1 ) or ( j3 = j4 & i4 + 1 = i3 ) ) by A29, A37;
supposeA38: ( j3 = j4 & i4 = i3 + 1 ) ; ::_thesis: contradiction
then (G * (i3,j3)) `2 <> S-bound (L~ f) by A1, A18, A24, A25, A26, A27, A28, Th19;
then (G * (1,j3)) `2 <> S-bound (L~ f) by A32, A33, A35, GOBOARD5:1;
then (S-max (L~ f)) `2 <> S-bound (L~ f) by A4, A6, A12, A17, A21, A34, A38, GOBOARD5:1;
hence contradiction by EUCLID:52; ::_thesis: verum
end;
supposeA39: ( j3 = j4 & i4 + 1 = i3 ) ; ::_thesis: contradiction
(G * (i3,j3)) `2 = (G * (1,j3)) `2 by A32, A33, A35, GOBOARD5:1
.= (S-max (L~ f)) `2 by A4, A6, A12, A17, A21, A34, A39, GOBOARD5:1
.= S-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in S-most (L~ f) by A14, A26, A31, GOBOARD1:1, SPRECT_2:11;
then (G * (i4,j4)) `1 >= (G * (i3,j3)) `1 by A4, A28, PSCOMP_1:55;
then i4 >= i4 + 1 by A17, A21, A30, A34, A32, A39, GOBOARD5:3;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
A40: k9 + 1 = k ;
f /. k9 in L~ f by A3, A13, A31, GOBOARD1:1, XXREAL_0:2;
then A41: (G * (i1,j1)) `2 <= (G * (i3,j3)) `2 by A10, A26, PSCOMP_1:24;
now__::_thesis:_contradiction
percases ( j3 + 1 = j4 or j3 = j4 + 1 ) by A29, A36;
suppose j3 + 1 = j4 ; ::_thesis: contradiction
then j3 >= j3 + 1 by A12, A21, A30, A34, A33, A41, A36, GOBOARD5:4;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
supposeA42: j3 = j4 + 1 ; ::_thesis: contradiction
k9 + (1 + 1) <= len f by A3;
then A43: (LSeg (f,k9)) /\ (LSeg (f,k)) = {(f /. k)} by A24, A40, TOPREAL1:def_6;
( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A18, A24, A40, TOPREAL1:21;
then f /. (k + 1) in {(f /. k)} by A8, A23, A26, A30, A34, A36, A42, A43, XBOOLE_0:def_4;
then A44: f /. (k + 1) = f /. k by TARSKI:def_1;
j1 <> j2 by A23;
hence contradiction by A5, A6, A7, A8, A44, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) ; ::_thesis: verum
end;
supposeA45: ( i1 = i2 & j1 + 1 = j2 & k = 1 ) ; ::_thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) )
set k1 = len f;
k < len f by A3, NAT_1:13;
then A46: len f > 1 + 0 by A2, XXREAL_0:2;
then len f in dom f by FINSEQ_3:25;
then reconsider k9 = (len f) - 1 as Element of NAT by FINSEQ_3:26;
k + 1 >= 1 + 1 by A2, XREAL_1:7;
then len f >= 1 + 1 by A3, XXREAL_0:2;
then A47: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Element of NAT such that
A48: [i3,j3] in Indices G and
A49: f /. k9 = G * (i3,j3) and
A50: [i4,j4] in Indices G and
A51: f /. (k9 + 1) = G * (i4,j4) and
A52: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, JORDAN8:3;
A53: f /. (len f) = f /. 1 by FINSEQ_6:def_1;
then A54: i1 = i4 by A5, A6, A45, A50, A51, GOBOARD1:5;
k9 + 1 <= len f ;
then k9 < len f by NAT_1:13;
then A55: k9 in dom f by A47, FINSEQ_3:25;
then f /. k9 in L~ f by A3, A13, GOBOARD1:1, XXREAL_0:2;
then A56: (G * (i1,j1)) `2 <= (G * (i3,j3)) `2 by A10, A49, PSCOMP_1:24;
A57: i3 <= len G by A48, MATRIX_1:38;
A58: j1 = j4 by A5, A6, A45, A53, A50, A51, GOBOARD1:5;
A59: 1 <= j3 by A48, MATRIX_1:38;
A60: ( 1 <= i3 & j3 <= width G ) by A48, MATRIX_1:38;
A61: i3 = i4
proof
assume A62: i3 <> i4 ; ::_thesis: contradiction
percases ( ( j3 = j4 & i4 = i3 + 1 ) or ( j3 = j4 & i4 + 1 = i3 ) ) by A52, A62;
supposeA63: ( j3 = j4 & i4 = i3 + 1 ) ; ::_thesis: contradiction
then (G * (i3,j3)) `2 <> S-bound (L~ f) by A1, A47, A48, A49, A50, A51, Th19;
then (G * (1,j3)) `2 <> S-bound (L~ f) by A57, A59, A60, GOBOARD5:1;
then (S-max (L~ f)) `2 <> S-bound (L~ f) by A4, A6, A12, A17, A21, A58, A63, GOBOARD5:1;
hence contradiction by EUCLID:52; ::_thesis: verum
end;
supposeA64: ( j3 = j4 & i4 + 1 = i3 ) ; ::_thesis: contradiction
(G * (i3,j3)) `2 = (G * (1,j3)) `2 by A57, A59, A60, GOBOARD5:1
.= (S-max (L~ f)) `2 by A4, A6, A12, A17, A21, A58, A64, GOBOARD5:1
.= S-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in S-most (L~ f) by A14, A49, A55, GOBOARD1:1, SPRECT_2:11;
then (G * (i4,j4)) `1 >= (G * (i3,j3)) `1 by A4, A45, A53, A51, PSCOMP_1:55;
then i4 >= i4 + 1 by A17, A21, A54, A58, A57, A64, GOBOARD5:3;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
A65: k9 + 1 = len f ;
now__::_thesis:_contradiction
percases ( j3 + 1 = j4 or j3 = j4 + 1 ) by A52, A61;
suppose j3 + 1 = j4 ; ::_thesis: contradiction
then j3 >= j3 + 1 by A12, A21, A54, A58, A59, A56, A61, GOBOARD5:4;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
supposeA66: j3 = j4 + 1 ; ::_thesis: contradiction
(len f) - 1 >= 0 by A46, XREAL_1:19;
then (len f) -' 1 = (len f) - 1 by XREAL_0:def_2;
then A67: (LSeg (f,k)) /\ (LSeg (f,k9)) = {(f . k)} by A45, JORDAN4:42
.= {(f /. k)} by A19, PARTFUN1:def_6 ;
( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A47, A65, TOPREAL1:21;
then f /. (k + 1) in {(f /. k)} by A8, A45, A49, A54, A58, A61, A66, A67, XBOOLE_0:def_4;
then A68: f /. (k + 1) = f /. k by TARSKI:def_1;
j1 <> j2 by A45;
hence contradiction by A5, A6, A7, A8, A68, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) ; ::_thesis: verum
end;
suppose ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) )
then j2 >= j2 + 1 by A12, A21, A11, A16, GOBOARD5:4;
hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) by NAT_1:13; ::_thesis: verum
end;
supposeA69: ( i2 = i1 + 1 & j1 = j2 ) ; ::_thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) )
(G * (i2,j2)) `2 = (G * (1,j2)) `2 by A20, A11, A22, GOBOARD5:1
.= S-bound (L~ f) by A12, A17, A21, A10, A69, GOBOARD5:1 ;
then G * (i2,j2) in S-most (L~ f) by A8, A14, A15, GOBOARD1:1, SPRECT_2:11;
then (G * (i1,j1)) `1 >= (G * (i2,j2)) `1 by A4, A6, PSCOMP_1:55;
then i1 >= i1 + 1 by A17, A21, A20, A69, GOBOARD5:3;
hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) by NAT_1:13; ::_thesis: verum
end;
end;
end;
hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) ; ::_thesis: f /. (k + 1) = G * (i2,j2)
thus f /. (k + 1) = G * (i2,j2) by A8; ::_thesis: verum
end;
theorem :: JORDAN1I:25
for f being non constant standard special_circular_sequence holds
( f is clockwise_oriented iff (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) )
proof
set i = 1;
let f be non constant standard special_circular_sequence; ::_thesis: ( f is clockwise_oriented iff (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) )
set r = Rotate (f,(W-min (L~ f)));
A1: Rotate (f,(W-min (L~ f))) is_sequence_on GoB (Rotate (f,(W-min (L~ f)))) by GOBOARD5:def_5;
A2: 1 + 1 <= len (Rotate (f,(W-min (L~ f)))) by TOPREAL8:3;
then A3: Int (left_cell ((Rotate (f,(W-min (L~ f)))),1)) c= LeftComp (Rotate (f,(W-min (L~ f)))) by GOBOARD9:21;
set j = i_s_w (Rotate (f,(W-min (L~ f))));
A4: W-min (L~ f) in rng f by SPRECT_2:43;
then A5: (Rotate (f,(W-min (L~ f)))) /. 1 = W-min (L~ f) by FINSEQ_6:92;
A6: 2 <= len f by TOPREAL8:3;
thus ( f is clockwise_oriented implies (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) ) ::_thesis: ( (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) implies f is clockwise_oriented )
proof
set k = (W-min (L~ f)) .. f;
(W-min (L~ f)) .. f < len f by SPRECT_5:20;
then A7: ((W-min (L~ f)) .. f) + 1 <= len f by NAT_1:13;
1 <= ((W-min (L~ f)) .. f) + 1 by NAT_1:11;
then A8: ((W-min (L~ f)) .. f) + 1 in dom f by A7, FINSEQ_3:25;
then f /. (((W-min (L~ f)) .. f) + 1) = f . (((W-min (L~ f)) .. f) + 1) by PARTFUN1:def_6;
then A9: f /. (((W-min (L~ f)) .. f) + 1) in rng f by A8, FUNCT_1:3;
A10: rng f c= L~ f by A6, SPPOL_2:18;
A11: f /. ((W-min (L~ f)) .. f) = W-min (L~ f) by A4, FINSEQ_5:38;
(W-min (L~ f)) .. f <= ((W-min (L~ f)) .. f) + 1 by NAT_1:13;
then A12: f /. (((W-min (L~ f)) .. f) + 1) = (Rotate (f,(W-min (L~ f)))) /. (((((W-min (L~ f)) .. f) + 1) + 1) -' ((W-min (L~ f)) .. f)) by A4, A7, REVROT_1:10
.= (Rotate (f,(W-min (L~ f)))) /. ((((W-min (L~ f)) .. f) + (1 + 1)) -' ((W-min (L~ f)) .. f))
.= (Rotate (f,(W-min (L~ f)))) /. 2 by NAT_D:34 ;
f is_sequence_on GoB f by GOBOARD5:def_5;
then A13: f is_sequence_on GoB (Rotate (f,(W-min (L~ f)))) by REVROT_1:28;
assume f is clockwise_oriented ; ::_thesis: (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f)
then consider i, j being Element of NAT such that
A14: [i,j] in Indices (GoB (Rotate (f,(W-min (L~ f))))) and
A15: [i,(j + 1)] in Indices (GoB (Rotate (f,(W-min (L~ f))))) and
A16: f /. ((W-min (L~ f)) .. f) = (GoB (Rotate (f,(W-min (L~ f))))) * (i,j) and
A17: f /. (((W-min (L~ f)) .. f) + 1) = (GoB (Rotate (f,(W-min (L~ f))))) * (i,(j + 1)) by A4, A7, A11, A13, Th21, FINSEQ_4:21;
A18: ( 1 <= i & i <= len (GoB (Rotate (f,(W-min (L~ f))))) ) by A14, MATRIX_1:38;
A19: ( 1 <= j + 1 & j + 1 <= width (GoB (Rotate (f,(W-min (L~ f))))) ) by A15, MATRIX_1:38;
A20: ( 1 <= j & j <= width (GoB (Rotate (f,(W-min (L~ f))))) ) by A14, MATRIX_1:38;
( 1 <= i & i <= len (GoB (Rotate (f,(W-min (L~ f))))) ) by A14, MATRIX_1:38;
then (f /. (((W-min (L~ f)) .. f) + 1)) `1 = ((GoB (Rotate (f,(W-min (L~ f))))) * (i,1)) `1 by A17, A19, GOBOARD5:2
.= (f /. ((W-min (L~ f)) .. f)) `1 by A16, A18, A20, GOBOARD5:2
.= W-bound (L~ f) by A11, EUCLID:52 ;
hence (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) by A12, A9, A10, SPRECT_2:12; ::_thesis: verum
end;
A21: [1,(i_s_w (Rotate (f,(W-min (L~ f)))))] in Indices (GoB (Rotate (f,(W-min (L~ f))))) by JORDAN5D:def_1;
then A22: ( 1 <= len (GoB (Rotate (f,(W-min (L~ f))))) & i_s_w (Rotate (f,(W-min (L~ f)))) <= width (GoB (Rotate (f,(W-min (L~ f))))) ) by MATRIX_1:38;
len (Rotate (f,(W-min (L~ f)))) > 2 by TOPREAL8:3;
then A23: 1 + 1 in dom (Rotate (f,(W-min (L~ f)))) by FINSEQ_3:25;
then consider i2, j2 being Element of NAT such that
A24: [i2,j2] in Indices (GoB (Rotate (f,(W-min (L~ f))))) and
A25: (Rotate (f,(W-min (L~ f)))) /. (1 + 1) = (GoB (Rotate (f,(W-min (L~ f))))) * (i2,j2) by A1, GOBOARD1:def_9;
A26: 1 <= j2 by A24, MATRIX_1:38;
A27: L~ (Rotate (f,(W-min (L~ f)))) = L~ f by REVROT_1:33;
then A28: (GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f)))))) = (Rotate (f,(W-min (L~ f)))) /. 1 by A5, JORDAN5D:def_1;
assume A29: (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) ; ::_thesis: f is clockwise_oriented
then ((GoB (Rotate (f,(W-min (L~ f))))) * (i2,j2)) `1 = ((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `1 by A5, A28, A25, PSCOMP_1:31;
then A30: i2 = 1 by A21, A24, JORDAN1G:7;
rng (Rotate (f,(W-min (L~ f)))) = rng f by FINSEQ_6:90, SPRECT_2:43;
then 1 in dom (Rotate (f,(W-min (L~ f)))) by FINSEQ_3:31, SPRECT_2:43;
then (abs (1 - 1)) + (abs ((i_s_w (Rotate (f,(W-min (L~ f))))) - j2)) = 1 by A1, A21, A28, A23, A24, A25, A30, GOBOARD1:def_9;
then 0 + (abs ((i_s_w (Rotate (f,(W-min (L~ f))))) - j2)) = 1 by ABSVALUE:2;
then A31: abs (j2 - (i_s_w (Rotate (f,(W-min (L~ f)))))) = 1 by UNIFORM1:11;
((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `2 <= ((GoB (Rotate (f,(W-min (L~ f))))) * (i2,j2)) `2 by A5, A28, A29, A25, PSCOMP_1:31;
then j2 - (i_s_w (Rotate (f,(W-min (L~ f))))) >= 0 by A22, A30, A26, GOBOARD5:4, XREAL_1:48;
then A32: j2 - (i_s_w (Rotate (f,(W-min (L~ f))))) = 1 by A31, ABSVALUE:def_1;
then j2 = (i_s_w (Rotate (f,(W-min (L~ f))))) + 1 ;
then ( 1 -' 1 = 1 - 1 & left_cell ((Rotate (f,(W-min (L~ f)))),1,(GoB (Rotate (f,(W-min (L~ f)))))) = cell ((GoB (Rotate (f,(W-min (L~ f))))),(1 -' 1),(i_s_w (Rotate (f,(W-min (L~ f)))))) ) by A2, A1, A21, A28, A24, A25, A30, GOBRD13:21, XREAL_1:233;
then A33: left_cell ((Rotate (f,(W-min (L~ f)))),1) = cell ((GoB (Rotate (f,(W-min (L~ f))))),0,(i_s_w (Rotate (f,(W-min (L~ f)))))) by A2, JORDAN1H:21;
Int (left_cell ((Rotate (f,(W-min (L~ f)))),1)) <> {} by A2, GOBOARD9:15;
then consider p being set such that
A34: p in Int (left_cell ((Rotate (f,(W-min (L~ f)))),1)) by XBOOLE_0:def_1;
reconsider p = p as Point of (TOP-REAL 2) by A34;
A35: ( LeftComp (Rotate (f,(W-min (L~ f)))) is_a_component_of (L~ (Rotate (f,(W-min (L~ f))))) ` & UBD (L~ (Rotate (f,(W-min (L~ f))))) is_a_component_of (L~ (Rotate (f,(W-min (L~ f))))) ` ) by GOBOARD9:def_1, JORDAN2C:124;
A36: 1 <= i_s_w (Rotate (f,(W-min (L~ f)))) by A21, MATRIX_1:38;
(i_s_w (Rotate (f,(W-min (L~ f))))) + 1 <= width (GoB (Rotate (f,(W-min (L~ f))))) by A24, A32, MATRIX_1:38;
then i_s_w (Rotate (f,(W-min (L~ f)))) < width (GoB (Rotate (f,(W-min (L~ f))))) by NAT_1:13;
then Int (left_cell ((Rotate (f,(W-min (L~ f)))),1)) = { |[t,s]| where t, s is Real : ( t < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,1)) `1 & ((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `2 < s & s < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,((i_s_w (Rotate (f,(W-min (L~ f))))) + 1))) `2 ) } by A36, A33, GOBOARD6:20;
then consider t, s being Real such that
A37: p = |[t,s]| and
A38: t < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,1)) `1 and
((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `2 < s and
s < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,((i_s_w (Rotate (f,(W-min (L~ f))))) + 1))) `2 by A34;
now__::_thesis:_not_west_halfline_p_meets_L~_(Rotate_(f,(W-min_(L~_f))))
A39: ((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `1 = ((GoB (Rotate (f,(W-min (L~ f))))) * (1,1)) `1 by A36, A22, GOBOARD5:2;
assume west_halfline p meets L~ (Rotate (f,(W-min (L~ f)))) ; ::_thesis: contradiction
then (west_halfline p) /\ (L~ (Rotate (f,(W-min (L~ f))))) <> {} by XBOOLE_0:def_7;
then consider a being set such that
A40: a in (west_halfline p) /\ (L~ (Rotate (f,(W-min (L~ f))))) by XBOOLE_0:def_1;
A41: a in L~ (Rotate (f,(W-min (L~ f)))) by A40, XBOOLE_0:def_4;
A42: a in west_halfline p by A40, XBOOLE_0:def_4;
reconsider a = a as Point of (TOP-REAL 2) by A40;
a `1 <= p `1 by A42, TOPREAL1:def_13;
then a `1 <= t by A37, EUCLID:52;
then a `1 < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `1 by A38, A39, XXREAL_0:2;
then a `1 < W-bound (L~ (Rotate (f,(W-min (L~ f))))) by A27, A5, A28, EUCLID:52;
hence contradiction by A41, PSCOMP_1:24; ::_thesis: verum
end;
then A43: west_halfline p c= UBD (L~ (Rotate (f,(W-min (L~ f))))) by JORDAN2C:126;
p in west_halfline p by TOPREAL1:38;
then LeftComp (Rotate (f,(W-min (L~ f)))) meets UBD (L~ (Rotate (f,(W-min (L~ f))))) by A3, A34, A43, XBOOLE_0:3;
then Rotate (f,(W-min (L~ f))) is clockwise_oriented by A35, GOBOARD9:1, JORDAN1H:41;
hence f is clockwise_oriented by JORDAN1H:40; ::_thesis: verum
end;
theorem :: JORDAN1I:26
for f being non constant standard special_circular_sequence holds
( f is clockwise_oriented iff (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) )
proof
let f be non constant standard special_circular_sequence; ::_thesis: ( f is clockwise_oriented iff (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) )
set r = Rotate (f,(E-max (L~ f)));
set j = i_n_e (Rotate (f,(E-max (L~ f))));
set i = len (GoB (Rotate (f,(E-max (L~ f)))));
A1: ( 1 + 1 <= len (Rotate (f,(E-max (L~ f)))) & Rotate (f,(E-max (L~ f))) is_sequence_on GoB (Rotate (f,(E-max (L~ f)))) ) by GOBOARD5:def_5, TOPREAL8:3;
A2: E-max (L~ f) in rng f by SPRECT_2:46;
then A3: (Rotate (f,(E-max (L~ f)))) /. 1 = E-max (L~ f) by FINSEQ_6:92;
A4: 2 <= len f by TOPREAL8:3;
thus ( f is clockwise_oriented implies (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) ) ::_thesis: ( (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) implies f is clockwise_oriented )
proof
set k = (E-max (L~ f)) .. f;
(E-max (L~ f)) .. f < len f by SPRECT_5:16;
then A5: ((E-max (L~ f)) .. f) + 1 <= len f by NAT_1:13;
1 <= ((E-max (L~ f)) .. f) + 1 by NAT_1:11;
then A6: ((E-max (L~ f)) .. f) + 1 in dom f by A5, FINSEQ_3:25;
then f /. (((E-max (L~ f)) .. f) + 1) = f . (((E-max (L~ f)) .. f) + 1) by PARTFUN1:def_6;
then A7: f /. (((E-max (L~ f)) .. f) + 1) in rng f by A6, FUNCT_1:3;
A8: rng f c= L~ f by A4, SPPOL_2:18;
A9: f /. ((E-max (L~ f)) .. f) = E-max (L~ f) by A2, FINSEQ_5:38;
(E-max (L~ f)) .. f <= ((E-max (L~ f)) .. f) + 1 by NAT_1:13;
then A10: f /. (((E-max (L~ f)) .. f) + 1) = (Rotate (f,(E-max (L~ f)))) /. (((((E-max (L~ f)) .. f) + 1) + 1) -' ((E-max (L~ f)) .. f)) by A2, A5, REVROT_1:10
.= (Rotate (f,(E-max (L~ f)))) /. ((((E-max (L~ f)) .. f) + (1 + 1)) -' ((E-max (L~ f)) .. f))
.= (Rotate (f,(E-max (L~ f)))) /. 2 by NAT_D:34 ;
f is_sequence_on GoB f by GOBOARD5:def_5;
then A11: f is_sequence_on GoB (Rotate (f,(E-max (L~ f)))) by REVROT_1:28;
assume f is clockwise_oriented ; ::_thesis: (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f)
then consider i, j being Element of NAT such that
A12: [i,(j + 1)] in Indices (GoB (Rotate (f,(E-max (L~ f))))) and
A13: [i,j] in Indices (GoB (Rotate (f,(E-max (L~ f))))) and
A14: f /. ((E-max (L~ f)) .. f) = (GoB (Rotate (f,(E-max (L~ f))))) * (i,(j + 1)) and
A15: f /. (((E-max (L~ f)) .. f) + 1) = (GoB (Rotate (f,(E-max (L~ f))))) * (i,j) by A2, A5, A9, A11, Th23, FINSEQ_4:21;
A16: ( 1 <= j & j <= width (GoB (Rotate (f,(E-max (L~ f))))) ) by A13, MATRIX_1:38;
A17: ( 1 <= j + 1 & j + 1 <= width (GoB (Rotate (f,(E-max (L~ f))))) ) by A12, MATRIX_1:38;
A18: ( 1 <= i & i <= len (GoB (Rotate (f,(E-max (L~ f))))) ) by A12, MATRIX_1:38;
( 1 <= i & i <= len (GoB (Rotate (f,(E-max (L~ f))))) ) by A12, MATRIX_1:38;
then (f /. (((E-max (L~ f)) .. f) + 1)) `1 = ((GoB (Rotate (f,(E-max (L~ f))))) * (i,1)) `1 by A15, A16, GOBOARD5:2
.= (f /. ((E-max (L~ f)) .. f)) `1 by A14, A18, A17, GOBOARD5:2
.= E-bound (L~ f) by A9, EUCLID:52 ;
hence (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) by A10, A7, A8, SPRECT_2:13; ::_thesis: verum
end;
assume A19: (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) ; ::_thesis: f is clockwise_oriented
len (Rotate (f,(E-max (L~ f)))) > 2 by TOPREAL8:3;
then A20: ( Rotate (f,(E-max (L~ f))) is_sequence_on GoB (Rotate (f,(E-max (L~ f)))) & 1 + 1 in dom (Rotate (f,(E-max (L~ f)))) ) by FINSEQ_3:25, GOBOARD5:def_5;
then consider i2, j2 being Element of NAT such that
A21: [i2,j2] in Indices (GoB (Rotate (f,(E-max (L~ f))))) and
A22: (Rotate (f,(E-max (L~ f)))) /. (1 + 1) = (GoB (Rotate (f,(E-max (L~ f))))) * (i2,j2) by GOBOARD1:def_9;
A23: j2 <= width (GoB (Rotate (f,(E-max (L~ f))))) by A21, MATRIX_1:38;
A24: [(len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f)))))] in Indices (GoB (Rotate (f,(E-max (L~ f))))) by JORDAN5D:def_4;
then A25: 1 <= i_n_e (Rotate (f,(E-max (L~ f)))) by MATRIX_1:38;
then A26: [(len (GoB (Rotate (f,(E-max (L~ f)))))),(((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1) + 1)] in Indices (GoB (Rotate (f,(E-max (L~ f))))) by A24, XREAL_1:235;
A27: L~ (Rotate (f,(E-max (L~ f)))) = L~ f by REVROT_1:33;
then A28: (GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f)))))) = (Rotate (f,(E-max (L~ f)))) /. 1 by A3, JORDAN5D:def_4;
then A29: (Rotate (f,(E-max (L~ f)))) /. 1 = (GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1) + 1)) by A25, XREAL_1:235;
(GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f)))))) in E-most (L~ (Rotate (f,(E-max (L~ f))))) by A27, A3, A28, PSCOMP_1:50;
then ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f))))))) `1 = (E-min (L~ (Rotate (f,(E-max (L~ f)))))) `1 by PSCOMP_1:47;
then A30: ((GoB (Rotate (f,(E-max (L~ f))))) * (i2,j2)) `1 = ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f))))))) `1 by A27, A19, A22, PSCOMP_1:47;
then A31: i2 = len (GoB (Rotate (f,(E-max (L~ f))))) by A24, A21, JORDAN1G:7;
A32: 1 + 1 <= len (Rotate (f,(E-max (L~ f)))) by TOPREAL8:3;
then A33: Int (left_cell ((Rotate (f,(E-max (L~ f)))),1)) c= LeftComp (Rotate (f,(E-max (L~ f)))) by GOBOARD9:21;
Int (left_cell ((Rotate (f,(E-max (L~ f)))),1)) <> {} by A32, GOBOARD9:15;
then consider p being set such that
A34: p in Int (left_cell ((Rotate (f,(E-max (L~ f)))),1)) by XBOOLE_0:def_1;
reconsider p = p as Point of (TOP-REAL 2) by A34;
A35: ( LeftComp (Rotate (f,(E-max (L~ f)))) is_a_component_of (L~ (Rotate (f,(E-max (L~ f))))) ` & UBD (L~ (Rotate (f,(E-max (L~ f))))) is_a_component_of (L~ (Rotate (f,(E-max (L~ f))))) ` ) by GOBOARD9:def_1, JORDAN2C:124;
A36: 1 <= j2 by A21, MATRIX_1:38;
A37: i_n_e (Rotate (f,(E-max (L~ f)))) <= width (GoB (Rotate (f,(E-max (L~ f))))) by A24, MATRIX_1:38;
rng (Rotate (f,(E-max (L~ f)))) = rng f by FINSEQ_6:90, SPRECT_2:46;
then 1 in dom (Rotate (f,(E-max (L~ f)))) by FINSEQ_3:31, SPRECT_2:46;
then (abs (i2 - i2)) + (abs ((i_n_e (Rotate (f,(E-max (L~ f))))) - j2)) = 1 by A24, A28, A20, A21, A22, A31, GOBOARD1:def_9;
then A38: 0 + (abs ((i_n_e (Rotate (f,(E-max (L~ f))))) - j2)) = 1 by ABSVALUE:2;
A39: 1 <= len (GoB (Rotate (f,(E-max (L~ f))))) by A24, MATRIX_1:38;
((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f))))))) `2 >= ((GoB (Rotate (f,(E-max (L~ f))))) * (i2,j2)) `2 by A3, A28, A19, A22, PSCOMP_1:47;
then (i_n_e (Rotate (f,(E-max (L~ f))))) - j2 >= 0 by A39, A25, A31, A23, GOBOARD5:4, XREAL_1:48;
then A40: (i_n_e (Rotate (f,(E-max (L~ f))))) - j2 = 1 by A38, ABSVALUE:def_1;
then j2 = (i_n_e (Rotate (f,(E-max (L~ f))))) - 1 ;
then A41: j2 = (i_n_e (Rotate (f,(E-max (L~ f))))) -' 1 by A25, XREAL_1:233;
then ( [(len (GoB (Rotate (f,(E-max (L~ f)))))),((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1)] in Indices (GoB (Rotate (f,(E-max (L~ f))))) & (Rotate (f,(E-max (L~ f)))) /. (1 + 1) = (GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1)) ) by A24, A21, A22, A30, JORDAN1G:7;
then left_cell ((Rotate (f,(E-max (L~ f)))),1,(GoB (Rotate (f,(E-max (L~ f)))))) = cell ((GoB (Rotate (f,(E-max (L~ f))))),(len (GoB (Rotate (f,(E-max (L~ f)))))),((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1)) by A1, A26, A29, GOBRD13:27;
then A42: left_cell ((Rotate (f,(E-max (L~ f)))),1) = cell ((GoB (Rotate (f,(E-max (L~ f))))),(len (GoB (Rotate (f,(E-max (L~ f)))))),((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1)) by A32, JORDAN1H:21;
(i_n_e (Rotate (f,(E-max (L~ f))))) - 1 < (i_n_e (Rotate (f,(E-max (L~ f))))) - 0 by XREAL_1:15;
then (i_n_e (Rotate (f,(E-max (L~ f))))) -' 1 < width (GoB (Rotate (f,(E-max (L~ f))))) by A37, A40, A41, XXREAL_0:2;
then Int (left_cell ((Rotate (f,(E-max (L~ f)))),1)) = { |[t,s]| where t, s is Real : ( ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),1)) `1 < t & ((GoB (Rotate (f,(E-max (L~ f))))) * (1,((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1))) `2 < s & s < ((GoB (Rotate (f,(E-max (L~ f))))) * (1,(((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1) + 1))) `2 ) } by A36, A41, A42, GOBOARD6:23;
then consider t, s being Real such that
A43: p = |[t,s]| and
A44: ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),1)) `1 < t and
((GoB (Rotate (f,(E-max (L~ f))))) * (1,((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1))) `2 < s and
s < ((GoB (Rotate (f,(E-max (L~ f))))) * (1,(((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1) + 1))) `2 by A34;
now__::_thesis:_not_east_halfline_p_meets_L~_(Rotate_(f,(E-max_(L~_f))))
assume east_halfline p meets L~ (Rotate (f,(E-max (L~ f)))) ; ::_thesis: contradiction
then (east_halfline p) /\ (L~ (Rotate (f,(E-max (L~ f))))) <> {} by XBOOLE_0:def_7;
then consider a being set such that
A45: a in (east_halfline p) /\ (L~ (Rotate (f,(E-max (L~ f))))) by XBOOLE_0:def_1;
A46: a in L~ (Rotate (f,(E-max (L~ f)))) by A45, XBOOLE_0:def_4;
A47: a in east_halfline p by A45, XBOOLE_0:def_4;
reconsider a = a as Point of (TOP-REAL 2) by A45;
a `1 >= p `1 by A47, TOPREAL1:def_11;
then A48: a `1 >= t by A43, EUCLID:52;
((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),1)) `1 = ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f))))))) `1 by A39, A25, A37, GOBOARD5:2;
then a `1 > ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f))))))) `1 by A44, A48, XXREAL_0:2;
then a `1 > E-bound (L~ (Rotate (f,(E-max (L~ f))))) by A27, A3, A28, EUCLID:52;
hence contradiction by A46, PSCOMP_1:24; ::_thesis: verum
end;
then A49: east_halfline p c= UBD (L~ (Rotate (f,(E-max (L~ f))))) by JORDAN2C:127;
p in east_halfline p by TOPREAL1:38;
then LeftComp (Rotate (f,(E-max (L~ f)))) meets UBD (L~ (Rotate (f,(E-max (L~ f))))) by A33, A34, A49, XBOOLE_0:3;
then Rotate (f,(E-max (L~ f))) is clockwise_oriented by A35, GOBOARD9:1, JORDAN1H:41;
hence f is clockwise_oriented by JORDAN1H:40; ::_thesis: verum
end;
theorem :: JORDAN1I:27
for f being non constant standard special_circular_sequence holds
( f is clockwise_oriented iff (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) )
proof
set j = 1;
let f be non constant standard special_circular_sequence; ::_thesis: ( f is clockwise_oriented iff (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) )
set r = Rotate (f,(S-max (L~ f)));
A1: Rotate (f,(S-max (L~ f))) is_sequence_on GoB (Rotate (f,(S-max (L~ f)))) by GOBOARD5:def_5;
len (Rotate (f,(S-max (L~ f)))) > 2 by TOPREAL8:3;
then A2: 1 + 1 in dom (Rotate (f,(S-max (L~ f)))) by FINSEQ_3:25;
then consider i2, j2 being Element of NAT such that
A3: [i2,j2] in Indices (GoB (Rotate (f,(S-max (L~ f))))) and
A4: (Rotate (f,(S-max (L~ f)))) /. (1 + 1) = (GoB (Rotate (f,(S-max (L~ f))))) * (i2,j2) by A1, GOBOARD1:def_9;
A5: i2 <= len (GoB (Rotate (f,(S-max (L~ f))))) by A3, MATRIX_1:38;
set i = i_e_s (Rotate (f,(S-max (L~ f))));
A6: S-max (L~ f) in rng f by SPRECT_2:42;
then A7: (Rotate (f,(S-max (L~ f)))) /. 1 = S-max (L~ f) by FINSEQ_6:92;
A8: 2 <= len f by TOPREAL8:3;
thus ( f is clockwise_oriented implies (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) ) ::_thesis: ( (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) implies f is clockwise_oriented )
proof
set k = (S-max (L~ f)) .. f;
(S-max (L~ f)) .. f < len f by SPRECT_5:14;
then A9: ((S-max (L~ f)) .. f) + 1 <= len f by NAT_1:13;
1 <= ((S-max (L~ f)) .. f) + 1 by NAT_1:11;
then A10: ((S-max (L~ f)) .. f) + 1 in dom f by A9, FINSEQ_3:25;
then f /. (((S-max (L~ f)) .. f) + 1) = f . (((S-max (L~ f)) .. f) + 1) by PARTFUN1:def_6;
then A11: f /. (((S-max (L~ f)) .. f) + 1) in rng f by A10, FUNCT_1:3;
A12: rng f c= L~ f by A8, SPPOL_2:18;
A13: f /. ((S-max (L~ f)) .. f) = S-max (L~ f) by A6, FINSEQ_5:38;
(S-max (L~ f)) .. f <= ((S-max (L~ f)) .. f) + 1 by NAT_1:13;
then A14: f /. (((S-max (L~ f)) .. f) + 1) = (Rotate (f,(S-max (L~ f)))) /. (((((S-max (L~ f)) .. f) + 1) + 1) -' ((S-max (L~ f)) .. f)) by A6, A9, REVROT_1:10
.= (Rotate (f,(S-max (L~ f)))) /. ((((S-max (L~ f)) .. f) + (1 + 1)) -' ((S-max (L~ f)) .. f))
.= (Rotate (f,(S-max (L~ f)))) /. 2 by NAT_D:34 ;
f is_sequence_on GoB f by GOBOARD5:def_5;
then A15: f is_sequence_on GoB (Rotate (f,(S-max (L~ f)))) by REVROT_1:28;
assume f is clockwise_oriented ; ::_thesis: (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f)
then consider i, j being Element of NAT such that
A16: [(i + 1),j] in Indices (GoB (Rotate (f,(S-max (L~ f))))) and
A17: [i,j] in Indices (GoB (Rotate (f,(S-max (L~ f))))) and
A18: f /. ((S-max (L~ f)) .. f) = (GoB (Rotate (f,(S-max (L~ f))))) * ((i + 1),j) and
A19: f /. (((S-max (L~ f)) .. f) + 1) = (GoB (Rotate (f,(S-max (L~ f))))) * (i,j) by A6, A9, A13, A15, Th24, FINSEQ_4:21;
A20: ( 1 <= i + 1 & i + 1 <= len (GoB (Rotate (f,(S-max (L~ f))))) ) by A16, MATRIX_1:38;
A21: ( 1 <= j & j <= width (GoB (Rotate (f,(S-max (L~ f))))) ) by A16, MATRIX_1:38;
A22: ( 1 <= j & j <= width (GoB (Rotate (f,(S-max (L~ f))))) ) by A16, MATRIX_1:38;
( 1 <= i & i <= len (GoB (Rotate (f,(S-max (L~ f))))) ) by A17, MATRIX_1:38;
then (f /. (((S-max (L~ f)) .. f) + 1)) `2 = ((GoB (Rotate (f,(S-max (L~ f))))) * (1,j)) `2 by A19, A21, GOBOARD5:1
.= (f /. ((S-max (L~ f)) .. f)) `2 by A18, A20, A22, GOBOARD5:1
.= S-bound (L~ f) by A13, EUCLID:52 ;
hence (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) by A14, A11, A12, SPRECT_2:11; ::_thesis: verum
end;
assume A23: (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) ; ::_thesis: f is clockwise_oriented
A24: [(i_e_s (Rotate (f,(S-max (L~ f))))),1] in Indices (GoB (Rotate (f,(S-max (L~ f))))) by JORDAN5D:def_6;
then A25: 1 <= i_e_s (Rotate (f,(S-max (L~ f)))) by MATRIX_1:38;
A26: L~ (Rotate (f,(S-max (L~ f)))) = L~ f by REVROT_1:33;
then A27: (GoB (Rotate (f,(S-max (L~ f))))) * ((i_e_s (Rotate (f,(S-max (L~ f))))),1) = (Rotate (f,(S-max (L~ f)))) /. 1 by A7, JORDAN5D:def_6;
then ((GoB (Rotate (f,(S-max (L~ f))))) * ((i_e_s (Rotate (f,(S-max (L~ f))))),1)) `2 = S-bound (L~ f) by A7, EUCLID:52
.= (S-min (L~ f)) `2 by EUCLID:52 ;
then ((GoB (Rotate (f,(S-max (L~ f))))) * (i2,j2)) `2 = ((GoB (Rotate (f,(S-max (L~ f))))) * ((i_e_s (Rotate (f,(S-max (L~ f))))),1)) `2 by A23, A4, PSCOMP_1:55;
then A28: j2 = 1 by A24, A3, JORDAN1G:6;
A29: 1 <= width (GoB (Rotate (f,(S-max (L~ f))))) by A24, MATRIX_1:38;
rng (Rotate (f,(S-max (L~ f)))) = rng f by FINSEQ_6:90, SPRECT_2:42;
then 1 in dom (Rotate (f,(S-max (L~ f)))) by FINSEQ_3:31, SPRECT_2:42;
then (abs (1 - 1)) + (abs ((i_e_s (Rotate (f,(S-max (L~ f))))) - i2)) = 1 by A1, A24, A27, A2, A3, A4, A28, GOBOARD1:def_9;
then A30: 0 + (abs ((i_e_s (Rotate (f,(S-max (L~ f))))) - i2)) = 1 by ABSVALUE:2;
((GoB (Rotate (f,(S-max (L~ f))))) * (i2,j2)) `1 <= ((GoB (Rotate (f,(S-max (L~ f))))) * ((i_e_s (Rotate (f,(S-max (L~ f))))),1)) `1 by A7, A27, A23, A4, PSCOMP_1:55;
then (i_e_s (Rotate (f,(S-max (L~ f))))) - i2 >= 0 by A25, A29, A28, A5, GOBOARD5:3, XREAL_1:48;
then A31: (i_e_s (Rotate (f,(S-max (L~ f))))) - i2 = 1 by A30, ABSVALUE:def_1;
then i2 = (i_e_s (Rotate (f,(S-max (L~ f))))) - 1 ;
then A32: i2 = (i_e_s (Rotate (f,(S-max (L~ f))))) -' 1 by A25, XREAL_1:233;
then A33: 1 <= (i_e_s (Rotate (f,(S-max (L~ f))))) -' 1 by A3, MATRIX_1:38;
A34: i_e_s (Rotate (f,(S-max (L~ f)))) <= len (GoB (Rotate (f,(S-max (L~ f))))) by A24, MATRIX_1:38;
A35: 1 + 1 <= len (Rotate (f,(S-max (L~ f)))) by TOPREAL8:3;
then A36: Int (left_cell ((Rotate (f,(S-max (L~ f)))),1)) c= LeftComp (Rotate (f,(S-max (L~ f)))) by GOBOARD9:21;
Int (left_cell ((Rotate (f,(S-max (L~ f)))),1)) <> {} by A35, GOBOARD9:15;
then consider p being set such that
A37: p in Int (left_cell ((Rotate (f,(S-max (L~ f)))),1)) by XBOOLE_0:def_1;
[(((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1) + 1),1] in Indices (GoB (Rotate (f,(S-max (L~ f))))) by A24, A25, XREAL_1:235;
then ( 1 -' 1 = 1 - 1 & left_cell ((Rotate (f,(S-max (L~ f)))),1,(GoB (Rotate (f,(S-max (L~ f)))))) = cell ((GoB (Rotate (f,(S-max (L~ f))))),((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1),(1 -' 1)) ) by A35, A1, A27, A3, A4, A28, A31, A32, GOBRD13:25, XREAL_1:233;
then A38: left_cell ((Rotate (f,(S-max (L~ f)))),1) = cell ((GoB (Rotate (f,(S-max (L~ f))))),((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1),0) by A35, JORDAN1H:21;
(i_e_s (Rotate (f,(S-max (L~ f))))) - 1 < i_e_s (Rotate (f,(S-max (L~ f)))) by XREAL_1:146;
then (i_e_s (Rotate (f,(S-max (L~ f))))) -' 1 < len (GoB (Rotate (f,(S-max (L~ f))))) by A34, A31, A32, XXREAL_0:2;
then A39: Int (left_cell ((Rotate (f,(S-max (L~ f)))),1)) = { |[t,s]| where t, s is Real : ( ((GoB (Rotate (f,(S-max (L~ f))))) * (((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1),1)) `1 < t & t < ((GoB (Rotate (f,(S-max (L~ f))))) * ((((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1) + 1),1)) `1 & s < ((GoB (Rotate (f,(S-max (L~ f))))) * (1,1)) `2 ) } by A33, A38, GOBOARD6:24;
reconsider p = p as Point of (TOP-REAL 2) by A37;
A40: ( LeftComp (Rotate (f,(S-max (L~ f)))) is_a_component_of (L~ (Rotate (f,(S-max (L~ f))))) ` & UBD (L~ (Rotate (f,(S-max (L~ f))))) is_a_component_of (L~ (Rotate (f,(S-max (L~ f))))) ` ) by GOBOARD9:def_1, JORDAN2C:124;
consider t, s being Real such that
A41: p = |[t,s]| and
((GoB (Rotate (f,(S-max (L~ f))))) * (((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1),1)) `1 < t and
t < ((GoB (Rotate (f,(S-max (L~ f))))) * ((((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1) + 1),1)) `1 and
A42: s < ((GoB (Rotate (f,(S-max (L~ f))))) * (1,1)) `2 by A39, A37;
now__::_thesis:_not_south_halfline_p_meets_L~_(Rotate_(f,(S-max_(L~_f))))
assume south_halfline p meets L~ (Rotate (f,(S-max (L~ f)))) ; ::_thesis: contradiction
then (south_halfline p) /\ (L~ (Rotate (f,(S-max (L~ f))))) <> {} by XBOOLE_0:def_7;
then consider a being set such that
A43: a in (south_halfline p) /\ (L~ (Rotate (f,(S-max (L~ f))))) by XBOOLE_0:def_1;
A44: a in L~ (Rotate (f,(S-max (L~ f)))) by A43, XBOOLE_0:def_4;
A45: a in south_halfline p by A43, XBOOLE_0:def_4;
reconsider a = a as Point of (TOP-REAL 2) by A43;
a `2 <= p `2 by A45, TOPREAL1:def_12;
then a `2 <= s by A41, EUCLID:52;
then A46: a `2 < ((GoB (Rotate (f,(S-max (L~ f))))) * (1,1)) `2 by A42, XXREAL_0:2;
((GoB (Rotate (f,(S-max (L~ f))))) * ((i_e_s (Rotate (f,(S-max (L~ f))))),1)) `2 = ((GoB (Rotate (f,(S-max (L~ f))))) * (1,1)) `2 by A25, A34, A29, GOBOARD5:1;
then a `2 < S-bound (L~ (Rotate (f,(S-max (L~ f))))) by A26, A7, A27, A46, EUCLID:52;
hence contradiction by A44, PSCOMP_1:24; ::_thesis: verum
end;
then A47: south_halfline p c= UBD (L~ (Rotate (f,(S-max (L~ f))))) by JORDAN2C:128;
p in south_halfline p by TOPREAL1:38;
then LeftComp (Rotate (f,(S-max (L~ f)))) meets UBD (L~ (Rotate (f,(S-max (L~ f))))) by A36, A37, A47, XBOOLE_0:3;
then Rotate (f,(S-max (L~ f))) is clockwise_oriented by A40, GOBOARD9:1, JORDAN1H:41;
hence f is clockwise_oriented by JORDAN1H:40; ::_thesis: verum
end;
theorem :: JORDAN1I:28
for i, k being Element of NAT
for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds
ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )
proof
let i, k be Element of NAT ; ::_thesis: for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds
ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )
let C be non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds
ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )
let p be Point of (TOP-REAL 2); ::_thesis: ( p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) implies ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) ) )
assume that
A1: p `1 = ((W-bound C) + (E-bound C)) / 2 and
A2: i > 0 and
A3: 1 <= k and
A4: k <= width (Gauge (C,i)) and
A5: (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) and
A6: p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) ; ::_thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )
set f = Lower_Seq (C,i);
set G = Gauge (C,i);
A7: Center (Gauge (C,i)) <= len (Gauge (C,i)) by JORDAN1B:13;
4 <= len (Gauge (C,i)) by JORDAN8:10;
then A8: 1 <= len (Gauge (C,i)) by XXREAL_0:2;
4 <= len (Gauge (C,1)) by JORDAN8:10;
then 1 <= len (Gauge (C,1)) by XXREAL_0:2;
then A9: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1 by A2, A8, JORDAN1A:36;
A10: ( 1 <= Center (Gauge (C,1)) & Center (Gauge (C,1)) <= len (Gauge (C,1)) ) by JORDAN1B:11, JORDAN1B:13;
A11: 1 <= Center (Gauge (C,i)) by JORDAN1B:11;
then A12: ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1 by A3, A4, A7, GOBOARD5:2;
0 + 1 <= i by A2, NAT_1:13;
then A13: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 by A11, A7, A10, JORDAN1A:43;
A14: (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) c= (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) or a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) )
assume A15: a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) ; ::_thesis: a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))
then reconsider q = a as Point of (TOP-REAL 2) ;
A16: a in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A15, XBOOLE_0:def_4;
A17: a in L~ (Lower_Seq (C,i)) by A15, XBOOLE_0:def_4;
then q in (L~ (Lower_Seq (C,i))) \/ (L~ (Upper_Seq (C,i))) by XBOOLE_0:def_3;
then q in L~ (Cage (C,i)) by JORDAN1E:13;
then S-bound (L~ (Cage (C,i))) <= q `2 by PSCOMP_1:24;
then A18: ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= q `2 by A7, JORDAN1A:72, JORDAN1B:11;
((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A3, A4, A11, A7, JORDAN1A:19;
then ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A13, XXREAL_0:2;
then A19: q `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A16, TOPREAL1:4;
q `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1 by A9, A12, A16, GOBOARD7:5;
then q in LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A12, A19, A18, GOBOARD7:7;
hence a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) by A17, XBOOLE_0:def_4; ::_thesis: verum
end;
A20: (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by RLTOPSP1:68;
((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A3, A4, A11, A7, JORDAN1A:19;
then (Gauge (C,i)) * ((Center (Gauge (C,i))),1) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A9, A12, A13, GOBOARD7:7;
then LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A20, TOPREAL1:6;
then (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) c= (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) by XBOOLE_1:27;
then (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) = (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) by A14, XBOOLE_0:def_10;
then A21: upper_bound (proj2 .: ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))))) = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) by A2, JORDAN1G:56;
A22: ( Lower_Seq (C,i) is_sequence_on Gauge (C,i) & Upper_Arc (L~ (Cage (C,i))) c= L~ (Cage (C,i)) ) by JORDAN1F:12, JORDAN6:61;
len (Gauge (C,i)) >= 4 by JORDAN8:10;
then width (Gauge (C,i)) >= 4 by JORDAN8:def_1;
then 1 <= width (Gauge (C,i)) by XXREAL_0:2;
then A23: [(Center (Gauge (C,i))),1] in Indices (Gauge (C,i)) by A11, A7, MATRIX_1:36;
[(Center (Gauge (C,i))),k] in Indices (Gauge (C,i)) by A3, A4, A11, A7, MATRIX_1:36;
then consider n being Element of NAT such that
A24: 1 <= n and
A25: n <= k and
A26: ((Gauge (C,i)) * ((Center (Gauge (C,i))),n)) `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))))) by A3, A4, A5, A11, A7, A23, A22, JORDAN1F:2, JORDAN1G:46;
take n ; ::_thesis: ( 1 <= n & n <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) )
thus 1 <= n by A24; ::_thesis: ( n <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) )
thus n <= width (Gauge (C,i)) by A4, A25, XXREAL_0:2; ::_thesis: p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n)
then p `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),n)) `1 by A1, A2, A24, JORDAN1G:35;
hence p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) by A6, A26, A21, TOPREAL3:6; ::_thesis: verum
end;