let n be Nat; :: thesis: for C being non empty connected compact non horizontal non vertical Subset of () 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 (); :: 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 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 ;
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 ;
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 ;
then (Cage (C,n)) . 1 = S-max (L~ (Cage (C,n))) by ;
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 ;
then (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by ;
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 ;
(Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (j,1) by ;
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 ;
A19: ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by ;
then consider kj, ki being 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 ;
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 ;
A23: ki <= width (Gauge (C,n)) by ;
A24: 1 <= kj by ;
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then A25: [j,1] in Indices (Gauge (C,n)) by ;
then A26: [((j -' 1) + 1),1] in Indices (Gauge (C,n)) by ;
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 ;
then ((Gauge (C,n)) * (j,1)) `2 = ((Gauge (C,n)) * (kj,ki)) `2 by ;
then A29: ki = 1 by ;
[j,1] in Indices (GoB (Cage (C,n))) by ;
then |.(1 - ki).| + |.(j - kj).| = 1 by ;
then A30: 0 + |.(j - kj).| = 1 by ;
A31: kj <= len (Gauge (C,n)) by ;
2 <= len (Cage (C,n)) by ;
then (Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in S-most (L~ (Cage (C,n))) by ;
then ((Gauge (C,n)) * (j,1)) `1 >= ((Gauge (C,n)) * (kj,ki)) `1 by ;
then kj <= j by ;
then kj + 1 = j by ;
then A32: kj = j - 1 ;
then kj = j -' 1 by ;
then A33: [(j -' 1),1] in Indices (Gauge (C,n)) by ;
(Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * ((j -' 1),1) by ;
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 ;
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 ;
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 ;
then j -' 1 < j by NAT_D:51;
then j -' 1 < len (Gauge (C,n)) by ;
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 ;
then LSeg (((Gauge (C,n)) * ((j -' 1),2)),((Gauge (C,n)) * (j,2))) c= cell ((Gauge (C,n)),(j -' 1),1) by ;
then A39: not S-max C in LSeg (((Gauge (C,n)) * ((j -' 1),2)),((Gauge (C,n)) * (j,2))) by ;
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then A40: 2 <= width (Gauge (C,n)) by ;
A41: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A42: j -' 1 <= len (Gauge (C,n)) by ;
then A43: ((Gauge (C,n)) * ((j -' 1),2)) `2 = S-bound C by ;
( ((Gauge (C,n)) * (j,2)) `2 = S-bound C & () `2 = S-bound C ) by ;
then A44: ( (S-max C) `1 > ((Gauge (C,n)) * (j,2)) `1 or () `1 < ((Gauge (C,n)) * ((j -' 1),2)) `1 ) by ;
per cases ) `1 < ((Gauge (C,n)) * ((j -' 1),1)) `1 or () `1 > ((Gauge (C,n)) * (j,1)) `1 ) by ;
suppose A45: (S-max C) `1 < ((Gauge (C,n)) * ((j -' 1),1)) `1 ; :: thesis: contradiction
cell ((Gauge (C,n)),(j -' 1),1) meets C by ;
then (cell ((Gauge (C,n)),(j -' 1),1)) /\ C <> {} by XBOOLE_0:def 7;
then consider c being object such that
A46: c in (cell ((Gauge (C,n)),(j -' 1),1)) /\ C by XBOOLE_0:def 1;
reconsider c = c as Element of () by A46;
A47: c in cell ((Gauge (C,n)),(j -' 1),1) by ;
A48: c in C by ;
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 ;
then c `2 <= ((Gauge (C,n)) * ((j -' 1),(1 + 1))) `2 by ;
then c in S-most C by ;
then A51: c `1 <= () `1 by PSCOMP_1:55;
((Gauge (C,n)) * ((j -' 1),1)) `1 <= c `1 by ;
hence contradiction by A45, A51, XXREAL_0:2; :: thesis: verum
end;
suppose A52: (S-max C) `1 > ((Gauge (C,n)) * (j,1)) `1 ; :: thesis: contradiction
south_halfline () meets L~ (Cage (C,n)) by ;
then consider r being object such that
A53: r in south_halfline () and
A54: r in L~ (Cage (C,n)) by XBOOLE_0:3;
reconsider r = r as Element of () by A53;
r in () /\ (L~ (Cage (C,n))) by ;
then r `2 = S-bound (L~ (Cage (C,n))) by ;
then r in S-most (L~ (Cage (C,n))) by ;
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 ;
hence S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (L~ (Cage (C,n)))))),1) by ; :: thesis: verum