let n be Nat; :: thesis: for C being non empty connected compact non horizontal non vertical Subset of () 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 (); :: 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 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 ;
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 ;
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 ;
then (Cage (C,n)) . 1 = W-min (L~ (Cage (C,n))) by ;
hence contradiction by A11, A10, FINSEQ_4:24; :: thesis: verum
end;
1 <= len (Gauge (C,n)) by ;
then A12: [1,j] in Indices (Gauge (C,n)) by ;
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 ;
then (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by ;
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 ;
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 ;
A19: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by ;
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 ;
A22: ( 1 <= kj & ki <= len (Gauge (C,n)) ) by ;
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 ;
then ((Gauge (C,n)) * (1,j)) `1 = ((Gauge (C,n)) * (ki,kj)) `1 by ;
then A25: ki = 1 by ;
2 <= len (Cage (C,n)) by ;
then (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in W-most (L~ (Cage (C,n))) by ;
then ((Gauge (C,n)) * (1,j)) `2 <= ((Gauge (C,n)) * (ki,kj)) `2 by ;
then A26: j <= kj by ;
( [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 ;
then |.(1 - ki).| + |.(j - kj).| = 1 by ;
then A27: 0 + |.(j - kj).| = 1 by ;
then A28: (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (1,(j + 1)) by ;
A29: kj = j + 1 by ;
then ( 1 <= j + 1 & j + 1 <= width (Gauge (C,n)) ) by ;
then [1,(j + 1)] in Indices (Gauge (C,n)) by ;
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 ;
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 ;
1 <= j + 1 by ;
then A33: ((Gauge (C,n)) * (2,(j + 1))) `1 = W-bound C by ;
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 ;
then A35: j < width (Gauge (C,n)) by NAT_1:13;
A36: 2 <= len (Gauge (C,n)) by ;
1 < len (Gauge (C,n)) by ;
then LSeg (((Gauge (C,n)) * ((1 + 1),j)),((Gauge (C,n)) * ((1 + 1),(j + 1)))) c= cell ((Gauge (C,n)),1,j) by ;
then A37: not W-min C in LSeg (((Gauge (C,n)) * (2,j)),((Gauge (C,n)) * (2,(j + 1)))) by ;
A38: ( 1 <= j + 1 & j + 1 <= width (Gauge (C,n)) ) by ;
j <= len (Gauge (C,n)) by ;
then A39: ((Gauge (C,n)) * (2,j)) `1 = W-bound C by ;
(W-min C) `1 = W-bound C by EUCLID:52;
then A40: ( (W-min C) `2 > ((Gauge (C,n)) * (2,(j + 1))) `2 or () `2 < ((Gauge (C,n)) * (2,j)) `2 ) by ;
per cases ) `2 > ((Gauge (C,n)) * (1,(j + 1))) `2 or () `2 < ((Gauge (C,n)) * (1,j)) `2 ) by ;
suppose A41: (W-min C) `2 > ((Gauge (C,n)) * (1,(j + 1))) `2 ; :: thesis: contradiction
cell ((Gauge (C,n)),1,j) meets C by ;
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 () by A42;
A43: c in cell ((Gauge (C,n)),1,j) by ;
A44: c in C by ;
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 ;
then c `1 <= ((Gauge (C,n)) * ((1 + 1),j)) `1 by ;
then c in W-most C by ;
then A47: c `2 >= () `2 by PSCOMP_1:31;
c `2 <= ((Gauge (C,n)) * (1,(j + 1))) `2 by ;
hence contradiction by A41, A47, XXREAL_0:2; :: thesis: verum
end;
suppose A48: (W-min C) `2 < ((Gauge (C,n)) * (1,j)) `2 ; :: thesis: contradiction
west_halfline () meets L~ (Cage (C,n)) by ;
then consider r being object such that
A49: r in west_halfline () and
A50: r in L~ (Cage (C,n)) by XBOOLE_0:3;
reconsider r = r as Element of () by A49;
r in () /\ (L~ (Cage (C,n))) by ;
then r `1 = W-bound (L~ (Cage (C,n))) by ;
then r in W-most (L~ (Cage (C,n))) by ;
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 ;
hence W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1) by ; :: thesis: verum