let n be 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)
let C be non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2); 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 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 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))
;
contradictionthen
(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;
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_0:30;
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 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_0:32;
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
|.(1 - ki).| + |.(j - kj).| = 1
by A6, A18, A13, A15, FINSEQ_4:20, GOBOARD5:12;
then A27:
0 + |.(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_0:32;
then
[1,(j + 1)] in Indices (Gauge (C,n))
by A5, MATRIX_0:30;
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 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_0:32;
1
<= j + 1
by A20, A29, MATRIX_0:32;
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)))
;
contradiction
j + 1
<= width (Gauge (C,n))
by A20, A29, MATRIX_0:32;
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_0:32;
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;
per cases
( (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;
suppose A41:
(W-min C) `2 > ((Gauge (C,n)) * (1,(j + 1))) `2
;
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
object 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_0:32, 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;
verum end; suppose A48:
(W-min C) `2 < ((Gauge (C,n)) * (1,j)) `2
;
contradiction
west_halfline (W-min C) meets L~ (Cage (C,n))
by JORDAN1A:54, SPRECT_1:13;
then consider r being
object 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;
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; verum